Type-checking the Mini-Language Arith in Elm

Image for post
Image for post

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:

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

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

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:

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

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:

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

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

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

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

And here is the code for checking types:

Written by

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

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