[MLton-user] a new approach to type-indexed values in SML

[Vesa Karvonen]

Quoting Stephen Weeks <sweeks at sweeks.com>:
[...]
> I've been thinking about how to define type-indexed values in a more
> modular/extensible way, closer to how Haskell type classes are done.

I haven't yet had the time to read your post (or look at the code), but
are you aware of the following (Haskell) papers:

  Generics for the Masses
  Ralf Hinze
  http://www.informatik.uni-bonn.de/~ralf/publications/ICFP04.pdf

  TypeCase: A Design Pattern for Type-Indexed Functions
  Oliveira and Gibbons
  http://citeseer.ist.psu.edu/oliveira05typecase.html

(I bumped into the former article recently by reading the latter.)  The
second technique explained in Hinze's paper is a close relative of the
value dependent encoding technique in SML.

At any rate, Haskell's type classes weren't exactly designed for the kind
of generic (or closed type-indexed) programming that is done in the above
two papers (and many others).

> The lack of first-class polymorphism in SML might make it seem
> impossible [...]

Indeed.  The way I understand them, type classes do not (really) increase
the expressive power of the type system.  Haskell techniques that (initially)
seem to do things with type classes that appear impossible in SML generally
(upon closer inspection) seem to also use either polymorphic recursion or
higher-rank polymorphism.  If you ask me, and if one has to choose, I'd take
higher-rank polymorphism and polymorphic recursion (in that order) before type
classes.   (I'd also love to see a cure for the value restriction.)  What type
classes do provide is a kind of inference mechanism that allows many (but not
all) things to be constructed implicitly as guided by the types.  This is a
two edged sword, however, as code can become locally very hard to understand.

It seems to me that type classes are fundamentally more important in a purely
functional language.  The reason for this is that without them (or some other
mechanism that allows things to be constructed or passed implicitly) one has
to pass everything explicitly and that can become extremely tedious or even
make some abstractions impossible.  Consider the following paper, for example:

  Functional Pearl: Implicit Configurations
  Kiselyov and Shan
  http://www.eecs.harvard.edu/~ccshan/prepose/prepose.pdf

(Admittedly the technique has some nice properties.)

Actually, I'm not even entirely sure whether type classes really fit nicely
into the imperative world of ML.  It seems intuitively important to me that
the construction of type class dictionaries is free of side-effects, because
it happens implicitly.  However, when one wants to build a type-index for an
imperative type (ref or array) one sometimes really needs to perform a
side-effect and one needs to be able to control when side-effects occure.
Consider the show function for instance.  Cycle detection relies on performing
a side-effect.

-Vesa Karvonen