An Effectful Treatment of Dependent Types

TL;DR

This paper extends Levy's call-by-push-value framework to dependent type theory to analyze effects and dependent types interaction, proposing new systems with semantic and operational insights.

Contribution

It introduces dependently typed CBPV systems, dCBPV- and dCBPV+, with semantics and operational properties, addressing effects and subtyping constraints.

Findings

dCBPV+ enables well-defined CBV and CBN translations of DTT

dCBPV- is simpler but less expressive with effects

Subtyping conditions are necessary for model construction and subject reduction

Abstract

We extend Levy's call-by-push-value (CBPV) analysis from simple to dependent type theory (DTT) in order to study the interaction between computational effects and dependent types. We define the naive system of dependently typed CBPV, dCBPV-, and its extension with a principle of Kleisli extensions for dependent functions, dCBPV+. We investigate these systems from the points of view of syntax, categorical semantics, concrete models and operational semantics, in presence of a range of effects. We observe that, while the expressive power of dCBPV+ is needed if we want well-defined call-by-value (CBV) and call-by-name (CBN) translations of DTT, it is a less straightforward system than dCBPV-, in presence of some effects. Indeed, to be able to construct specific models and to retain the subject reduction property in the operational semantics, we are required to impose certain subtyping conditions, the idea being that the type of a computation may only become more (not less) specified as certain effects are executed.