Implementing the Mini-Language Arith in Elm

The Grammar of Arith

   S = if iszero succ 0 then succ succ succ 0 else false
> input = "if iszero succ 0 then succ succ succ 0 else false"> parse input
Ok (IfExpr (IsZero (Succ Zero)) (Succ (Succ (Succ Zero))) F)
: Result (List Parser.DeadEnd) Term
> ast = IfExpr (IsZero (Succ Zero)) (Succ (Succ (Succ Zero))) F> stringValue ast
"if iszero succ 0 then succ succ succ 0 else False" : String
> parse "if 0 then pred else succ"
Err [...]
: Result (List Parser.DeadEnd) Term

The AST

The Type of a Term

type Term
= T
| F
| Zero
| Succ Term
| Pred Term
| IsZero Term
| IfExpr Term Term Term

A Parser

parse : String -> Result (List Parser.DeadEnd) Term
parse str = Parser.run term str
term : Parser Term
term =
succeed identity
|. spaces
|= oneOf
[ true
, false
, zero
, succ
, pred
, iszero
, lazy (\_ -> ifExpr)
]
true : Parser Term
true =
succeed T
|. symbol "true"
succ : Parser Term
succ =
symbol "succ"
|> andThen (\_ -> term)
|> map (\t -> Succ t)
andThen : (a -> Parser b) -> Parser a -> Parser b
ifExpr : Parser Term
ifExpr =
succeed IfExpr
|. symbol "if"
|= term
|. spaces
|. symbol "then"
|= term
|. spaces
|. symbol "else"
|= term

An Evaluator

type Value
= Numeric Int
| Boolean Bool
| Error String
input = "if succ 0 then 0 else succ 0"
ast = IfExpr (Succ Zero) Zero (Succ Zero)
> eval ast
Error ("If-then-else: expecting boolean value") : Value
eval : Term -> Value
eval t =
case t of
Zero ->
Numeric 0
Succ a ->
case eval a of
Numeric b ->
Numeric (b + 1)
_ ->
Error "succ expects numeric value"
Pred a ->
case eval a of
Numeric b ->
if b == 0 then
Numeric 0
else
Numeric (b - 1)
_ ->
Error "pred expects numeric value"
F ->
Boolean False
T ->
Boolean True
IsZero a ->
case eval a of
Numeric b ->
Boolean (b == 0)
_ ->
Error "iszero expects a numeric value"
IfExpr a b c ->
case eval a of
Boolean v ->
case v of
True ->
eval b
False ->
eval c
_ ->
Error "If-then-else: expecting boolean value"

Comments

  1. The reason that the eval function can produce values of type Error String is that the language arith is not typed. Thus sentences such as “if succ iszero succ 0 then 0 else succ 0” can be compiled into a valid AST but cannot be evaluated without error.
  2. Julian Antonielli has some very nice slides describing a type checker for arith. His implementation is in Haskell. I plan to give it a try in Elm. Among the references at the end of Julian’s slides is a link to a YouTube video on “typechecking from scratch.”
  3. A good exercise is to rig up a function to compute the depth of the AST produced by parse. Another good exercise is to work out a definition of stringValue. You will find code for both of these in the GitHub repo for the Elm implementation of arith.

Definition of depth

  1. The depth of a term like true, false, 0 is 1.
  2. The depth of the term succ t is 1 + depth t, and similarly for pred and iszero.
  3. The depth of if a then b else c is 1 + max(depth a, depth b, depth c).

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store