[mercury-users] Document Giving Help with Typeclasses

[Tyson Dowd]

On 02-Nov-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> I've been bitten quite hard when trying to use typeclasses and it seems
> I'm not alone.  Below is a document I've knocked out that describes most
> of the problems I've come up against, explains what the problem is and
> provides the solution.  Feedback most welcome, esp. error reports.

Thanks Ralph, this looks like a good start on an important document.

I've got a few comments inline (hopefully more to come).

> 
> Cheers,
> 
> Ralph
> 
> 
> 
> Typeclasses.txt		Ralph Becket <rbeck at microsoft.com>	2 Nov 2000
> 
> 
> 
> Understanding how typeclasses, multi-parameter typeclasses, and existential
> types work has been an uphill struggle.  It is obvious from the Mercury 
> mailing lists that I'm not the only person who's found them tricky.  This
> document is intended to convey what I have learned and hopefully will be of
> assistance to other people in getting to grips with typeclasses.
> 
> Many thanks to Fergus for all his help in leading me to this point.
> 
> 
> 
> EXISTENTIAL TYPES
> 
> Q. What's the difference between existential types and polymorphic types?
> 
> A. A polymorphic type is decided by the caller, so
> 
> :- func make_pair(T) = {T, T}.
> make_pair(X) = {X, X}.
> 
> has to work for *any* type T that is passed to it by the caller.

Add something like:

It is as if there is an explicit `for all [T]' attached to the
function's type signature. 

Note that this is why a value of type T needs to be an input parameter.

> Sometimes, however, we want things to work the other way around.  Consider
> 
> :- type db(DB) ---> db(DB, map(key(DB), record)).
> :- type record.
> :- type key(DB).
> 
> :- some [DB] func new_db = db(DB).
> :-           mode new_db = uo is det.
> 
> :- pred add_record(record, key(DB), db(DB), db(DB)).
> :- mode add_record(in, out, di, uo) is det.
> 
> :- pred lookup_record(key(DB), record, db(DB), db(DB)).
> :- mode lookup_record(in, out, di, uo) is det.
> 
> Here, new_db/0 generates new database objects on demand.  Each database has
> its own, unique type.  When we add records to a database, we obtain keys
> also tagged with that type.  This means that the compiler can statically
> check that we don't use keys from one database to try to access records in
> another database.
> 
> This only works because new_db/0 decides the DB type tag, not its callers.

I'm not so sure about this example, because it involves some
functionality that is under the hood which is reasonably complex.
Perhaps if the implementation were given this would be good.
It's not clear what "tagged with that type" and "unique type" mean.

Explaining that it is the :- some [DB] .... part that makes the
difference is good.

It's good to note the relationship with existential type variables and output
modes (and to compare with universal type vars and input modes).

> 
> Q. Will life always be like this?
> 
> A. Hopefully not.  Constructor classes and, in particular, functional type
> dependencies will be integrated into the typeclass mechanism and do away
> with the need for many of the work-arounds outlined in this document.

It's worth noting that AFAIK nobody is actually working on this right
now (e.g. there is nobody planning on implementing this in the next 6-12
months).  This could change, but I don't know of any plans.

-- 
       Tyson Dowd           # 
                            #  Surreal humour isn't everyone's cup of fur.
     trd at cs.mu.oz.au        # 
http://www.cs.mu.oz.au/~trd #
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------