Haskell GADT typesafe Evaluator: Constant term for more than one type.
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.
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
上一篇: 类型族实例中的约束