haskell GADTs constructor

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.

Answer 1

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.