Types and Erlang from Dialyzer to (...)
summary
Dialyzer works as a gradual success-typing analyzer that proves concrete mistakes (not full correctness), infers shapes like “params must be a map” and flags mismatched types; Uppsala’s approach makes typing optional so old code keeps running. Research on session types models typed protocols (example: a shop protocol that sequences add/check-out) promises reasoning about message timelines but clashes with Erlang’s anonymous actors, pids and live upgrades. Hot code swap is brittle in practice—only one noted user (Clara) still does it—so session types remain research, not production-ready.
AI-written summary · about
chapters (8)
- 0:00Intro
- 1:45What is type system
- 7:30How we failed to type
- 16:00Hot code swap
- 16:45gradual type system
- 20:32code
- 29:01session types
- 35:59question
related talks
27mTyping Erlang with eqWAlizer
40mGradualizer: challenges implementing a type checker
44mA Few Improvements to Erlang
32mIntrinsically Typed Sessions with Callbacks
46mThe Calculated Typer (Functional Pearl)
34mAnalysing and Understanding Erlang Programmatically
23mHow Elixir Learns Types from Guards
26mType Narrowing the Hard Way