Motivation
Linear Type theories
New type theory

Going Without:a linear modality and FP
Valeria de Paiva

MSFP 2022(joint work with Eike Ritter, Paola Maneggia and Milly Maietti)
1 / 33

Motivation
Linear Type theories
New type theory

Thanks for the invitation Max and Jeremy!

2 / 33

Motivation
Linear Type theories
New type theory

Today
Categorical Models for Linear and Intuitionistic Type Theory(FOSSACS, LNCS Springer, vol 1784, 2000).
Relating Categorical Semantics for Intuitionistic Linear Logic(Applied Categorical Structures, volume 13(1):1–36, 2005)

why are these important?

3 / 33

Motivation
Linear Type theories
New type theory

Linear Type Theories
why I love them

I worked on Gödel’s Dialectica interpretation for my thesis withMartin Hyland.
I realized that the basic internal categorical model for theDialectica corresponds to linear logic, not intuitionistic logic.

4 / 33

Motivation
Linear Type theories
New type theory

Linear Type Theories
why I love them

Together with Martin Hyland, Nick Benton, and Gavin Bierman I
worked on the first linear type theory, 1993.
Nick then worked on his own version, the LNL calculus, 1995.
Andrew Barber (Plotkin’s student) came up with what I thought
was the best formulation, the DILL calculus, 1997.
5 / 33

Motivation
Linear Type theories
New type theory

xSLAM: eXplicit Substitutions Linear Abstract Machine
EPSRC 1997–2000
Ritter’s PhD thesis on categorical combinators for theCalculus of Constructions (Cambridge 1992, TCS 1994)
de Paiva’s PhD thesis on models of Linear Logic & linear
lambda-calculus (Cambridge 1990)
Put the two together for Categorical Abstract Machines for
Linear Functional Programming
Project xSLAM Explicit Substitutions for Linear AbstractMachines‘categorical structured syntax’ in Hyland’s turn of phrase6 / 33

Motivation
Linear Type theories
New type theory

xSLAM: eXplicit Substitutions Linear Abstract Machine
Twenty years later:
More than 10 papers only submitted to conferences
Only two in journals: Linear Explicit Substitutions. (Ghani, dePaiva, Ritter, 2000) and Relating Categorical Semantics for
Intuitionistic Linear Logic (Maietti, Maneggia, de Paiva, Ritter2005)
Master’s thesis: An Abstract Machine based on Linear Logicand Explicit Substitutions. Francisco Alberti, 1997
Two international workshops: Logical Abstract Machines(Saarbruecken, 1998), Logical Abstract Machines(Birmingham, 1999)
International Dagstuhl meeting: Linear Logic and Applications(1999)
7 / 33

Motivation
Linear Type theories
New type theory

xSLAM Project Work

1Maietti, de Paiva, Ritter. Linear primitive recursion. manuscript 2000.

2

Maietti, de Paiva, Ritter. Categorical Models for Intuitionistic and Linear Type Theory. FoSSaCS 2000.

3

Cervesato, de Paiva, Ritter. Explicit Substitutions for Linear Logical Frameworks. LFM 1999

4Ghani, de Paiva, Ritter. Explicit Substitutions for Constructive Necessity. ICALP 1998

5Ghani, de Paiva, Ritter. Categorical Models for Explicit Substitutions. FoSSaCS 1999.

6de Paiva, E. Ritter. On Explicit Substitutions and Names. ICALP 1997.

7Nesi, de Paiva, Ritter. Rewriting Properties of Combinators for Intuitionistic Linear Logic. Higher OrderAlgebra, Logic and Term Rewriting, HOA’1993.

8Maietti, de Paiva and Ritter. Normalization Bounds in Rudimentary Linear Logic ICC, 2002.

9de Paiva and Eike Ritter. Variations on Linear PCF. WESTAPP, 1999.

8 / 33

Motivation
Linear Type theories
New type theory

Many years later...

time to try again?
9 / 33

Motivation
Linear Type theories
New type theory

Many years later...

”Despite their obvious promise, and a huge research literature,linear type systems have not made it into mainstream
programming languages,[...]”
Linear Haskell, Today and Tomorrow I: Jean-Philippe Bernardy
University of Gothenburg, Sweden, ICFP 2021
Haskell 2021 - Why Functional Programming with Linear Types
Matters, Sep 2021, Mathieu Boespflug Tweag I/O
10 / 33

Motivation
Linear Type theories
New type theory

Categorical Proof Theory
Model derivations/proofs, not whether theorems are true ornotProofs definitely first-class citizens
How? Uses extended Curry-Howard correspondence
Why is it good? Modeling derivations useful where you need
proofs themselves, in linguistics, functional programming,compilers, etc.
Why is it important? Widespread use of logic/algebra in CS
means new important problems to solve with our favorite
tools.
Why so little impact on maths, CS or logic?

11 / 33

Motivation
Linear Type theories
New type theory

Linear Type Theories with Categorical Models

Linear λ-calculus (Benton, Bierman, de Paiva, Hyland, 1992)
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR262.html
DILL system (Plotkin and Barber, 1996)
http://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/
LNL system (Benton, 1995) https://www.researchgate.
net/publication/221558077_A_Mixed_Linear_and_
Non-Linear_Logic_Proofs_Terms_and_Models
Many more without explicit categorical models...

