ICFP 2021
Sun 22 - Sat 28 August 2021
Sun 22 Aug 2021 23:30 - 23:52 at HIW - Types and GHC 2 Chair(s): Andres Löh

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

f x = [x, x]


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.

Sun 22 Aug

Displayed time zone: Seoul change

23:30 - 01:00
Types and GHC 2HIW at HIW
Chair(s): Andres Löh Well-Typed LLP
Generalization is hard, but somebody's got to do it
A new interface for GHC typechecker plugins and type-family rewriting
Media Attached
The Dynamic Haskell Plugin for GHC
Matthías Páll Gissurarson Chalmers University of Technology, Sweden, Agustín Mista Chalmers University of Technology
GHC Status update
Simon Peyton Jones Microsoft, UK
File Attached