Question
I have the following
data Expr = Condition v
| And Expr Expr
| Or Expr Expr
and I am asked to consider the follow untyped version in order to complete:
data Expr e where
I'm not sure what I'm suppose to write for the constructors. I tried the following:
data Expr e where
Condition :: v -> Expr v
And :: -- really not sure what to do with this one
OR :: Expr b -> (Expr b -> Expr a) -> Maybe Expr a -> Expr b
Also, since v
can be of any type ie int
, bool
etc is it possible just to call it the following (above) and declare the type of v
later?
data v = IntVat int
any help would be much appreciated :)
EDIT : changed the whole post to add a little bit more information and clarity (based on my understanding of the exercise).
Basically I need help figuring out the constructors for the GADTs given the data Expr = Condition v...etc
as reference.
Solution
If I were setting an assignment on GADTs using a basic expression language as the motivating example, here's the kind of answer I'd have in mind:
data Expr v where
Literal :: v -> Expr v
And :: Expr Bool -> Expr Bool -> Expr Bool
Or :: Expr Bool -> Expr Bool -> Expr Bool
-- and I'd probably add some things like this to
-- show why the type variable is useful
Equal :: Expr Int -> Expr Int -> Expr Bool
If :: Expr Bool -> Expr v -> Expr v -> Expr v
You can see why you might call this a "typed" expression: the instantiations of the type variables look like typing rules for a small language:
a : Bool b : Bool
-------------------------
And a b : Bool
a : Int b : Int
------------------------
Equal a b : Bool
etc.
OTHER TIPS
That sounds like an existential type to me. I must admit, I've never really used them, I only tried to understand them; anyway, maybe it's meant like this:
data Expr = forall v. Condition v
| And Expr Expr
| Or Expr Expr
Then you had a GADT like this (they generalize existentials, see here):
data Expr where
Condition :: v -> Expr
And :: Expr -> Expr -> Expr
Or :: Expr -> Expr -> Expr
Although, that wouldn't (as far as I understood the concept) make much sense, since you can't use v
for anything.
On the other hand, this would (I hope) make more sense (since there's a "condition"):
class Testable v where
test :: v -> Bool
data Expr where
Condition :: Testable v => v -> Expr
And :: Expr -> Expr -> Expr
Or :: Expr -> Expr -> Expr
then you could do, e.g.
eval :: Expr -> Bool
eval (Condition v) = test v
eval (And e1 e2) = (eval e1) && (eval e2)
eval (Or e1 e2) = (eval e1) || (eval e2)
which would work for different kinds of "conditions".
I didn't test this code, though, and, as I've said, I'm not really a professional about existentials. I hope my code is correct, but please tell me anyone, if you know better (or I'm totally wrong...)