Types and Erlang from Dialyzer to (...)
summary
Erlang already uses Dialyzer’s success typing and a gradual type approach that prove definite mistakes (not full correctness); examples show Dialyzer infers maps, booleans and integer constraints and flags mismatches. Session types promise typed protocols that track message sequences (the shop checkout example) but integrating them with PIDs, anonymous actor lifetimes and live hot code swaps is hard. Past efforts (a 1‑year Wadler attempt, Uppsala gradual systems) work partially; no complete, backwards‑compatible static solution exists yet.
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
37mSession Types: A History and Applications
39mProtocol engineering for communicating actors
35mDiving into Erlang is a one-way ticket
40mSo I used Erlang...is my system as scalable as they say it'd be?
14mLightning Talk: Towards Mailbox Typing for Erlang
45mTaming Distribution: Formal Protocols for Akka Typed
01h 01mThe Erlang Ecosystem
31mMulti-lingual Erlang