LFCS Seminar: Tuesday 17th June: Andreas Abel

Title: Graded Call-by-push-value -- tracking (co)effects in a functional language

Abstract

Call-by-push-value (CBPV) is a simply typed lambda calculus that

polarizes types into value and computation types and can thus

express both call-by-name and call-by-value evaluation in the

presence of effects. Semantically, effects are modeled by a monad,

and computation types as algebras over this monad.

Effect type systems usually express more information than the

presence of an effect; often effects are categorized by a preordered

monoid where the monoid operation represents accumulation of effects

and the order expresses effect subsumption, in analogy to subtyping.

In this work, a graded version of CBPV is presented where the

typing of computations likens effect typing. Semantically,

computation types are then represented as graded monad algebras.

Observing that the value types of CBPV can be interpreted as comonad

coalgebras, we further present a version of CBPV that has coeffects

graded by a preordered semiring. Value types and contexts are

interpreted as graded comonad coalgebras, allowing resource-aware

interpretations of CBPV.

Finally, we combine the two systems into a fully graded version of

CBPV where both effects and coeffects are graded. This turns out to

be possible without specifying any interaction between effects and

coeffects.