monomorphisation in Haskell

[Bernard James POPE]

Hi Henry and others,

I have sent this to Lee Naish and Toby Ord because they are working in
the debugger too and I think they will be interested in this
discussion.

> I'm not super familiar with Haskell, but I'm really surprised to hear that it
> has polymorphic recursion.  Given the undecidability  of  type  inference  in
> this  case,  I  assume  that  you  must  explicitly  type definitions of such
> functions.  Is this correct?

Yes, you must provide type signatures if you want polymorphic recursion. 
This is a requirement of the Mycroft type-checking algorithm (not type 
inference). Haskell uses Hindley Milner inference when no sigs are provided, 
and Mycroft when they are provided.

Polymorphic recursion doesn't get used that often, typically only for
weird data-structures. I think Chris Okasaki has used PR in
his book Purely Functional Data Structures:
http://www.cs.columbia.edu/~cdo/papers.html#cup98

> Also I assume that Haskell does not have the value  restriction  of  ML,  and
> Stephen  and  I  were  talking  relatively recently about how it is only this
> which makes monomorphisation possible.

Haskell is purely functional so the value restriction is not required.

>   In Haskell you don't  have  any  side
> effects, but still, how would you translate something like the following:
> 
>     val f: unit -> 'a -> 'a =
>        fn () =>
>           let fun loop n =
>                      if n = 0
>                         then ()
>                         else loop (n - 1)
>               val _ = loop 10000000
>           in fn x => x
>           end
> 
>     val g: 'a -> 'a = f ()
>     val _ = g "foo"
>     val _ = g true

The equivalent Haskell code is:

      f :: () -> a -> a
      f = \() -> let loop n =  
                       if n == 0 
                          then () 
                          else loop (n - 1) 
                 in loop 1000000 `seq` (\x -> x)

      g :: a -> a
      g = f () 

      topLevel :: String
      topLevel = g "foo" ++ show (g True)

The seq forces its left argument to evaluate to WHNF. This must be done b/c 
Haskell is lazy, so normally the loop would never be run b/c its result 
is not required.

> If  you  duplicate  the  definition  of  g for the two types it is applied to
> (string and bool) then you will have to run the loop action twice instead  of
> just once.  

This is true.

> Given that your use is for a debugger, I guess you could do this,
> but for a compiler the results would be rather catastrophic.

For the debugger we pay the cost of extra computation (sigh).

However, it is not as bad as you might think. With our debugger, we only
specialise when a type variable is instantiated with a functional type
(something with an arrow in it). So for the above example we do not call 
different versions of g for the two types it is called in, and hence we only 
run the loop once. Having said that, you could easily construct an example 
where higher order arguments are used, and we would have to specialise apart.
Thus I should point out that in the debugger we are not obliged to always
specialise polymorphic functions, we only do so in selected cases. For a
compiler you might always have to do this. I suppose if you were to
relax the value restriction from ML then you could specialise only those
parts of the program that abided by the original restriction, anything else
would have to be generated as polymorphic code and hence used boxed 
representations. The downside is that you would need to box and unbox values
all over the place and this would be messy and slow.

Monomorphisation is not possible in general (as far as we know) when you 
encounter polymorphic recursion. I think this point is made in some of the
material that Stephen sent me.

So we can only debug the subset of Haskell that is restricted to monomorphic
recursion.

Regards,
Bernie.