Types from values using existential types?

[Fergus Henderson]

On 10-Feb-2001, Dylan Thurston <dpt@math.harvard.edu> wrote:
> I sent the message.  It seems like
> rather a pain to always wrap your existential types inside data
> structures,

Yes, definitely.

> > You might want to  consider trying this with Mercury, since Mercury
> > has both multiparameter type classes and existential types for
> > functions.  (On the other hand, Mercury's restrictions on instance
> > declarations can cause difficulties for the use of multiparameter
> > type classes, so this design might not be workable in Mercury as it
> > currently stands.)
> 
> Great, thanks!  I looked at it a little, and so far it looks like
> quite an elegant type system.  But is it decidable?

The existential types part is decidable.

(Mercury's type system as a whole is not decidable because we allow
inference of polymorphic recursion.  But decidability is not really so
important.  Being able to infer polymorphic recursion is more useful
than decidability.)

> Where can I read
> about it?  (None of the papers on the home page seemed directly
> relevant.)

David Jeffery and I have been working on a paper on this.  Well, to be
fair, David has been working on it; I really haven't done much in the
way of writing for it yet.  But I don't think the current draft is
ready for public consumption at this point.

Of course, we freely distribute the source code for the Mercury
compiler.

> Does it work with type inference, as in Haskell?

Yes.

> > Mercury's "store" module uses existential types in this fashion to
> > ensure that each call to `store__new' is treated as having a different
> > type, to ensure that you don't use a key from one store as an index
> > into a different store.  This is similar to the Hugs/ghc `runST'
> > function, although `runST' uses continuation passing and explicit
> > universal quantification (a.k.a. "first class polymorphism"),
> > rather than existential quantification.  The paper "Lazy functional
> > state threads" by John Launchbury and Simon L Peyton Jones has a
> > description of how `runST' works, IIRC.
> 
> I'll take a look to see if I can use the techniques in 'runST' to hide
> the existential quantification, though I'm initially sceptical.

Well, I'm pretty sure it could be done, but doing it this way is a pain,
because it forces the user of such a routine to restructure their
program using continuation passing.  Existential types are a nicer
approach.

> > I think there might also be some stuff on types for matrices in Chris
> > Okasaki's work.
> 
> I'll look it up.  Should I look in his book?

I must shamefully confess that I haven't read his book, so I don't
know if it is in there.  I just have a vague recollection from
some talk I've heard or paper I've read.

The stuff I'm thinking of didn't involve existential types,
but used types that represented integers (using successor
arithmetic and the like) as type parameters.

Oh, here we are... I just tried an internet search for
"Chris Okasaki matrix matrices type" and altavista pulled up
the following reference, which I'm pretty sure is the one
I was thinking of:

 | International Conference on Functional Programming, September 1999,
 | pages 28-35. (136K postscript)
 | 
 | Abstract:
 | 
 | Square matrices serve as an interesting case study in functional
 | programming. Common representations, such as lists of lists, are both
 | inefficient--at least for access to individual elements--and
 | error-prone, because the compiler cannot enforce ``squareness''.
 | Switching to a typical balanced-tree representation solves the first
 | problem, but not the second. We develop a representation that solves
 | both problems: it offers logarithmic access to each individual element
 | and it captures the shape invariants in the type, where they can be
 | checked by the compiler. One interesting feature of our solution is
 | that it translates the well-known fast exponentiation algorithm to the
 | level of types. Our implementation also provides a stress test for
 | today's advanced type systems--it uses nested types, polymorphic
 | recursion, higher-order kinds, and rank-2 polymorphism.
 |
 | http://www.cs.columbia.edu/~cdo/icfp99.ps

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.