Type inference for Haskell, part 20
This is part 20 of the series on type inference for Haskell.
(THIH Section 11.5, From Types to Type Schemes)
The previous few posts dealt with some processing that gets applied to the predicates for a binding. The predicates were converted to head-normal form and then simplified to remove redundant predicates. Even after all that processing, there might be some issues with the predicates. Today we’re going to look at the first of the possible issues.
Consider this example, which has an outer binding
foo and an inner binding
When processing the inner binding
bar, we’ll discover a constraint that the type of
x (let’s call that
tx) needs to implement
Show. That’s because we’re calling
show x1. This need is expressed as the predicate
(Show tx). The type of
bar is then a little bit odd:
(Show tx) => String -> String
The predicate mentions the type variable
tx doesn’t appear anywhere in the type! It’s a bit silly to attach the predicate there. It would be much better to just defer that predicate to the outer binding for
foo. The type for
foo then looks like a good place for that predicate:
(Show tx) => tx -> String
With the predicate moved out there, the type of bar is then simply
String -> String.
When a predicate is moved out to the outer binding, we call that “deferring” the predicate. When the predicate stays on the current binding, we call that “retaining” the predicate.
The logic for this is actually just one line. If you look at the code from THIH, you’ll find this line in the
split function. The main job of the
split function is to split apart the deferred and the retained predicates, but it also does other stuff we’ll get to in another post.
That is one very dense line. What does it do?
To start with, you need to know what data is found in the variables it references:
ps'contains the list of predicates that were returned from context reduction. For the
barfunction, this would be
fsis the set of type variables in the assumptions. These are the type variables in the types of other variables that are currently in scope. For the
barfunction, this would include
x(which has type
tx), so the set
This expression relies on a few functions:
tvis the function defined many posts ago to find free type variables.
elemare built-in functions.
partitionis a function from
Data.Listthat splits a list into two based on some boolean function. Elements go in the first list when the function returns true, and in the second when it returns false.
This results in two variables.
ds is the deferred predicates and
rs is the retained predicates.
So, this line is saying, defer a predicate if all the type variables in that predicate are used in types from the outer scope. If not, assume the predicate belongs to this function.
It’s worth noting that the logic wasn’t written the other way around - checking if the type variables are used in the current binding. That is because there might be some predicates that have type variables that don’t reference either this binding’s type or any of the variables in scope. Those are potential ambiguities. I’ll look at those in the next post.
We haven’t yet covered how class constraints are actually found. The logic basically collects all the predicates from the all functions called in the expression.↩