Type inference for application spines
summary
Argues that typechecking whole application spines — head plus all arguments — yields concrete wins: clearer error locations (e.g. “third argument of f”), supports visible type application and required type arguments, and makes impredicative instantiation feasible. Tools are bidirectional checking, an expected-type reference cell for infer-vs-check, short-lived instantiation variables, and the Quick Look instantiation strategy; this design is implemented in GHC practice for ~20 years, covers the common case (≈99% heads are variables), and works in the compiler.
AI-written summary · about
chapters (8)
- 0:00Introduction to type checking
- 1:06Bidirectional type checking
- 3:50Working with type inference
- 6:17Refining the inference algorithm
- 11:22Limitations of binary application
- 21:09Treating applications as a whole
- 25:10Formalizing the application model
- 29:48Conclusion and Q&A
related talks
01h 02mType Inference in GHC
30mDotty and types: the story so far
13mA Quick Look at Impredicativity
39mEverything You Always Wanted to Know About Type Inference
26mType Narrowing the Hard Way
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
15mTaming Type Annotations in Gradual Typing
19mIll-Typed Programs Don't Evaluate