Type inference for Haskell, part 19
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 :: Monad m => ClassEnv -> [Pred] -> m [Pred] reduce ce ps = do qs <- toHnfs ce ps return (simplify ce qs)
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 (
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.
simplify :: ClassEnv -> [Pred] -> [Pred] simplify ce = loop  where loop rs  = rs loop rs (p:ps) | entail ce (rs++ps) p = loop rs ps | otherwise = loop (p:rs) ps
It’s time to look at an example. Say typing a function resulted in the predicates
Eq (a, a), Ord a.
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.