# type signatures with existentially quantified data constructors

Koen Claessen koen@cs.chalmers.se
Fri, 31 Aug 2001 17:58:30 +0200 (MET DST)

```Levent Erkok wrote:

| data Expr a = Haskell a
|             | If (Expr Bool) (Expr a) (Expr a)
|             | forall b . Appl (Expr (b->a)) (Expr b)
|             | forall b c . MkPair (Expr b) (Expr c) (b -> c -> a)

This is a beautiful solution!

The third argument to MkPair can be seen as "proof" that the
expression constructed really is a pair.

This trick reminds me bit of a solution I came up with in
the following situation. When dealing with different kinds
of indexing structures (lists, arrays, etc.), it is often
useful to have a type class of the following kind:

class Indexing c where
(!) :: c a -> Int -> a

It is possible to make the following instances:

instance Indexing [] where
(!) = (!!)

instance Indexing Array where
(!) = (Array.!)

However, there are also other structures in which one would
like to index, such as bit-arrays, which have the following
signature:

data BitArray -- abstract
(!) :: BitArray -> Int -> Bool
...

It is then possible to make the following type:

data BitArray' a
= MkBitArray BitArray (a -> Bool) (Bool -> a)

The first argument is the real bit array, the second and
third are the "proof" that the type parameter 'a' is really
a boolean (or isomorphic to it). (Often it is useful to have
the conversion both ways).

Now one can make the instance:

instance Indexing BitArray' where
MkBitArray arr back forth ! i = forth (arr BitArray.! i)

This trick is akin to implementing for example Sets (which
require equality to be defined on their arguments) as
follows:

data Set a = MkSet [a] (a -> a -> Bool)

empty :: Eq a => Set a
empty = MkSet [] (==)

union :: Set a -> Set a -> Set a -- no type constraints!!
MkSet xs1 eq `union` MkSet xs2 _ = nubBy eq (xs1 ++ xs2)

...

Note that none of these tricks require type system features
that lie outside Haskell98! I used these tricks heavily when
converting TkGofer (that used multiple-parameter type
classes and overlapping instances) to pure Haskell98. (The
result is called Yahu, and will be soon available for