Towards Dependently-Typed Control Effects (Extended Abstract)
summary
Design of a dependently-typed language with delimited control operators includes a purity restriction that types may depend only on pure terms and a selective CPS translation that converts only effectful terms to CPS. Extension with conditionals whose branches have different types/effects reveals that conditional computation types can fail to normalize, breaking static compatibility checks and CPS translation. The work stops short of a solution and suggests dynamic CPS semantics as a possible remedy.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:11Combining dependent types and effects
- 2:37Motivating example
- 4:30Typing judgment (without conditional)
- 5:12Typing rules of application
- 6:32CPS translation of dependent application
- 7:25Type preservation
- 7:51Typing judgment (with conditional)
- 8:09Typing rules of conditional
- 10:25CPS translation of non-dependent conditional
- 11:14Summary & questions for audience
related talks
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
19mType System for Four Delimited Control Operators
29mHigher-Order Weakest Precondition Transformers via a CPS Transformation
15mHandling Bidirectional Control Flow
15mBack to Direct Style: Typed and Tight
19mTowards a Reflection for Effect Handlers
18mDeveloping a Dependently Typed Language with Runtime Proof Search
22mType-Safe Code Generation With Algebraic Effects and Handlers