Haskell GADT typesafe Evaluator: Constant term for more than one type.

Question

I've been working through some Haskell Tutorials introducing GADTs using the typesafe evaluator examples. A lot of the evaluators operate on both Boolean and Int type. So the GADT type for an evaluator which has the functions (Constant Integer, Constant Boolean, Add, Multiply, and Check Equality) has the form:

data Expr a where
  I   :: Int  -> Expr Int
  B   :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int
  Mul :: Expr Int -> Expr Int -> Expr Int
  Eq  :: Expr Int -> Expr Int -> Expr Bool

I'm mostly fine with this example, but I would like to be able to define general constant types to be either Int or Bool types, rather than having separate entries for Int and Bool. Is this possible.

This seems to work if I just use a Type variable instead of Int or Bool in my GADT.

This makes the above example:

data Expr a where
  Con :: t -> Expr t
  Add :: Expr Int -> Expr Int -> Expr Int
  Mul :: Expr Int -> Expr Int -> Expr Int
  Eq  :: Expr Int -> Expr Int -> Expr Bool

By then the Constant type is not restricted enough as I can then have a Constant List input, or a constant String/Float, where I ONLY want Constants to be Int or Bool.

I've thought about using TypeClasses (I think) to solve this as this seems to be able to limit the "domain" of the type variable such as using the "Ord" Class would limit the possible types that the typevariable t could take in the line

Con :: Ord t => t -> Term t

Unfortunately I'm not sure how to write my own class to do this to restrict the type variable to be just Boolean or Integer. Is this even the right track?

Thanks.

Random Dev Random Dev · Accepted Answer · 2016-05-21T06:13:26

the idea of using a constraint like you asked for can be implemented like this:

class Constant a

instance Constant Int
instance Constant Bool

data Expr a where
  C :: Constant a => a -> Expr a
  Add :: Expr Int -> Expr Int -> Expr Int
  Mul :: Expr Int -> Expr Int -> Expr Int
  Eq  :: Expr Int -> Expr Int -> Expr Bool

which would work well I guess

eval :: Expr a -> a
eval (C a) = a
eval (Add a b) = eval a + eval b
eval (Mul a b) = eval a * eval b
eval (Eq a b) = eval a == eval b

On the other hand you can use another GADT if you ever want to match on the constant itself:

module SO where

data Const a where
  ConstB :: Bool -> Const Bool
  ConstI :: Int -> Const Int

data Expr a where
  C :: Const a -> Expr a
  Add :: Expr Int -> Expr Int -> Expr Int
  Mul :: Expr Int -> Expr Int -> Expr Int
  Eq  :: Expr Int -> Expr Int -> Expr Bool

usage

λ> C (ConstB False)
C (ConstB False) :: Expr Bool
λ> C (ConstI 5)
C (ConstI 5) :: Expr Int

Haskell GADT typesafe Evaluator: Constant term for more than one type.

1 Answers

usage