Types from values using existential types?
Fri, 9 Feb 2001 18:54:13 -0500
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
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))
Are there any pointers to previous work I should look at?