haskell GADTs constructor

0
votes

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.

2
haskellgadt
The non-GADT declaration of Expr has no parameter (in contrast to the GADT one), is that on purpose? – huon
@dbaupp I'd say so, since that was what was given to me for the exercise. – SNpn
V is not a type variable (in the first definition), since it's uppercase it must refer to a specific type, right? – Peter
@Peter oh sorry, its lower case – SNpn
Shouldn't your first code be 'data Expr v = Condition v | And (Expr v) (Expr v) | Or (Expr v) (Expr v)'? – gfour

2 Answers

3
votes

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.

0
votes

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