type signatures with existentially quantified data constructors

[Levent Erkok]

How about:

===================================================================
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)
 
eval :: Expr a -> a
eval (Haskell x) = x
eval (If x y z)  = if eval x then eval y else eval z
eval (Appl x y) = (eval x) (eval y)
eval (MkPair x y f) = f (eval x) (eval y)
 
mkpair x y = MkPair x y (\x y -> (x, y))
===================================================================

Then, you can say:

Main> eval (mkpair (Haskell 3.12) (Haskell True))
(3.12,True)

-Levent.


On Thursday 16 August 2001 05:11 am, Avi Pfeffer wrote:
> Hi all,
>
> I'm trying to write an interpreter for a language embedded in Haskell,
> that "inherits" Haskell types and values.  So I create a type Expr a, to
> represent expressions of type a, and an evaluator that takes an Expr a
> and produces an a.  (To keep things simple, let's assume there are no
> variables.)   I start with
>
> data Expr a = Haskell a
>
>             | If (Expr Bool) (Expr a) (Expr a)
>
> eval :: Expr a -> a
> eval (Haskell x) = x
> eval (If x y z)  = if eval x then eval y else eval z
>
> Next, applications.  To correctly type an application expression, I need
> to introduce an existentially quantified type variable:
>
> data Expr a = ... | forall b . Appl (Expr (b->a)) (Expr a)
>
> eval (Appl x y) = (eval x) (eval y)
>
> 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
>
> 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)
>
> GHC produces the error message
>
>     Cannot unify the type-signature variable `a'
>         with the type `(t, t1)'
>         Expected type: a
>         Inferred type: (t, t1)
>     in the definition of function `eval': (eval x, eval y)
>
> I have tried various ways of adding type annotations, but I can't seem to
> make it work.  The problem seems to be the combination of class constraint
> with existential variables.  How can I tell the compiler that it should in
> fact unify a with (t,t1) here?  Or am I misunderstanding something, and
> there is a reason it can't?  Perhaps there's a way of typing MkPair
> without introducing the Pair class?  Or is there a completely different
> approach to my problem?  All suggestions welcome.
>
> --Avi
>
>
>
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell