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