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