Writing a simple evaluator and type-checker inĀ Haskell

By Boro Sitnikovski

This tutorial serves as a very short and quick summary of the first few chapters of TAPL. Huge thanks to the ##dependent@freenode community (pgiarrusso, lyxia, mietek, …) for clearing all my questions, which provided a good sense of the design of such systems.

1. Untyped simple language

Our syntax, per BNF is defined as follows:

 <term> ::= <bool> | <num> | If <bool> Then <expr> Else <expr> | <arith> <bool> ::= T | F | IsZero <num> <num> ::= O <arith> ::= Succ <num> | Pred <num> 

For simplicity, we merge all them together in a single Term.

 data Term = T | F | O | IfThenElse Term Term Term | Succ Term | Pred Term | IsZero Term deriving (Show, Eq) 

1.2. Inference rules (evaluator)

The semantics we use here are based on so called small-step style, which state how a term is rewritten to a specific value, written t \to v. In contrast, big-step style states how a specific term evaluates to a final value, written t \Downarrow v.

Evaluation of a term is just pattern matching the inference rules. Given a term, it should produce a term:

 eval :: Term -> Term 

The list of inference rules:

Name Rule
E-IfTrue \text{If T Then } t_2 \text{ Else } t_3 \to t_2
E-IfFalse \text{If F Then } t_2 \text{ Else } t_3 \to t_3
E-If \frac{t_1 \to t'}{\text{If }t_1 \text{ Then } t_2 \text{ Else } t_3 \to \text{If }t' \text{ Then } t_2 \text{ Else } t_3}
E-Succ \frac{t_1 \to t'}{\text{Succ }t_1 \to \text{ Succ } t'}
E-PredZero \text{Pred O} \to \text{O}
E-PredSucc \text{Pred(Succ } k \text {)} \to k
E-Pred \frac{t_1 \to t'}{\text{Pred }t_1 \to \text{ Pred } t'}
E-IszeroZero \text{IsZero O} \to \text{T}
E-IszeroSucc \text{IsZero(Succ } k \text {)} \to \text{F}
E-IsZero \frac{t_1 \to t'}{\text{IsZero }t_1 \to \text{ IsZero } t'}

As an example, the rule E-IfTrue written using big-step semantics would be \frac{t_1 \Downarrow T, t2 \Downarrow v}{\text{If }T \text{ Then } t_2 \text{ Else } t_3 \Downarrow t_2}.

Given the rules, by pattern matching them we will reduce terms. Implementation in Haskell is mostly “copy-paste” according to the rules:

 eval (IfThenElse T t2 t3) = t2 eval (IfThenElse F t2 t3) = t3 eval (IfThenElse t1 t2 t3) = let t' = eval t1 in IfThenElse t' t2 t3 eval (Succ t1) = let t' = eval t1 in Succ t' eval (Pred O) = O eval (Pred (Succ k)) = k eval (Pred t1) = let t' = eval t1 in Pred t' eval (IsZero O) = T eval (IsZero (Succ t)) = F eval (IsZero t1) = let t' = eval t1 in IsZero t' eval _ = error "No rule applies" 

1.3. Conclusion

As an example, evaluating the following:

 Main> eval $ Pred $ Succ $ Pred O Pred O 

Corresponds to the following inference rules:

 ----------- E-PredZero pred O -> O ----------------------- E-Succ succ (pred O) -> succ O ------------------------------------- E-Pred pred (succ (pred O)) -> pred (succ O) 

However, if we do:

 Main> eval $ IfThenElse O O O *** Exception: No rule applies 

It’s type-checking time!

2. Typed simple language

In addition to the previous syntax, we create a new one for types, so per BNF it’s defined as follows:

 <type> ::= Bool | Nat 

In Haskell:

 data Type = TBool | TNat 

2.2. Inference rules (type)

Getting a type of a term expects a term, and either returns an error or the type derived:

 typeOf :: Term -> Either String Type 

Next step is to specify the typing rules.

Name Rule
T-True \text{T : TBool}
T-False \text{F : TBool}
T-Zero \text{O : TNat}
T-If \frac{t_1\text{ : Bool}, t_2\text{ : }T, t_3\text{ : }T}{\text{If }t_1 \text{ Then } t_2 \text{ Else } t_3\text{ : }T}
T-Succ \frac{t\text{ : TNat }}{\text{Succ } t \text{ : TNat}}
T-Pred \frac{t\text{ : TNat }}{\text{Pred } t \text{ : TNat}}
T-IsZero \frac{t\text{ : TNat }}{\text{IsZero } t \text{ : TBool}}

Code in Haskell:

 typeOf T = Right TBool typeOf F = Right TBool typeOf O = Right TNat typeOf (IfThenElse t1 t2 t3) = case typeOf t1 of Right TBool -> let t2' = typeOf t2 t3' = typeOf t3 in if t2' == t3' then t2' else Left "Types mismatch" _ -> Left "Unsupported type for IfThenElse" typeOf (Succ k) = case typeOf k of Right TNat -> Right TNat _ -> Left "Unsupported type for Succ" typeOf (Pred k) = case typeOf k of Right TNat -> Right TNat _ -> Left "Unsupported type for Pred" typeOf (IsZero k) = case typeOf k of Right TNat -> Right TBool _ -> Left "Unsupported type for IsZero" 

2.3. Conclusion

Going back to the previous example, we can now “safely” evaluate (by type-checking first), depending on type-check results:

 Main> typeOf $ IfThenElse O O O Left "Unsupported type for IfThenElse" Main> typeOf $ IfThenElse T O (Succ O) Right TNat Main> typeOf $ IfThenElse F O (Succ O) Right TNat Main> eval $ IfThenElse T O (Succ O) O Main> eval $ IfThenElse F O (Succ O) Succ O 

3. Environments

Our neat language supports evaluation and type checking, but does not allow for defining constants. To do that, we will need kind of an environment which will hold information about constants.

 type TyEnv = [(String, Type)] -- Type env type TeEnv = [(String, Term)] -- Term env 

We also extend our data type to contain TVar for defining variables, and meanwhile also introduce the Let ... in ... syntax:

 data Term = ... | TVar String | Let String Term Term 

Here are the rules for variables:

Name Rule
Add binding \frac{\Gamma, a \text{ : T}}{\Gamma \vdash a \text{ : T}}
Retrieve binding \frac{a \text{ : T} \in \Gamma}{\Gamma \vdash a \text{ : T}}

Haskell definitions:

 addType :: String -> Type -> TyEnv -> TyEnv addType varname b env = (varname, b) : env getTypeFromEnv :: TyEnv -> String -> Maybe Type getTypeFromEnv [] _ = Nothing getTypeFromEnv ((varname', b) : env) varname = if varname' == varname then Just b else getTypeFromEnv env varname 

Analogously for terms:

 addTerm :: String -> Term -> TeEnv -> TeEnv addTerm varname b env = (varname, b) : env getTermFromEnv :: TeEnv -> String -> Maybe Term getTermFromEnv [] _ = Nothing getTermFromEnv ((varname', b) : env) varname = if varname' == varname then Just b else getTermFromEnv env varname 

3.1. Inference rules (evaluator)

At this point we stop giving mathematical inference rules, but it’s a good homework if you want to do it 🙂

eval' is exactly the same as eval, with the following additions: 1. New parameter (the environment) to support retrieval of values for constants

2. Pattern matching for the new Let ... in ... syntax