Bidirectional Typing for Erlang
summary
A bidirectional type system for Erlang is implemented as a prototype that subsumes Hindley‑Milner and supports union types and higher‑rank polymorphism, requiring only seven top‑level annotations to typecheck existing code and running on three standard library modules without rewriting user code. Type inference uses ordered contexts and application judgments from Dunfield and Krishnaswami style algorithms and achieves similar performance to the Erlang type checker. Current limits: subset of Erlang, no records, no concurrency or builtin subtyping yet.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:11Outline
- 0:34Lack of Static Type System
- 1:25Previous Attempts for a Static Type System
- 4:34Dynamic Type Behaviours in Erlang
- 7:54Higher-Rank Polymorphism
- 10:24Examples for Bidirectional Typing Judgements
- 12:48Bidirectional Typing for Polymorphism
- 15:24Examples From OTP Libraries
- 16:06Limitations
- 16:21Future Work
related talks
19mBidirectional Higher-Rank Polymorphism with Intersection and Union Types
01h 03mKeynote: Precision in Type System Design
15mScalable Type Inference for Intrinsically-Typed Binders
27mDecomposable Type Highlighting for Bidirectional Type and Cast Systems
33mTyped Clojure: From Optional to Gradual Typing
33mStatically Typed Interpreters
49mThe Trouble With Types
01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in Haskell