Gradualizer: challenges implementing a type checker
summary
Discusses implementing a gradual type checker for Elixir using the Gradualizer project, focusing on practical challenges of building and properly testing such a compiler-time type checker and comparing its potential value to Dialyzer's long-established approach.
AI-written summary · about
chapters (21)
- 0:00Start
- 1:35Why type checking
- 5:41What is gradual typing
- 6:56Compatible subtype
- 7:54Gradualizer: Design decisions
- 9:03Notation changes
- 9:40Success typing vs static typing
- 11:16Function type signatures
- 12:28Bidirectional type checking
- 13:13Type checking mode
- 14:08Type propagation mode f
- 15:06User controls type propagation
- 17:16Existing rich type system cont.
- 18:08Spec's with type variables
- 20:55Annotated types
- 22:06Overloaded spec's
- 24:15Maps subtyping
- 26:17Variable bindings example
- 26:43Pattern matching - type refinement
- 30:08Inline type annotation operators?
- 32:44Summary
related talks
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
18mGradual Typing for Effect Handlers
23mHow Elixir Learns Types from Guards
40mTypes and Erlang from Dialyzer to (...)
25mIncremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
16mGradually Typing Strategies
46mThe Calculated Typer (Functional Pearl)
20mDeveloping a Monadic Type Checker for an Object-Oriented Language