Type inference for Haskell, part 18

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

Today we’re going to take a look at another detail required by Haskell’s language specification. I believe (but don’t quote me on this!) that this detail is necessary to prevent ambiguity in what a given program does.

(THIH Section 7.4, Context Reduction)

Some types are in head-normal form, some are not. Haskell requires that type mentioned in a predicate (called the “class argument”¹) be in head-normal form, so we need a way to ensure that a type is in head-normal form when using it in type classes.

So what it is? It’s where the leftmost part of the type is a type variable. For example the type a is in head-normal form, but the type Maybe a is not. Though it is unusual to see, a Int is also considered to be in head-normal form. Here’s an example of code that uses it:

data SomeData a = SomeData (a Int)

showData :: Show (a Int) => SomeData a -> String
showData (SomeData x) = "SomeData " ++ show x

Another way to put this is that a type is in head-normal form (HNF) if and only if it is a type variable, possibly applied to some other types. It doesn’t matter what those other types are. Here’s that rule expressed as code:

inHnf       :: Pred -> Bool
inHnf (IsIn c t) = hnf t
 where hnf (TVar v)  = True
       hnf (TCon tc) = False
       hnf (TAp t _) = hnf t

Note how it just cares about the left half of type applications.

From here on out I’ll abbreviate head-normal form as HNF.

When typing a function, we might end up with a predicate like (Show [a]). That’s a problem since [a] isn’t in HNF (the type [a] expands to TAp (TCon "[]") (TVar "a")). This is a function where that might happen:

f a b = show [a, b]

We can’t give f the type (Show [a]) => a -> a -> String because the type in the predicate isn’t in HNF. What can we do about this? Though we can’t include the predicate (Show [a]), we are allowed to add other predicates to the type. Haskell will end up giving that function the type (Show a) => a -> a -> String. At this point, it’s worth asking two questions: why is that valid to do that, and how does Haskell figure out that it should use that type?

When a predicate like Show [a] that isn’t in HNF is encountered, there needs to be some way to convert it to other predicates (in this case, Show a). In order to be allowed to do that there needs to be an instance of Show for lists of things. If there wasn’t that instance, this conversion would fail. The type for f mentioned above is only valid because of the existance of an instance declaration.

To convert a type in a predicate to HNF, we need the class environment as well as that predicate. The function will either return some predicates or fail if it cannot find an instance declaration that it needs. Note that by the end, we might actually end up with multiple predicates.

Imagine we had the predicate (Eq (a, b)). The type (a, b) isn’t in HNF, so we need to look for some instance of the class Eq that can be used for types like (a, b). We’re in luck because such an instance does exist. That instance is declared with (Eq a, Eq b) => Eq (a, b). That means if a is an instance of Eq and b is an instance of Eq, then (a, b) is also an instance of Eq. We can follow the logic backwards. Since we need Eq (a, b), if we require Eq a and Eq b, then we know that we’ll also get Eq (a, b). In a sense, we “trade in” the Eq (a, b) predicate for the two predicates Eq a, Eq b. The types a and b are both in HNF, so the process stops there. If they hadn’t been, we would have recursively converted those types to HNF as well.

This logic is implemented by the toHnf function:

toHnf :: Monad m => ClassEnv -> Pred -> m [Pred]
toHnf ce p | inHnf p   = return [p]
           | otherwise = case byInst ce p of
                           Nothing -> fail "context reduction"
                           Just ps -> toHnfs ce ps

toHnfs      :: Monad m => ClassEnv -> [Pred] -> m [Pred]
toHnfs ce ps = do
  pss <- mapM (toHnf ce) ps
  return (concat pss)

There are a few things to note about the toHnf function:

• It returns the input predicate if it is already in HNF.
• It is recursively called when it finds new predicates (the predicates on the matching instance), since those might not be in HNF either.
• It is possible for it to return an empty set of predicates. For example, if given the predicate (Show Int), it would find the Show instance for Int. That instance has no more predicates, so the result is just an empty list.
• It fails if there is no matching instance for the predicate, meaning it is not possible for it to hold true. For example, it would fail if you gave it the predicate (Num [a]) since there is no Num instance of a list of things. This happens when byInst returns Nothing.
• It might return duplicates of some predicates, but that’s OK because they’ll be cleaned up shortly after (in code that we haven’t seen yet). For example, (Eq (a, a)) would get converted into [Eq a, Eq a].

Like the entail function from the previous post, toHnf is also used to process the predicates when typing a function is done. How these get used is a subject for the next post.