Canonical bidirectional typechecking

TL;DR

This work establishes a canonical bidirectional typechecking framework for polarised System L, linking the checkable/synthesisable split to the calculus's polarity and chirality. It develops cocontextual typing with co-de Bruijn scoping, then unifies the positive and negative fragments into full polarised System L, and finally extends to System LNL to incorporate linear-nonlinear modalities with annotated derived connectives. The approach reveals three-way coincidences among polarisation shifts, LNL modalities, and bidirectional typing, and it outlines a program to embed conventional calculi and richer type theories into System L-based frameworks to facilitate principled typechecking and potential subject reduction results.

Abstract

We demonstrate that the checkable/synthesisable split in bidirectional typechecking coincides with existing dualities in polarised System L, also known as polarised $μ\tildeμ$-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.

Figures (10)

• Figure 1: Scoping rules of standard bidirectional $\lambda$-calculus
• Figure 2: Scoping rules for products and coproducts in standard bidirectional $\lambda$-calculus
• Figure 3: Scoping rules for cocontextual linear $\lambda$-calculus
• Figure 4: Co-de Bruijn $\lambda$-calculus, scoping rules
• Figure 5: Scoping rules for positive system L