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.