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
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