Canonical bidirectional typechecking

TL;DR

This paper reveals a deep connection between bidirectional typechecking, polarised System L, and linear-nonlinear calculus, unifying various logical dualities and type systems.

Contribution

It demonstrates that the checkable/synthesisable split in bidirectional typechecking aligns with dualities in polarised System L and extends this to a combined linear and cartesian type framework.

Findings

Identifies a 3-way coincidence between polarised System L, LNL calculi, and bidirectional calculi.

Extends the duality framework to ordinary System L using co-de Bruijn scopes.

Unifies linear and cartesian types within a linear-nonlinear style.

Abstract

We demonstrate that the checkable/synthesisable split in bidirectional typechecking coincides with existing dualities in polarised System L, also known as polarised $\mu\tilde{\mu}$-calculus. Specifically, positive terms and negative coterms are checkable, and negative terms and positive coterms are synthesisable. This combines a standard formulation of bidirectional typechecking with Zeilberger's `cocontextual' variant. We extend this to ordinary `cartesian' System L using Mc Bride's co-de Bruijn formulation of scopes, and show that both can be combined in a linear-nonlinear style, where linear types are positive and cartesian types are negative. This yields a remarkable 3-way coincidence between the shifts of polarised System L, LNL calculi, and bidirectional calculi.