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 bar
:
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 x
1. 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
, but 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 thebar
function, this would be(Show tx)
.fs
is 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 thebar
function, this would includex
(which has typetx
), so the setfs
includestx
.
This expression relies on a few functions:
tv
is the function defined many posts ago to find free type variables.all
andelem
are built-in functions.partition
is a function fromData.List
that 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.↩