Panel discussion: Types for All: From weak to strong, from static to dynamic
summary
Panelists compare concrete systems and trade-offs: dependent types in Idris 2 (about 50,000 lines of Idris, with tests taking ~3x the build time) eliminate deep name-handling bugs; a 100k-line Scala compiler swaps list representation and hits equality/equals pitfalls; Newspeak’s parser-combinator reuse breaks easy static typing; industry examples—TypeScript, Flow, Hack, Sorbet—prove gradual/optional typing at scale works while preserving dynamic freedom.
AI-written summary · about
chapters (12)
- 0:00Welcome and introductions
- 0:23Panelist introductions
- 5:59Why type systems matter
- 12:58Types vs unit tests
- 17:37Refining test strategies
- 22:15When types hinder progress
- 27:35Practical tips for types
- 31:53Optional and gradual typing
- 36:57Implementing optional typing
- 42:57Teaching type systems
- 46:46The role of compiler errors
- 52:02Future of type systems
related talks
43mIdris 2: Type-driven development of Idris
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
41mThe Dialectics of Type-Level Programming
01h 06mKeynote – Edwin Brady
30mDotty and types: the story so far
33mLightning Talks II
24mImperative Syntax for Dependent Types
19mIll-Typed Programs Don't Evaluate