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" |> evalResult
Just (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" |> evalResult
Just (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 ift 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 0does 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 0
2
> succ succ false
Not typable
> foo bar baz
Parse 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