I recently had an idea to allow one to create types from values. This would have many uses in Haskell; e.g., it would be very nice to have a type of nxn matrices for n that are not necessarily statically determined. (It is easy to create a type of matrices and check that the sizes are compatible at run time; the point is to do more checks at compile time.) Of course, one has to be careful to preserve decidability of type checking. The idea is to provide a function that returns an element of an undetermined (existential) type: class Singleton a b where singletonValue :: b -> a singleton :: forall a . a -> (exists b . (Singleton a b) => b) singleton returns a token of some new type; this token can then be passed around, stored in data structures, etc., to guarantee type consistency. 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? They would clearly make some simple program transformations illegal: for the idea to be useful, the type of (a,a) where a = singleton 5 should be of type exists a . (Singleton Int a) => (a, a) while the type of (singleton 5, singleton 5) has to be ((exists a . (Singleton Int a) => a), (exists b . (Singleton Int b) => b)) for decidability. Are there any pointers to previous work I should look at? Thanks, Dylan Thurston
On 09-Feb-2001, Dylan Thurston <dpt@math.harvard.edu> wrote:
I recently had an idea to allow one to create types from values. This would have many uses in Haskell; e.g., it would be very nice to have a type of nxn matrices for n that are not necessarily statically determined. (It is easy to create a type of matrices and check that the sizes are compatible at run time; the point is to do more checks at compile time.) Of course, one has to be careful to preserve decidability of type checking.
The idea is to provide a function that returns an element of an undetermined (existential) type:
class Singleton a b where singletonValue :: b -> a
singleton :: forall a . a -> (exists b . (Singleton a b) => b)
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 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?
Yes. 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'.
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.) 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. 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: :- module term. :- interface. :- type term(T). :- type var(T). ... :- implementation. :- type term(T) ---> functor(const, list(term(T)), context) ; variable(var(T)). :- type var(T) ---> var(int). ... The equivalent in Haskell would be module Term(Term, Var, ...) where data Term t = Functor (Const, [Term t], Context) | Variable (Var t) data Var t = Var Int ... The only purpose of this type variable T is to ensure that you don't mix terms of different types. This is used by the Mercury compiler, which uses different types for different sorts of variables in the program being compiled, e.g. ordinary ("program") variables and type variables: :- type prog_var_type ---> prog_var_type. :- type prog_var == var(prog_var_type). :- type prog_term == term(prog_var_type). :- type type_var_type ---> type_var_type. :- type type_var == var(type_var_type). :- type type_term == term(type_var_type). % (the names above are changed slightly from those actually % used in the Mercury compiler) For matrices you want something more general, of course. You could do it with an existentially typed function to construct a new matrix: :- module matrix. :- interface. % An NxN matrix whose elements are of type T; % the type TypeForN is a type that % represents the natural number N. :- type square_matrix(TypeForN, ElementType). % new_matrix(N, F) returns the NxN matrix whose % elements are given by the function F :- some [TypeForN] func new_matrix(int, func(int, int) = ElementType) = square_matrix(TypeForN, ElementType). :- implementation. :- type square_matrix(TypeForN, ElementType) ---> square_matrix(int, func(int, int) = ElementType). :- type dummy ---> dummy. new_matrix(N, F) = square_matrix(N, F) `with_type` square_matrix(dummy, ElementType). 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. Sorry for all the Mercury syntax, but none of the existing Haskell implementations support existentially typed functions. The translation into Haskell would be something like this: module Matrix(SquareMatrix, new_matrix) where -- An NxN matrix whose elements are of type T; -- the type TypeForN is a type that -- represents the natural number N. data SquareMatrix type_for_n element_type = SquareMatrix Int (Int -> Int -> element_type) data Dummy = Dummy % new_matrix(N, F) returns the NxN matrix whose % elements are given by the function F new_matrix :: some type_for_n . Int -> (Int -> Int -> element_type) -> SquareMatrix type_for_n element_type new_matrix n f = SquareMatrix n f :: SquareMatrix Dummy element_type but this relies a couple of extensions to standard Haskell, at least one of which is not supported by any existing Haskell implementation. I think there might also be some stuff on types for matrices in Chris Okasaki's work. -- 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.
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
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.
I recently had an idea to allow one to create types from values. This would have many uses in Haskell; e.g., it would be very nice to have a type of nxn matrices for n that are not necessarily statically determined. (It is easy to create a type of matrices and check that the sizes are compatible at run time; the point is to do more checks at compile time.) Of course, one has to be careful to preserve decidability of type checking. ..... Are there any pointers to previous work I should look at?
If type systems for matrices are of interest for you then I think you should check out Barray Jay's work on the language FiSH. Björn Lisper
participants (3)
-
Bjorn Lisper -
Dylan Thurston -
Fergus Henderson