Types from values using existential types?

Fergus Henderson fjh@cs.mu.oz.au
Sat, 10 Feb 2001 18:37:03 +1100


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.