2022.06.03: Linearity and Uniqueness

Daniel Marshall, Michael Vollmer, Dominic Orchard, [2022],
“Linearity and Uniqueness: An Entente Cordiale”

presenter: Alex

Main idea: study and formalise the relationship between linear and unique types, show that it is possible and advantageous to have both in the same type system.

Implementation (integrated into Granule): https://github.com/granule-project/granule/blob/main/examples/uniqueness.gr

1. Introduction

substructural logics (restricted contraction/weakening)

linear types - used exactly once
uniqueness types - values are guaranteed to have at most one reference to them

classic primary use of uniqueness: access to safe in-place update in a functional language without working inside a monad

2. Key Ideas

2.1 Are linearity and uniqueness (essentially) the same?

identical without exponentials: in a setting where all values must be linear, we can also guarantee that every value is unique, and vice versa

dereliction (!A -> A) breaks the symmetry

linearity is not as useful for arrays as for file handles (affine adds weakening)

informations flows in reverse for uniqueness

2.2 Are linearity and uniqueness dual?

Harrington’s ‘uniqueness logic’

! is a comonad (storage+dereliction), \circ is a monad (comonoidal, whereas ? is monoidal)

linear types provide a restriction on what can be done with a value ‘in the future’ (outgoing substitutions) whilst uniqueness types provide a guarantee about what has been done with a value ‘in the past’ (incoming substitutions).

Takeaway: Linearity and uniqueness behave dually with respect to composition, but identically with respect to structural rules, i.e., their internal plumbing.

3. The Linear-Cartesian-Unique Calculus

LCU

linearity is the base and uniqueness is a modality:

Granule compat
unique base is more complex

treat non-linearity and non-uniqueness as the same state

IMELL with additional rules for uniqueness

3.1 Typing

mixed linear/non-linear contexts

context addition ~ PCM

borrow (forget uniqueness, “return”) & copy (create unique, “bind”)

*+! = relative monad

3.2 Equational theory

beta+eta for !
units+assoc for *

3.3 Exploiting uniqueness for mutation

prim arrays

3.4 Operational heap model

the heap records the number of references currently held to it

evaluating a function application first puts the body into the heap

3.5 Metatheory

4. Implementation

Granule

4.1 Frontend

semiring graded necessity modality

4.2 Compilation and Evaluation

unsafe array mutation

Clean
Ownership
Regions
Capabilities

6. Future Work

fractional permissions
Linear Haskell
Adjoint models (only LNL-style)
Ordered and dependent types

7. Conclusion

Suggestions

Aleks:

rewrite the paper using natural deduction instead of sequent calculus
use adjoint logic?