Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
summary
Claims a reusable Haskell implementation strategy for bidirectional typing and Hindley-Milner inference built on the scope-safe Free Foil representation; provides capture-avoiding substitution, alpha-equality and a working HM inference prototype while level-based generalization is pending. Handles mixed term/type syntax by unifying grammars (a noted limitation of Free Foil for true mutual recursion), ships code on GitHub with partial docs, and aims to automate Dunfield–Fanning recipe and generalize interfaces for language-agnostic checkers.
AI-written summary · about
chapters (11)
- 0:00Project introduction
- 1:10Motivation for generic type checking
- 2:13Bidirectional typing approach
- 4:19Fenning recipe for bidirectional systems
- 5:46Hindley-Milner overview
- 6:27Free Foil for scoped syntax
- 8:12Mutually recursive terms and types
- 10:37Unified syntax for error messages
- 11:40Zero-cost scoping and checks
- 13:03Implementation status and plans
- 14:09Name spaces and IDE integration
related talks
16mSyntax-Generic Operations, Reflectively Reified (Extended Abstract)
46mThe Calculated Typer (Functional Pearl)
59mHaskell Design Patterns for Genericity & Asynchronous Behavior
20mInteractive Haskell Type Inference Exploration (Extended Abstract)
42mFunctional interpreters and you
39mHands-On Intro to Bidirectional Type Inference with Elm
16mDigging for Fold: Synthesis-Aided API Discovery for Haskell
46mTesting in the world of Functional Programming