-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2018.InternalizingVariance
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 show a nice use case (positivity checking, co-/inductive sized types) for tracking the variance/monotonicity of functions. The syntax and judgments used by Andreas are similar to those I presented in the talk.
- A. Abel. Polarized Subtyping for Sized Types, MSCS'06.
- A. Abel. The Next 700 Modal Type Assignment Systems, TYPES'15.
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.