When we were here last, I outlined how to write most of a type inferencer in haskell. I outlined a 5-step plan, and charted a course through the treacherous waters that stopped just shy of the fifth step: “Remove all the unification variables, replacing them with `TyVars`

and introducing `Foralls`

as appropriate to get into roughly the form described above.” And then I stopped! Let’s talk about how to go from an expression tree that is full of unification-fd’s `UVar`

s to one that explicitly introduces `Forall`

s in appropriate places.

What does it mean to say something is an appropriate place to introduce a `Forall`

? Remember that the point of these is to declare where the type machinery has to commit to a particular type being used consistently for a type variable. If we consider haskell’s map function `(a -> b) -> [a] -> [b]`

, once we commit to a particular type `a`

in either argument we’re locked in to using that type in both arguments. By the same token, using a type for `b`

in the result requires you to use the same type in the first argument, and vice versa. So we need to put both our `forall`

s at the start, yielding `forall a b. (a -> b) -> [a] -> [b]`

.

It’s not always necessary to put all the `forall`

s at the start. For example, consider a function that takes an argument of type `c`

and returns a function that takes an argument of type `d`

, ignores it, and returns the initial argument `c`

. This is probably `const`

and has type `c -> (d -> c)`

. In this case, as soon as you pass in the first argument, we’re committed to the final return type. We’re not committed to the type of the second argument, though! So we end up with `forall c. c -> (forall d. d -> c)`

. The value you get after picking a type for `c`

and applying a value of that type as the first argument has a `forall`

in it, which reflects the fact that you still get to choose what type will substitute in for the type variable `d`

.

Each of those examples reflects one of my priorities in cooking up a function for introducing `Forall`

s. The first is an example of making `Forall`

s as specific as necessary. The second is an example of making them as general as possible. Putting that a little more concretely, I want to put the `Forall`

for each logic variable as far down in the AST as possible while still only having one `Forall`

per logic variable.

In attempting to write a function to do that, I found it more difficult than I was anticipating, so I want to talk first about a simple thing based again on Diehl’s Write You A Haskell tutorial. In that tutorial – and in my type inference code – the only time you introduce the sort of flexibility that demands `Forall`

s is around let bindings. That means you can get a good result by structuring your `Forall`

introduction around those let bindings. I categorised expressions that were either at the top level of the program, or at the top of an expression bound within a let clause, as Top expressions. To introduce `Forall`

s to a Top expression, you find all of the type variables in that expression’s type and those of its non-Top sub-expressions, and make `Forall`

s for them. When looking at a non-Top expression, you’ve already introduced `Forall`

s for all its type variables and only need to rewrite the logic variables to type variables. You can see all the gory details in the commit with the code.

At this point I had working code, but I was distinctly dissatisfied with it. Can we allow more generality than that? I think we can!

The key thing is that for any expression, you need to introduce type variables for any logic variable that occurs in two or more child expressions. This gets you 90% of the way and covers pretty much all of the obviously useful functions. There are some funny functions, like `const :: a -> b -> a`

, where that doesn’t cut it. I repair those cases by also introducing type variables for any logic variable that occurs in the type of the expression I’m looking at right now. Here’s the diff with all the particulars.

This implementation seems to work, but it’s definitely not perfect. I know it leaves a certain amount of generality on the table because of the way it handles functions like `const`

. By introducing `Forall`

s for every variable in the type in one go, we lose the opportunity to put a `forall`

further down the type like in the `const :: forall c. c -> (forall d. d -> c)`

motivating example.

It might be possible to solve this by only introducing type variables when a logic variable appears in two sub-expressions of a `UTerm Ty`

, but that would create the potential for another problem. Consider an implementation `const x = \_ -> x`

. We know the expression `\_ -> x`

has type `forall d. d -> c`

, where the type variable `c`

has been brought into scope previously. Knowing that means it’s safe for the type of `const`

to be `forall c. c -> (forall d. d -> c)`

. In general, we know that an expression `\(x :: a) -> (y :: β)`

will have a type `a -> β`

. If an algorithm introducing `forall`

s to that type leaves `forall`

s within the type of `β`

, its correctness depends on putting `forall`

s in the same place when processing the type of the expression `y :: β`

. I do not have confidence that my algorithm has that property!

I duck this question entirely at the moment, because we err on the side of introducing `forall`

s earlier than necessary, and at that point the type variables they introduce go into the type environment for sub-expressions. That means we have the same type variable assignments in the environment when we’re introducing `forall`

s to the type of this expression as we do when we’re working on the sub-expressions, which ensures that we come up with the same types for both.

I do have a nagging question, though… does this algorithm that I thought was so much more sophisticated actually just do the same thing as the let-centric algorithm?

In any case…. that’s a wrap! We now have a type inferencer that goes all the way from our expression language to our type language. Sweet!

## One thought on “From Logic Variables to Type Variables”