Types and Typeclasses

Types enable humans and computers to reason about our programs. The halting problem is not a problem, because types can prove code must terminate. They can do even more and prove a program terminates with the right answer: for example, we can prove a given function correctly sorts a list.

Types can be lightweight. Indeed, they can be invisible. A compiler can use type inference to type-check a program completely free of any type annotations. However, it’s good to throw a few type annotations in the source, as they are a form of documentation that is especially reliable because the compiler ensures they stay in sync with the code.

Therefore, we ought to add types to our language. We mimic Haskell, with at least one deliberate difference: let is not generalized. We only generalize top-level definitions.

Typically

We shamelessly lift code from Mark P. Jones, Typing Haskell in Haskell. Our version is simpler because we lack support for mutual recursion and pattern matching.

Since we’re using the Scott encoding, from a data type declaration:

data Adt a b c = Foo a | Bar | Baz b c

we generate types for the data constructors:

("Foo", a -> Adt a b c)
("Bar", Adt a b c)
("Baz", b -> c -> Adt a b c)

Along with:

("|Foo|Bar|Baz", Adt a b c -> (a -> x) -> x -> (b -> c -> x) -> x)

which represents the type of case in:

case x of
  Foo a -> f a
  Bar -> g
  Baz b c -> h b c

The case keyword is replaced with the identity combinator during compilation:

I x (\a -> f a) (\ -> g) (\b c -> h b c)

Our type checker is missing several features, such as kind checking and rejecting duplicate definitions.

▶ Toggle Source

Classy

In the worst case, types are a burden, and force us to wrestle with the compiler. We twist our code this way and that, and add eye-watering type annotations until it finally compiles.

In contrast, well-designed types do more with less. Haskell’s type system not only enables easy type inference, but also enables typeclasses, a syntax sugar for principled overloading. By bestowing Prolog-like powers to the type checker, the compiler can predictably generate tedious code so humans can ignore irrelevant details.

Again, Typing Haskell in Haskell provides some background. Since we’re generating code as well as checking types, we also need techniques described in John Peterson and Mark Jones, Implementing Type Classes.

We choose the dictionary approach. A dictionary is a record of functions that is implicitly passed around. For example, if we infer the function foo has type:

foo :: Eq a => Show a => a -> String

then we may imagine our compiler turning fat arrows into thin arrows:

foo :: Eq a -> Show a -> a -> String

Our compiler then seeks dictionaries that fit the two new arguments of types Eq a and Show a, and inserts them into the syntax tree.

With this in mind, we modify the type inference functions so they return a syntax tree along with its type. Most of the time, they just return the input syntax tree unchanged, but if type constraints are inferred, then we create a Proof node for each constraint, and apply the syntax tree to these new nodes.

In our example, if t is the syntax tree of foo, then our type inference function would change it to A (A t (Proof "Eq a")) (Proof "Show a"). Here, we’re using strings to represent constraints for legibiity; in reality, we have a dedicated data type to hold constraints, though later on, we do in fact turn them into strings when generating variable names.

We call such a node a Proof because it’s a cute short word, and we think of a dictionary as proof that a certain constraint is satisfied. Peterson and Jones instead write "Placeholder".

Typeclass methods are included in the above. For example, while processing the expression:

(==) (2+2) 5

we infer that (==) has type Eq a => a -> a -> Bool, so we modify the syntax tree to:

(select-==) (Proof "Eq a") (2+2) 5

After type unification, we learn a is Int:

(select-==) (Proof "Eq Int") (2+2) 5

The next phase constructs records of functions to be used as proofs. We loosely follow Typing Haskell in Haskell once more, and search for instances that match a given constraint. A matching instance may create more constraints.

We walk through how our compiler finds a proof for:

Proof "Eq [[Int]]"

Our compiler finds an instance match: Eq a => Eq [a], so it rewrites the above as:

(V "Eq [a]") (Proof "Eq [Int]")

The "Eq [a]" string is taken verbatim from an instance declaration, while the "Eq [Int]" is the result of a type substitution found during unification on "Eq a".

Our compiler recursively seeks an instance match for the new Proof. Again it finds Eq a => Eq [a], so the next rewrite yields:

(V "Eq [a]") ((V "Eq [a]") (Proof "Eq Int"))

and again it recursively looks for an instance match. It finds the Eq Int instance, and we have:

(V "Eq [a]") ((V "Eq [a]") (V "Eq Int"))

This works, because our compiler has previously processed all class and instance declarations, and has prepared the symbol table to map "Eq Int" to a record of functions for integer equality testing, and "Eq [a]" to a function that takes a "Eq a" and returns a record of functions for equality testing on lists of type a.

Overloading complicates our handling of recursion. For example, each occurrence of (==) in:

instance Eq (Int, String) where (x, y) == (z, w) = x == z && y == w

refers to a distinct function, so introducing the Y combinator here is incorrect. We should only look for recursion after type inference expands them to select-== Dict-Eq-Int and select-== Dict-Eq-String, and we look for recursion at the level of dictionaries.

Among the many deficiencies in our compiler: we lack support for class contexts; our code allows instances to stomp over one another; our algorithm for finding proofs may not terminate.

Without garbage collection, this compiler requires unreasonable amounts of memory.

▶ Toggle Source

Barely

Our compilers are becoming noticeably slower. The main culprit is the type unification algorithm we copied from the paper. It is elegant and simple, but also grossly inefficient. The pain is exacerbated by long string constants, which expand to a chain of cons calls before type checking.

Fortunately, we can easily defer expansion so it takes place after type checking. This alleviates enough of the suffering that we’ll leave improving unification for another time.

This change is a good opportunity to tidy up. In particular, we eliminate the murky handling of the R data constructor: before type checking, it represented integer constants, while after type checking, its field was to be passed verbatim to the next phase. Now, data types clear up the picture.

We immediately take advantage of the neater code and add a few rewrite rules to cut down the number of combinators.

To make this incarnation of our compiler more substantial, we knuckle down and implement a Map based on Adams trees. Again, we mostly copy code from a paper. The running time improves slightly after replacing the association list used in the last compilation step with Map.

We choose the BB-2.5 variant, based on the benchmarks in the paper, though it is troubling that Data.Map chose BB-3 trees.

We also move the assembler from C to Haskell, that is, our compiler now outputs bare machine code rather than ION assembly.

▶ Toggle Source


Ben Lynn blynn@cs.stanford.edu 💡