# 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 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 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