Implicit Polarized F: local type inference for impredicativity

Reference. Implicit Polarized F: local type inference for impredicativity

System F, the polymorphic lambda calculus, features the principle of impredicativity: polymorphic types may be (explicitly) instantiated at other types, enabling many powerful idioms such as Church encoding and data abstraction. Unfortunately, type applications need to be implicit for a language to be human-usable, and the problem of inferring all type applications in System F is undecidable. As a result, language designers have historically avoided impredicative type inference. We reformulate System F in terms of call-by-push-value, and study type inference for it. Surprisingly, this new perspective yields a novel type inference algorithm which is extremely simple to implement (not even requiring unification), infers many types, and has a simple declarative specification. Furthermore, our approach offers type theoretic explanations of how many of the heuristics used in existing algorithms for impredicative polymorphism arise.

Cite

Cite as @mercer-2022-implicit (helia, typst) · \cite{mercer-2022-implicit} (LaTeX)

BibTeX

bibtex · 8 lines

@misc{mercer-2022-implicit,
  author = {Henry Mercer and Cameron Ramsay and Krishnaswami, Neelakantan R.},
  title = {Implicit Polarized F: local type inference for impredicativity},
  year = {2022},
  month = {3},
  eprint = {2203.01835},
  archiveprefix = {arXiv}
}

hayagriva YAML (typst)

yaml · 10 lines

mercer-2022-implicit:
  type: misc
  title: 'Implicit Polarized F: local type inference for impredicativity'
  author:
  - Mercer, Henry
  - Ramsay, Cameron
  - Krishnaswami, Neelakantan R.
  date: 2022-03
  serial-number:
    arxiv: '2203.01835'

Download: mercer-2022-implicit.bib · mercer-2022-implicit.yml

Cited by (1)

Canonical bidirectional typechecking mihejevs-2025-canonicalarXiv · 2025

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.

arXiv

Cites 25 works (1 here)

With notes (1)

Complete and easy bidirectional typechecking for higher-rank polymorphism dunfield-2013-completeICFP · 2013

PDF · DOI · arXiv · pldb

External (24)

A quick look at impredicativity (2020)
Guarded impredicative polymorphism (2018)
A dissection of L (2014)
Flexible types: robust type inference for first-class polymorphism (2009)
HMF: simple type inference for first-class polymorphism (2008)
FPH: first-class polymorphism for Haskell (2008)
From ML to MLF: graphic type constraints with efficient type inference (2008)
System F with type equality coercions (2007)
Practical type inference for arbitrary-rank types (2007)
Call-by-push-value: Decomposing call-by-value and call-by-name (2006)
Boxy types: inference for higher-rank types and impredicativity (2006)
A Linear Spine Calculus (2003)
MLF: raising ML to the power of system F (2003)
Colored local type inference (2001)
Local type inference (2000)
Polymorphic subtyping without distributivity (1998)
The subtyping problem for second-order types is undecidable (1996)
Putting type annotations to work (1996)
An implementation of F<: (1993)
Theorems for free! (1989)
Types, Abstraction and Parametric Polymorphism (1983)
A Theory of Type Polymorphism in Programming (1978)
Towards a theory of type structure (1974)
Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types (1971)