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