Type inference for Haskell, part 19

Posted on January 20, 2019

This is part 19 of the series on type inference for Haskell.

(THIH Section 7.4, Context Reduction)

After inferring the type for a function, there may be some predicates. Cleaning those up is the job of context reduction. It converts the predicates to head-normal form (HNF) and removes redundant predicates with the entail function. We saw those details one and two posts ago, respectively.

Those two steps are the job of the reduce function:

It converts all the predicates to HNF (which, remember, might fail if it needs an instance that doesn’t exist) then simplifies the resulting list of predicates (qs).

The simplify function is what calls entail. It checks each predicate in the list and removes it if it is entailed by all the other predicates still in the list. This sounds inefficient until you realize that there are rarely more than a small handful of predicates.

It’s time to look at an example. Say typing a function resulted in the predicates Eq (a, a), Ord a.

The reduce function would first convert these to HNF. Since there is an Eq instance for tuples, this succeeds. Ord a is already in HNF, so it doesn’t need any conversion. toHnfs returns a new list of predicates, which now looks like Eq a, Eq a, Ord a.

The second step is to simplify those predicates. First we see that the first Eq a is entailed by Eq a, Ord a because it appears in that list, so it gets dropped. Then, we see that the other Eq a is entailed by Ord a since Eq is a superclass of Ord. At the end, we are left with just Ord a as the only predicate.

It is worth reiterating that context reduction can only fail due to a missing instance (when there is a predicate that wants a class for a type that doesn’t have that class).

You would think we would be done processing the list of predicates at this point! Amazingly, there are still more details left to deal with. I’ll get to those in the following posts.