LNL-FPC: The Linear/Non-linear Fixpoint Calculus
2021
We describe a type system with mixed linear and non-linear recursive types
called LNL-FPC (the linear/non-linear fixpoint calculus). The type system
supports linear typing, which enhances the safety properties of programs, but
also supports non-linear typing as well, which makes the type system more
convenient for programming. Just as in FPC, we show that LNL-FPC supports
type-level recursion, which in turn induces term-level recursion. We also
provide sound and computationally adequate categorical models for LNL-FPC that
describe the categorical structure of the substructural operations of
Intuitionistic Linear Logic at all non-linear types, including the recursive
ones. In order to do so, we describe a new technique for solving recursive
domain equations within cartesian categories by constructing the solutions over
pre-embeddings. The type system also enjoys implicit weakening and contraction
rules that we are able to model by identifying the canonical comonoid structure
of all non-linear types. We also show that the requirements of our abstract
model are reasonable by constructing a large class of concrete models that have
found applications not only in classical functional programming, but also in
emerging programming paradigms that incorporate linear types, such as quantum
programming and circuit description programming languages.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
0
Citations
NaN
KQI