Handling Delimited Continuations with Dependent Types
Dependent types are a powerful tool for maintaining program invariants.
To take advantage of this aspect in real-world programming, efforts
have been put into enriching dependently typed languages with missing
constructs, most notably, effects.
This paper presents a language that has two practically interesting
ingredients: dependent inductive types, and the delimited control
constructs shift and reset.
When integrating delimited control into a dependently typed language,
however, two challenges arise.
First, the dynamic nature of control operators, which is the source of
their expressiveness, can break fundamental language properties such
as logical consistency and subject reduction.
Second, CPS translations, which we often use to define the semantics
of control operators, do not scale straightforwardly to dependently
typed languages.
We solve the former issue by restricting dependency of types, and the
latter using answer-type polymorphism of pure terms.
The main contribution of this paper is to give a sound type system of
our language, as well as a type-preserving CPS translation.
We also discuss various extensions, which would make our language more
like a full-spectrum proof assistant but pose non-trivial issues.