Type inference for Haskell, part 17

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

The previous post defined the data structures we’ll use when working with type classes. Today, we’re going to be looking at a behavior of Haskell where it “cleans up” the set of predicates attached to a binding. The resulting types are intuative enough that you might not have even realized that this process was happening.

(THIH Section 7.3, Entailment)

The feature is called entailment (at least, it’s called that by Typing Haskell in Haskell). It’s easiest to show what it is with some examples.

When you have a function with a type signature like

(Show a) => String -> Maybe a -> String

The (Show a) part is a predicate. It says that the type a must have an implementation of the Show class. You can turn this into a question: Does a implement Show? If so, that predicate holds true.

Consider another type

(Eq a, Ord a) => a -> a -> Bool

This is actually equivalent to writing

(Ord a) => a -> a -> Bool

Why can we leave off the Eq a? That’s because Eq is a superclass of Ord, meaning that if a is an instance of Ord, then it definitely is also an instance of Eq. So we don’t have to manually write down the fact that we want it to also be an instance of Eq - we get that for free.

That’s the first of the two related things that entailment handles.

Now look at this type signature:

foo :: (Show Int) => Int -> Int -> String
foo a b = show (max a b)

Writing Show Int isn’t useful here because we already know that Int implements Show. If it didn’t, the show call in the function body would fail to type check. Either way, we aren’t helped by writing Show Int. It’s better to leave it out of the function’s type.

This is the second thing that entailment looks at.

When inferring the type for a function, we might get predicates like those in the examples above. The entailment algorithm is used to clean them up. (It is also used for a few other things that we’ll come to in another post.)

I still haven’t told you what the function actually does. It takes in a predicate (like (Eq a)) that we want to evaluate and a list of other predicates that we are assuming hold true (like (Ord a)). It also takes information about what classes exist and what instances they have. It returns true if, given the other predicates, we know that the predicate holds true. It has no error cases.

Here’s how the logic works for that. If our predicate appears in the list of other predicates, then it trivially holds true if they all hold true (that’s like asking, given that A is true, is A true?). It also holds true if it appears in any of the superclasses of the other predicates (that’s what handles our (Eq a, Ord a) example). Finally, the predicate also holds true if there is an instance of the class for that type (the (Show Int) case) where any predicates on that instance also hold true (with a recursive call to entail).

Show Int doesn’t have any predicates on the instance. For an example that does have some, consider an instance declaration like

instance (Foo a) => Foo [a] where

And a predicate like (Foo [Bar]). When checking that predicate, we’ll first find the instance above. Foo [a] matches with Foo [Bar], so the instance can be used. From there, the (Foo a) predicate on the instance means that we will next have to check if (Foo Bar) holds true. If there is an instance of class Foo for the type Bar, then we’ll recursively check its predicates, too.

Here’s the actual entail function from THIH:

entail :: ClassEnv -> [Pred] -> Pred -> Bool
entail ce ps p =
  any (p `elem`) (map (bySuper ce) ps) ||
  case byInst ce p of
    Nothing -> False
    Just qs -> all (entail ce ps) qs

Note that it ORs two cases together. The first case handles the situation where the predicate is either directly in the list of predicates we are assuming hold true, or it is a superclass of at least one of them. That would return true for Eq a if Ord a was in the list of given predicates. The second case is for the situation where the class has an instance for the type mentioned in the predicate. Note that this case involves a recursive call to entail. That call checks the predicates (if there are any) on that particular instance of the class.

Note that bySuper includes the predicate itself, not just superclasses.

bySuper :: ClassEnv -> Pred -> [Pred]
bySuper ce p@(IsIn i t) =
    p : concat [ bySuper ce (IsIn i' t) | i' <- super ce i ]

And here is byInst. It attempts to find an instance of the class mentioned in the predicate that works for the type mentioned in the predicate. It uses a function called matchPred to determine if a given instance of the class works for this particular case. msum takes the first Just _ value in the list, or returns Nothing if there are none.

byInst                   :: ClassEnv -> Pred -> Maybe [Pred]
byInst ce p@(IsIn i t)    = msum [ tryInst it | it <- insts ce i ]
  where tryInst (ps :=> h) = do
          u <- matchPred h p
          Just (map (apply u) ps)

The matchPred first checks to make sure the classes being talked about are the same, then checks if the types in the predicate “match.” If you look at the code of match, you are probably reminded of the mgu function. match is like a one-sided version of mgu. Instead of finding a substitution that can be applied to both types to make them the same, it finds a substitution that can be applied to the left type that can turn it into the right type.

This allows the right type to be more specific than the left type, but the left type cannot be more specific than the right. This would mean that we could match [a] with [Bar] to determine that an instance of a class on [a] can be used for the type [Bar]. The match function is how you tell if the particular instance you are looking at can be used for the type you have.

matchPred :: Pred -> Pred -> Maybe Subst
matchPred  = lift match

lift m (IsIn i t) (IsIn i' t')
         | i == i'   = m t t'
         | otherwise = fail "classes differ"

match :: Monad m => Type -> Type -> m Subst
match (TAp l r) (TAp l' r')              = do
    sl <- match l l'
    sr <- match r r'
    merge sl sr
match (TVar u)   t | kind u == kind t    =
    return (u +-> t)
match (TCon tc1) (TCon tc2) | tc1 == tc2 =
    return nullSubst
match t1 t2                              =
    fail "types do not match"

+-> is that infix function defined a long while ago that creates a single-element substitution.

Also notice that matching is using merge to combine substitutions instead of composing them. merge is interesting because it might fail. Let’s look at why.

For example:

match `(a, b)` `(Int, String)`

works and returns the substitution {a: Int, b: String}. However, in this example:

match `(a, a)` `(Int, String)`

it would fail because we’d have to substitute a for Int on one side and for String on the other. This is where merge detects an error because the two substitutions don’t agree.

merge      :: Monad m => Subst -> Subst -> m Subst
merge s1 s2 = if agree then return (s1++s2) else fail "merge fails"
 where agree = all (\v -> apply s1 (TVar v) == apply s2 (TVar v))
                   (map fst s1 `intersect` map fst s2)

That’s it for the logic behind entailment. We won’t see where entail is called for another two posts, and it will be even longer before finding out where this hooks back up to the type inference algorithm. The short version of the story is that this is one of the steps that happens when processing the predicates that are going to be saved for the type of a binding.

To unwind the stack of where we currently are:

• merge combines two substitutions, assuming they agree.
• match checks that you can change one type into the other with a substitution.
• matchPred both runs match on the types and verifies that the predicates are talking about the same class.
• That allows byInst to find an instance of a given class that matches the type mentioned in the predicate.
• If byInst returns a type, that’s used by entail to check if a predicate like (Show Int) is known to be true thanks to an instance declaration.

And all of this is in the service of making nice type signatures! (And other things, but those are for another day.)