type signatures with existentially quantified data constructors

[Koen Claessen]

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
downloading. :-)

/Koen.

--
Koen Claessen         http://www.cs.chalmers.se/~koen
phone:+46-31-772 5424      mailto:koen@cs.chalmers.se
-----------------------------------------------------
Chalmers University of Technology, Gothenburg, Sweden