[mercury-users] Polymorphism / Type classes

[David Jeffery]

On 14-Jun-2001, Ralph Becket <rbeck at microsoft.com> wrote:
> > From: David Jeffery [mailto:dgj at cs.mu.OZ.AU]
> > Sent: 14 June 2001 11:55
> > [...]
> > As it is written as the moment, the definition of do_useful quite 
> > correctly gives a type error. This is because the type checker 
> > needs to bind the type `U' to something, and ensure that this 
> > type is in the useful type class. Given that the type variable 
> > isn't bound to anything, we implicitly bind it to `void', and 
> > there is no instance for useful(void).
> 
> Is there a simple explanation for why 2nd order polymorphism is
> hard?

A simple explanation? Not really.

Well, one point is that if you aren't careful, type unification becomes
undecidable. The details are rather compicated, but you can kind of think of
`all' in a type as being like `\lambda' in an expression in lambda calculus.
If you allow them in arbitrary places, then reducing an expression doesn't
necessarily terminate. (Well, they're kind of similar mechanisms).

But the good news is that if you restrict `all' quantifiers to a nesting
depth of only 2, type unification is decidable. This is called rank 2
polymorphism. (Type checking under rank 3 or more is undecidable.)

There would still be some complications to the type checker, but it is 
essentially doable. Not sure what the repurcussions on the rest of the
compiler might be... I imagine quite a few things might break.

Implementing the RTTI side of things might not be all that straightforward.
You need to pass around a runtime representation of a truly polymorphic
type, and instantiate that with various types are runtime.
There is *some* support for instantiating type variables (pseudo typeinfos)
in the RTTI, so it mightn't be as horrendous as I think.
But then, these things typically turn out to be far more horrendous than
I think. ;-)

> > :- type dummy1 ---> dummy1.
> > :- instance foo(dummy1) where [
> > 	dummy(_A, B, C) :- do_stuff(B, C)
> > ].
> > 
> > :- pred do_stuff(U, U) <= useful(U).
> > :- mode do_stuff(di, uo) is det.
> > 
> > do_stuff --> does lots of stuff.
> 
> Hooargh!  Will life always be like this?

Well, Fergus and I have gone over some of the details of implementing rank 2
polymorphism, and I think there is a good chance that it will be added to
the language one day. When someone gets around to implementing it,
which would be a non-trivial amount of work.

FWIW, rank 2 polymorphism is not part of Haskell 98. There is an implementation
in GHC, but you have to pass '-fglascow-exts' or somesuch to the compiler.

> If I write
> 
> :- typeclass a(A) where [ func f(all [B] func(B) = B <= b(B), A) = A ].
> 
> :- typeclass b(B) where [].
> 
> :- func g(T1) = T1 <= a(T1).
> g(X) = f(h, X).
> 
> :- func h(T2) = T2 <= b(T2).
> h(Y) = Y.
> 
> then I get all sorts of syntax errors on the definition for typeclass a.
> Is this a 2nd order polymorphism thing?

Well, it's because you're using a made up syntax for a feature that isn't
implemented!

> I think we're going to need some very clear explanation of these points
> if people are going to use typeclasses for fun and profit.  It all looks
> so like it should work and it's frustrating not to have a clear picture
> of where things went wrong!

Well, as I pointed out in another mail, this really has nothing to do
with type classes. It just so happens that the predicate we are talking
about is a class method, but it could well have been a plain old, vanilla
flavoured predicate. (Then again, maybe this style of programming is more 
common with type classes. (?))


dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) | If you want to build a ship, don't drum up 
PhD student,                    | people together to collect wood or assign 
Dept. of Comp. Sci. & Soft. Eng.| them tasks and work, but rather teach them 
The University of Melbourne     | to long for the endless immensity of the sea.
Australia                       | -- Antoine de Saint Exupery
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------