TRANSLATING MONOMORPHISM TO POLYMORPHISM, AND POLYMORPHIC RECURSION
(An addition to Konstantin and Mark's remarks.)
The great thing about Milner's polymorphism is that it came for free:
adding a function declaration does not make a function more efficient.
This is true for the usual implementations of functional languages,
where all values are pointers and polymorphism is cheap. As we move to
new optimisations, such as unboxing, this is no longer the case: naive
implementations of polymorphism either don't work (one can't have
polymorphism over unboxed types in Glasgow Haskell), or are not free,
or require less naive implementation techniques (generating one
function body for each monomorphic instance at which a polymorphic
function is used).
The sad thing about Haskell's type classes is that they did not come
for free: adding a function declaration could make an overloaded
function an order of magnitude more efficient. This was true for the
naive implementation of type classes, where dictionaries are passed at
run time. But with a less naive technique, again involving monomorphic
function instances, type classes are free, in the sense that adding a
declaration does not make the program more efficient. Mark Jones and
the Glasgow group have both experimented with such definitions.
(Indeed, they are what I had in mind when type classes were first
suggested, and it is an embarassment that they have taken so long to
come into existence.)
So, we have come full circle. Sophisticated compiling techniques,
based on translating polymorphism to monomorphism, are required to
make Milner-style polymorphism free in the presence of optimisations
such as unboxing, and are required to make Haskell type classes free.
Now, it is a fact of the Milner type system that every polymorphic
program has a monomorphic equivalent. The proof is easy, just replace
every occurrence of `let x = t in u' by `u[t/x]' (that is, `u' with `t'
substituted for `x'). Of course, the latter may lead to code
explosion, but by in fact creating only one instance of `t' for each
type at which `x' is used, this explosion usually remains managable).
However, for the extended type system that allows polymorphism in
recursion, this is no longer the case -- my thanks to Lennart
Augustsson for pointing this out. The counter-example (similar
to one of Mark's) is:
g :: a -> Bool
g x = g [x]
This function is silly, as it never terminates, but there are less
silly examples; see below. Note that the trick for translating
polymorphic recursion into type classes (as described by Konstantin) no
longer works here. The closest one can come is
class G a where
g :: a -> Bool
g x = g [x]
instance G Int where
instance G [Int] where
instance G [[Int]] where
...
which requires an infinite number of instance declarations.
Incidentally, there has been a lot of work done on Milner's type
system extended to allow polymorphic recursion; this system is
sometimes called ML+. One motivating example -- which I first
heard from Milner -- is:
data Trie x = Atom x | List [Trie x]
maptrie :: (a -> b) -> Trie a -> Trie b
maptrie f (Atom x) = Atom (f x)
maptrie f (List xts) = List (map (maptrie f) xts)
(This is similar to Mark's example with functor Y.)
The function `maptrie' is untyped in ML, but typed in ML+.
So the bottom line is that Konstantin's trick gives you some of
the power of ML+, but not all of it; in particular, it does not
give sufficient power to define `maptrie'. On the other hand,
both ML and Haskell type classes admit the useful compiling
technique of transforming polymorphism to monomorphism; ML+ does
not.
Cheers, -- P
-----------------------------------------------------------------------
Philip Wadler [EMAIL PROTECTED]
Department of Computing Science tel: +44 41 330 4966
University of Glasgow fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND
