[mercury-users] Polymorphism / Type classes

[David Jeffery]

On 14-Jun-2001, Michael Day <mikeday at corplink.com.au> wrote:
> 
> The code below doesn't work, as the types for the predicate argument of
> with_useful and do_stuff don't match up? Are too polymorphic? Anyway, I
> can't seem to specify the right type class constraints to make this work.
> Does anyone know if this is possible?
> 
> :- typeclass useful_factory(F) where
> 	[
> 		pred with_useful(pred(U, U), F, F) <= useful(U),
> 		mode with_useful(in(pred(di, uo) is det), di, uo) is det
> 	].
> 
> :- pred do_useful(F, F) <= useful_factory(F).
> :- mode do_useful(di, uo) is det.
> 
> do_useful -->
> 	with_useful(do_stuff).	% type error
> 
> :- pred do_stuff(U, U) <= useful(U).
> :- mode do_stuff(di, uo) is det.
> 
> do_stuff --> does lots of stuff.

If I understand your example correctly, it looks like you are trying
to use second order polymorphism (which we have no direct support for at this
stage).

Basically, the problem is that you are trying to pass a predicate to
with_useful that works on any type U which is in the type class 'useful'.
In our current type system, we only allow you, for any type U with is in the
type class 'useful', to pass a predicate that works on U. Sounds like the same
thing? The difference is perhaps fairly subtle.

You have written the type of your 'with_useful' method as:

	all [U] pred with_useful(pred(U, U), F, F) <= useful(U)

whereas what I think you are trying to say is something like

	pred with_useful(all [U] pred(U, U) <= useful(U), F, F)

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).

How do you get around it? Two ways, and neither of them is terribly pretty.

First, you can re-arrange your code so that the type that you call
`do_stuff' with is bound at the point at which you call with_useful. Not
always easy to do...

The other way is to use a trick with type classes. This trick takes advantage
of the fact that the implementation of type classes effectively uses
second order polymorphism to encode the type class dictionaries (although
this is hidden in a layer of C code because our compiler back end can't
handle second order polymorphism at the moment).

Basically, rather than trying to pass along a polymorphic predicate as
a first class object (ie. with its `all' still intact),
we use type classes to associate a polymorphic predicate with a type, 
and pass a value of that type along. The polymorphic predicate is passed
along implicitly in the type class dictionary:

:- typeclass foo(T) where [
	pred dummy(T, U, U) <= useful(U)
].

...and then you change your type class as follows:

:- typeclass useful_factory(F) where
	[
		pred with_useful(T, F, F) <= foo(T),
		mode with_useful(in, di, uo) is det
	].

Now, rather than passing a predicate to with_useful, you create a new
type to associate with that predicate, and pass a value of that type
instead.

:- 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.

And there you have it... all you have to do is change the call to with_useful
to use the type class trick too:

:- pred do_useful(F, F) <= useful_factory(F).
:- mode do_useful(di, uo) is det.

do_useful -->
	with_useful(dummy1).	% Implicitly pass the polymorphic class method

And that's it.

It you want to pass a different predicate to do_useful, you just create a
new instance of `foo'.

HTH.

Enough babble from me... you just managed to ask me a question about
exactly the material that I'm currently writing in my thesis...


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
--------------------------------------------------------------------------