Abstract
Many programming languages use static typing to guarantee runtime safety properties such as the integrity of data structures prior to program execution. At the start of this seventh lecture, we showed how well-known type systems (simple types and parametric polymorphism) extend to advanced control structures : exceptions, effect handlers, unbounded continuations ( call/cc operator), and bounded continuations (cupto operator). This extension can be achieved with little effort, provided that the types of exceptions, effects or program points(prompts) are explicitly declared before use, and that the generalization of type variables is restricted to expressions that are values.
The lecture then turned to the problem of programs that terminate prematurely on an uncaught exception or unhandled effect. We reviewed several linguistic mechanisms that have been proposed to control these risks : exception declarations with dynamic checking (CLU, C++) ; exception declarations with static checking (Java) ; and the use of capabilities to restrict exception raising (Scala 3). Finally, we introduced type and effect systems, which keep track not only of the possible values of expressions but also of the side effects their evaluation may trigger, and developed such a system for a language with algebraic effects, effect handlers and row polymorphism.
