Type System for Four Delimited Control Operators
summary
Presents a monomorphic type system that covers the four delimited control operators shift, control, shift0 and control0 by deriving types from a CPS interpreter (Danvy and Filinski style) and adding constraints to track trail and meta-continuation information. Implements a typed CPS interpreter in Agda to prove the CPS translation preserves types and to show the calculus with all four operators is terminating. Also maps the new system back to existing shift/control/shift0 systems to show compatibility.
AI-written summary · about
chapters (11)
- 0:00Start
- 0:54What is a delimited control operator?
- 2:184 delimited control operators
- 2:48Type system for each, but not for all
- 3:03Back to the initial motivation...
- 3:51Comparing shift, control, shifto and controlo
- 5:51Review: two dynamic behaviors
- 7:00Two dynamic behaviors, also in CPS interpreter
- 8:41Deriving the whole type system from the interpreter
- 9:42Derivation approach
- 12:19Summary
related talks
12mTowards Dependently-Typed Control Effects (Extended Abstract)
29mA Typed and Unified Reflection for Shift and Shift0
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
15mBack to Direct Style: Typed and Tight
02h 50mIntro to Type Systems and Operational Semantics
21mSyntax with Shifted Names
56mOn Type-Based Techniques for Program Manipulation
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers