Type-checking the Mini-Language Arith in Elm

In a previous post, I discussed an Elm implementation of the mini-language Arith discussed in Benjamin Peirce’s book Types and Programming Languages (TAPL). The implementation provides a parser and an eval function, so we can do things like this:

`> parse "succ succ 0"Ok (Succ (Succ Zero))> parse "succ succ 0" |> evalResultJust (Numeric 2) `

As it stands now, the expression `succ succ false` is perfectly “grammatical” and is accepted by the parser:

`> parse "succ succ false"Ok (Succ (Succ F))`

But of course, this expression makes no sense, and when we evaluate it, we get an error:

`> parse "succ succ false" |> evalResultJust (Error ("succ expects numeric value"))`

Type systems

A type system is designed to detect such nonsense before it ever gets to the eval function. We recount here the type system for `Arith` which is discussed in TAPL, chapter 8. It will have just two types, one for values like `true` and `false`, another for numbers, like `0`, `succ 0`, `succ succ 0`, etc:

`                  type Type_ = Boolean | Nat`

In addition to types, we have typing rules. Here are some:

`(a) 0 : Nat      (b) true : Boolean     (c) false : Boolean`

These rules have the form `a:T`, where `a` is a value and `T` is a type, read as “a has type T.” The next set of rules look a bit different:

`      t : Nat              t : Nat                   t : Nat(d) ------------     (e) --------------    (f)  ------------------    succ t : Nat          pred t : Nat           iszero t : Boolean`

The first rule can be read as “if `t` is of type `Nat`, then so is `succ t`.” Our new rules have the form

`                          premise                      --------------                         conclusion`

If the premise holds, then so does the conclusion. There is just one more rule:

`                       s : Boolean    t : T    u : T               (g)   ----------------------------------                        if s then t else u : T`

This rule is reads “if `s` if of type `Boolean` and if`t` and `u` both have type `T`, then the expression `if s then t else u` has type `T`. The emphasis on “both” is important, as we will see in a moment.

Playing with the rules

Let’s play around with the rules to get a feel for how they work. Consider first the expression `0`. We look for a relevant rule, and find that (a) applies. It tells us that `0` has type `Nat`. Consider next the expression `succ 0`. Rule (d) applies, assuming that `0` is of type `Nat`. But `0`does have that type, by virtue of rule (a), which has no premise. Rules without premises are called axioms. Notice what has happened: in both the case of `0` and `succ 0`, we can use the rules to reach back to axioms. When this happens, we can assert that our value has a certain type. Why? Because we can then reverse the process, starting with axioms and ending with an assertion of the type of our value. Just like what we did in geometry class, when we studied Euclid. When this happens, we say that our value is well-typed, or typable.

Let’s try this on the expression `succ false`. When we cast about for applicable rules, we find none. So this expression has no type: it is not typable. One more example: `if true then 0 else false`. Is it typable? No. the only rule that might apply is (g). But since `0` and `false` have different types, (g) does not apply.

Implementation of a type-checker

Our Elm implementation of type checking for `Arith` is a function of the form

`              typeCheck : Term -> Maybe Type_`

Its definition is a straightforward application of the typing rules (see below). Using it, we can design a small program to parse user input, pass it to the type checker if it can be parsed, and then pass it to the eval function if it type checks. Here is a short session

`> succ succ 02> succ succ falseNot typable> foo bar bazParse error`

And here is the code for checking types:

`typeCheck : Term -> Maybe Type_typeCheck term =    case term of        T ->            Just Boolean        F ->            Just Boolean        Zero ->            Just Nat        Succ term_ ->            case typeCheck term_ of                Just Boolean ->                    Nothing                Just Nat ->                    Just Nat                Nothing ->                    Nothing        Pred term_ ->            case typeCheck term_ of                Just Boolean ->                    Nothing                Just Nat ->                    Just Nat                Nothing ->                    Nothing        IsZero term_ ->            case typeCheck term_ of                Just Boolean ->                    Nothing                Just Nat ->                    Just Boolean                Nothing ->                    Nothing        IfExpr t1 t2 t3 ->            case ( typeCheck t1, typeCheck t2, typeCheck t3 ) of                ( Just Boolean, Just Boolean, Just Boolean ) ->                    Just Boolean                ( Just Boolean, Just Nat, Just Nat ) ->                    Just Nat                _ ->                    Nothing`

--

--

More from James Carlson

jxxcarlson on elm slack, http://jxxcarlson.github.io