Types from values using existential types?

Dylan Thurston dpt@math.harvard.edu
Sat, 10 Feb 2001 18:26:48 -0500


Thanks for the very informative message!

On Sat, Feb 10, 2001 at 06:37:03PM +1100, Fergus Henderson wrote:
> On 09-Feb-2001, Dylan Thurston <dpt@math.harvard.edu> wrote:
> > ...
> > singleton returns a token of some new type; this token can then be
> > passed around, stored in data structures, etc., to guarantee type
> > consistency.
> Could you elaborate a bit on how this would be used?

I thought you elaborated very well; I'm not sure what to add.  Your
matrix examples in Mercury are exactly what I want to do.

(I added the "Singleton" class so that one could go backwards,
reconstructing a value from the type, to, e.g., print out the matrix.
But it is not necessary; it's easy enough to keep track of the value
separately.  

> > I have no idea what existential types would do to the Haskell type
> > system; is there a way to add them to preserve decidability, etc, etc?
>
> Most of the Haskell implementations support existential types,
> although only in data structures, not for functions.
> Mercury supports existential types on functions, though.
> 
> To get your example to work with Hugs/ghc, you'd need to enable
> Hugs/ghc extensions, and write it as
> 
> 	data SomeSingleton a = forall b . Singleton a b => SomeSingleton a
> 
> 	singleton :: a -> SomeSingleton a
> 
> Code which calls singleton will then need to explicitly pattern-match
> the result against `SomeSingleton x'.

Yes, this occurred to me after I sent the message.  It seems like
rather a pain to always wrap your existential types inside data
structures, although potentially doable.

> > Are there any pointers to previous work I should look at?
> 
> 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?  Where can I read
about it?  (None of the papers on the home page seemed directly
relevant.)  Does it work with type inference, as in Haskell?

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

> Mercury's "term" module, which provides an interface for manipulating
> Prolog-style terms, defines types for terms and variables that
> are parameterized by a dummy type variable T:
>  <deleted>
> The only purpose of this type variable T is to ensure that you don't
> mix terms of different types. ...

This is reminiscent of another approach I thought of, where you have a
number of dummy types:
  data MatSize1 = MatSize1
  data MatSize2 = MatSize2
  ...
and then have your matrices parametrized by these.

> For matrices you want something more general, of course.
> You could do it with an existentially typed function to construct
> a new matrix:
>  <deleted>
> I don't think you need the `singleton' function
> or the `singetonValue' type class that you mentioned.
> As you can see from the example above, it can be done
> just using existentially typed functions and the module system.
> I don't think there's any need to generalize it.

As I mentioned above, I've been convinced that singleton can be
constructed from a more primitive function that returns a different
type on each call.  (Or maybe the same type, but in a disguised way.)

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

Best,
	Dylan Thurston