type signatures with existentially quantified data constructors

[Dylan Thurston]

On Thu, Aug 16, 2001 at 01:11:25AM -0400, Avi Pfeffer wrote:
> Works fine.  Things get tricky when I try to add pairs.  In order to type
> a pair expression, I find I need to create a Pair class and introduce a 
> class constraint:
> 
> class Pair a b c | a -> b c, b c -> a 
>
> instance Pair (b,c) b c 

I tried making this:

class Pair a b c | a -> b c, b c -> a where
  mkPair :: b -> c -> a
  breakPair :: a -> (b, c)

instance Pair (b,c) b c where
  mkPair    = (,)
  breakPair = id

so that then you can do...

> data Expr a = ... | forall b c . Pair a b c => MkPair (Expr b) (Expr c)
> 
> This seems to express the right type relationships.  But now I find I
> can't write eval for MkPair:
> 
> eval (MkPair x y) = (eval x, eval y)

eval (MkPair x y) = mkPair (eval x) (eval y)

But this didn't work either.  I agree that it should.

As an alternative, you could make Expr into a class rather than a data
constructor, like this:

----
class Expr a b | a -> b where
  eval :: a -> b

data Haskell a = Haskell a
instance Expr (Haskell a) a where
  eval (Haskell x) = x

data If a = forall x y z . (Expr x Bool, Expr y a, Expr z a) => If x y z
instance Expr (If a) a where
  eval (If x y z) = if eval x then eval y else eval z

data Appl a = forall x y b . (Expr x (b -> a), Expr y b) => Appl x y
instance Expr (Appl a) a where
  eval (Appl x y) = eval x (eval y)

data MkPair a b = forall x y . (Expr x a, Expr y b) => MkPair x y
instance Expr (MkPair a b) (a,b) where
  eval (MkPair a b) = (eval a, eval b)
----

Best,
	Dylan Thurston