Ill-Typed Programs Don't Evaluate

on YouTube ↗23m

" summary

Introduces two-sided type systems — sequent-calculus judgments that allow arbitrary expressions on the left and lists of typings on the right, plus a top type containing all values — and claims a pair of guarantees: well-typed programs don’t go wrong and ill-typed programs don’t evaluate (reach a value). Demonstrates the system on constructors and pattern matching (proves head(nil) does not evaluate), defines a necessity arrow for leftward reasoning, gives an algorithm for type inference in the appendix (not yet implemented), and explores internalising negation as a type complement that yields an alternate semantics where well-typed code can still go wrong.

AI-written summary · about

" chapters (12)

1. 0:00Functional programming basics
2. 2:09Correctness in type systems
3. 5:22Typing judgments for bugs
4. 8:14Typing rules for properties
5. 11:54Necessity arrow type
6. 15:51Left-hand typing bugs
7. 17:21Conclusion
8. 18:05Q&A
9. 19:50Termination and call-by-value vs call-by-name
10. 20:32Ill-typed programs
11. 21:15Implementation and inference
12. 21:59Defining 'go wrong'