Skip to content

Abstracts.2018.InternalizingVariance

Jump to bottom
Sandro Stucki edited this page Mar 6, 2019 · 4 revisions

Internalizing variance using 2-categories

by Sandro Stucki

The notion of "variance", "monotonicity" or "polarity" of operations is ubiquitous in the meta-theory of logics and programming languages, but it is seldom reflected into the syntax of such languages, so that a programmer or logician can reason directly about monotone functions. In this talk I will present a modal extension to the simply-typed lambda calculus that allows reasoning about ordered terms and monotone functions defined over them. I will show that the usual categorical semantics of STLC as CCCs can be extended to a 2-categorical semantics that covers the extra order-theoretic structure. Since I don't expect any prior knowledge about higher category theory, I will also give a brief intro to 2-categories.

Update: unfortunately, there are no notes for my talk (yet), but the following papers by Andreas Abel and Martin Steffen show a nice use case for tracking the variance/monotonicity of functions: positivity checking for type operators, in particular for co-/inductive (sized) types. This is important to ensure the soundness of inductive type definitions (e.g. in Agda and Coq) and for subtype-checking in OO-languages with generics (e.g. Java, Scala). The syntax and judgments used by Andreas are similar to those I presented in the talk.

Also, the polarity lattice I described in the talk forms a coeffect structure. For more info on coeffects (including their categorical semantics), see the references to papers on coeffects included in the abstract for my earlier talk on that subject.

Clone this wiki locally