Hindley, Milner, and Damas taught us how to go from

f x = [x, x]

to

f :: a -> [a]

We guess a type for x, discover that this type is unconstrained by the usage sites of x, and then generalize over its type, calling it a. We can go even further with this basic understanding of generalization and apply it in scenarios where a function is defined locally, with some type variables in scope. (Hint: don’t generalize a type variable that’s already in use!)

Haskell, however, is not so simple. Here are some harder cases:

g x = (x == x) || (x < x)   -- infer constraints with Eq or Ord or both?

h x = [x] == []             -- infer Eq [a] or Eq a?

class C a b | a -> b where
  meth :: a -> b
j x = [x, meth True]        -- looks like j :: C Bool a => ...,
                            -- but the fundep means we *always* know a

type family F a
type family G a
injectF :: a -> F a
injectF = ...
injectG :: a -> G a
injectG = ...

k x = [injectF x, injectG x]   -- we require (F a ~ G a) here

We can find even harder examples, especially if we consider the possibility of local functions.

In this talk, I will walk the audience through GHC’s simplifyInfer function, which is responsible for inferring types, both in the case where there is no type signature at all, and also for partial type signatures. The key action in simplifyInfer is generalization, when GHC figures what variables and constraints to quantify over.

Along the way, we will also see why GHC does not always infer principal types (https://gitlab.haskell.org/ghc/ghc/-/issues/19977) and how GHC’s notion of generalization is expected to change ever so slightly in the presence of functional dependencies.

Principal Researcher at Tweag. I believe that clever application of theory can eliminate a great deal of programmer errors – specifically, I think fancy types and functional programming are the future. I completed my PhD in 2016 at University of Pennsylvania working under Stephanie Weirich; my dissertation topic was the integration of dependent types into the Haskell programming language. I am a core contributor to the Glasgow Haskell Compiler (GHC) and Chair of the Board of Directors at the Haskell Foundation.