[Haskell] sugar for extensible types (was: class associated types, via GADTs.)

[Ralf Laemmel]

Assoc types and GADTs are great but
I am still too fond of encoding extensible datatypes with (open) classes.
I contributed to some related discussion at comp.compilers a while ago [1].
The Haskell code samples are worth sharing (because they are sooooo simple):

http://homepages.cwi.nl/~ralf/OOHaskell/src/interpreter/nonextensible.hs
http://homepages.cwi.nl/~ralf/OOHaskell/src/interpreter/extensible.hs
(Note: *no* OOHaskell idioms used.)

My conclusion at that time was:

1. Style/verbosity-wise, this is close to mainstream OOP.

2. It would be great (and rather trivial) to provide syntactic sugar for 
"data"
to replace the class/instances needed per extensible datatype.
Reifying closed datatypes as open classes is folk-lore.

3. I am not too much concerned to write equations of extensible functions
as instances of a dedicated class. One reason to complain is of course that
the programmer had to provide instance constraints for each equation (in
fact, instance) of an extensible function. (In particular, I mean the 
instance
constraints for recursive occurrences of the extensible function under 
definition.)

So type inference would fall short for extensible datatypes.

4. But this is not difficult to resolve either.
The existing compiler/type system does all the hard work already.
That is, each equation of an extensible function is hiddenly given
to the type checker as a normal function using a fresh function symbol 
on the LHS.
The class constraints of the thereby inferrable type can now be turned 
into instance
constraints for the equation-encoding instance of the class for the 
extensible function.
(Thanks to Oleg for enlightening me.)

Add some syntactic sugar to that, and you are done.

5. One remaining problem is about type signatures,
in particular, the inferred type signatures such as those obtained by "t:".

The problem is that they blow up whenever a concrete value of an extensible
datatype is involved. We would see the entire term structure in the type!
How difficult could it be to inform the type-checker, or (I am kidding)
just the pretty printer for type signatures such that types for extensible
types are generalised to the corresponding class before printing.

A bit more cheating:  the class is not reported as a constraint on the LHS
of "=>" but as (extensible) type on the RHS of "=>". Not difficult.

This should also work the other way around, say, we would also be allowed to
enter type signatures where we use the names of extensible datatypes in 
types
without exposing the underlying nature of these extensible datatypes to 
correspond
to classes.

6. There is one _real_ problem, which is about the size of the resulting 
dictionaries,
and the complexity of the operations on that. There is a good chance 
that our
extensible datatypes won't scale in current Haskell implementations. I 
am sure that
some sort of memoisation for dictionary types/constraint checking should
provide sufficient help here. However I don't hold my breath --- this 
might be difficult.

Ralf

[1] http://compilers.iecc.com/comparch/article/04-12-111

-- 
Ralf Lammel
ralfla at microsoft.com
Microsoft Corp., Redmond, Webdata/XML
http://www.cs.vu.nl/~ralf/