Hands-On Intro to Bidirectional Type Inference with Elm
summary
Implements a bidirectional type inference engine for a simply-typed lambda calculus in Elm, with working infer and check functions, use of Elm's Elm Dictionary as the gamma context, and live demo code in an online Elm IDE. Shows concrete rules: variables, function application (infer E1 then check E2), and annotated lambdas (check mode requiring top‑level annotations). Several unit tests start failing but after coding the three cases identity and basic integer/boolean examples succeed; error reporting still uses Maybe vs Result.
AI-written summary · about
chapters (19)
- 0:00Intro to bidirectional type inference
- 1:07Motivation for bidirectional type inference
- 4:22Structure and benefits of bidirectional inference
- 5:47Roadmap and Elm setup
- 6:09Simply typed lambda calculus
- 10:24Type context and dictionary ops
- 11:31Type judgments and deduction rules
- 13:00Implementing type judgments in Elm
- 15:30Type inference for function application
- 18:47Challenges with function declarations
- 19:30Check versus infer split
- 21:17Live demo and Elm IDE walkthrough
- 22:41Check-infer and annotation rules
- 25:56Implementing variable inference
- 27:00Implementing function application
- 30:00Implementing function declarations
- 33:17When to check vs infer
- 35:54Future improvements and resources
- 37:18Call for volunteers and closing
related talks
20mTowards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
46mThe Calculated Typer (Functional Pearl)
20mInteractive Haskell Type Inference Exploration (Extended Abstract)
51mElm-Friendly Functional Programming For The Web
53mAdventures in Elm: Events, Reproducibility, and Kindness
21mParsing lexical ambiguity with Elm and expressive types
27mElm, a Truly Innovative Language for the Web
51mGreek Classics: Lambda Calculus For Beginners