Types and Programming Languages Chapter 8 Typed Arithmetic Expressions
As mentioned in the introduction of the book, we wish to check the run-time behaviour of a program without evaluating it in order to quickly spot potential bad behaviours. By introducing types into our language, we can express rules about those types (not entirely dissimilar to the evaluation rules we've seen in previous chapters) and check them statically before evaluating a program.
If we can prove that every well-typed term is either a value or can be evaluated a single step ("progress") and that evaluating a well-typed term also results in a well-typed term ("preservation") then we can confident that our program will not get stuck ("safety").
@mudge takes a knee (prodigious amounts of hummus not pictured).
@mrageh gives an example of a badly-typed expression and leads a discussion of programs that will evaluate but won't type check (Simon Peyton-Jones' "The Region of Abysmal Pain").
@urbanautomaton takes to the board.
@urbanautomaton consults the book.
@jcoglan takes to the board.
@leocassarani discusses adding more typing rules to handle edge cases.
@tomstuart takes to the board.
@tomstuart discusses progress and preservation.
@tomstuart discusses safety.
@leocassarani works through the derivation of a well-typed term.
@leocassarani works through the derivation of a badly typed term.
@tomstuart talks about the stronger claim of preservation with our arithmetic language.
The final state of the whiteboard.
A little trolling.
Innovative new ways of moving circular tables are discovered by @tuzz and @jcoglan.
Cheersy cheers!
Thanks to Leo and Geckoboard for hosting, to all those who contributed snacks and to Abeer for organising the meeting (and last week's Computation Pub).