12 / 33

Motivation
Linear Type theories
New type theory

Linear λ-calculus

13 / 33

Motivation
Linear Type theories
New type theory

DILL

14 / 33

Motivation
Linear Type theories
New type theory

LNL

15 / 33

Motivation
Linear Type theories
New type theory

Categorical Models
Linear λ-calculus (ILL)
A linear category is a symmetric monoidal closed (smc)category equipped with a linear monoidal comonad, such thatthe co-Kleisli category of the comonad is a Cartesian closed
Category (CCC). (loads of conditions)
DILL system
A DILL-category is a pair, a symmetric monoidal closed
category and a cartesian category, related by a monoidaladjunction.
LNL system
An LNL-model is a (symmetric) monoidal adjunction between
a smcc and a ccc.
16 / 33

Motivation
Linear Type theories
New type theory

In pictures

17 / 33

Motivation
Linear Type theories
New type theory

In pictures

18 / 33

Motivation
Linear Type theories
New type theory

Wait!

Are these models equivalent?
How do I choose one?
How do I choose the model morphisms?
the solution: Internal Language Theorems!

19 / 33

Motivation
Linear Type theories
New type theory

Explaining Internal Languages
Thanks Milly Maietti for slides!

20 / 33

Motivation
Linear Type theories
New type theory

Explaining Internal Languages
Thanks Milly Maietti for slides!

21 / 33

Motivation
Linear Type theories
New type theory

Explaining Internal Languages
Thanks Milly Maietti for slides!

22 / 33

Motivation
Linear Type theories
New type theory

Explaining Internal Languages
Thanks Milly Maietti for slides!

23 / 33

MotivationLinear Type theories
New type theory

Explaining Internal Languages
Thanks Milly Maietti for slides!

24 / 33

Motivation
Linear Type theories
New type theory

Linear Curry-Howard Isos
“Relating Categorical Semantics for Intuitionistic LinearLogic”(with P. Maneggia, M. Maietti and E. Ritter), Applied
Categorical Structures, vol 13(1):1–36, 2005.

Take home: Categorical models need to be more than sound andcomplete. They need to provide internal languages for the theories
they model.
25 / 33

Motivation
Linear Type theories
New type theory

Why a new calculus?
(ILT, Fossacs 2000)

Choosing between the three type theories:
DILL is best, less verbose than ILL, but closer to what wewant to do than LNL.
Easy formulation of the promotion ruleContains the usual lambda-calculus as a subsystem
However, most FPers would prefer to use a variant of DILL
where instead of !, one has two function spaces, → and −◦But then: what’s the categorical model?

26 / 33

Motivation
Linear Type theories
New type theory

Intuitionistic and Linear Type Theory(ILT, Fossacs 2000)

If we have two function spaces, but no modality !, how can wemodel it?
All the models discussed before have a notion of !, created by theadjunction.
Well, we need to use deeper mathematics, i.e. fibrations orindexed categories.

27 / 33

Motivation
Linear Type theories
New type theory

Calculus ILT
Categorical models for intuitionistic and linear type theory(Maietti et al, 2000)

Γ|a:A⊢a:A

Γ, x : A | ⊢ x : A

Γ | ∆, a : A ⊢ M : B

Γ, x : A | ∆ ⊢ M : B

Γ | ∆ ⊢ λaA .M : A −◦ B

Γ | ∆ ⊢ λx A .M : A → B

Γ | ∆1 ⊢ M : A −◦ B

Γ | ∆2 ⊢ N : A Γ | ∆ ⊢ M : A → B

Γ | ∆ ⊢ M lN : B

Γ| ⊢N:AΓ | ∆ ⊢ M iN : B

28 / 33

Motivation
Linear Type theories
New type theory

ILT MODELS?
(Maietti et al, 2000)
Idea goes back to Lawvere’s hyperdoctrines satisfying thecomprehension axiom.
Model of ILT should modify this setting to capture the separation
between intuitionistic and linear variables.
A base category B, which models the intuitionistic contexts of ILT,
objects in B model contexts (Γ| ).
Each fibre over an object in B modelling a context models termsΓ|∆ ⊢ M : A for any context ∆.
The fibres are now symmetric monoidal closed categories withfinite products and model the linear constructions of ILT

29 / 33

Motivation
Linear Type theories
New type theory

ILT MODELS
have internal language theorems

Missing an understanding of what is essential, what can bechanged, and limitations of the methods.

30 / 33

Motivation
Linear Type theories
New type theory

Speculation

Can we do the same for Modal Logic S4?
Can we do the same for Relevant Logic?
I hope so. But have not managed yet.
Meanwhile pictures do help to remember
the main messages.

31 / 33

Motivation
Linear Type theories
New type theory

Conclusions

Linear type theories are interesting both from implementationand theory perspectives
Internal language theorems are essential for categorical proof
theory: soundness&completeness not enough
Paying attention to morphisms is necessary
Paying attention to implementors is necessary
Finding right abstractions depends on checking other logicalsystems. more experimentation is needed!
Definitely a good time to sharpen our theoretical tools

32 / 33

Motivation
Linear Type theories
New type theory

Thanks!

33 / 33