This post is my musings about a type system proposed by Conor McBride in I Got Plenty o' Nuttin' and refined by Robert Atkey in Syntax and Semantics of Quantitative Type Theory: Quantitative Type Theory or QTT for short. Idris 2 is based on QTT, so at the end there is some code too.
But let me start with recalling Simply Typed Lambda Calculus with Products and Coproducts, (that is a mouthful!). As the name already says there are three binary connectives, functions, products and coproducts (or sums).
But in Martin Löf Type Theory (not quantiative) we have only two: pi and sigma types.
We can recover ordinary functions, and ordinary pairs in a straigh-forward way:
However, to get coproducts we need something extra. One general way is to add finite sets. We get falsehood (empty finite set), truth (singleton finite set), booleans (binary finite sets), and so on. But these three are enough.
With booleans we can define
Which is very reasonable. That is how we represent sum types on physical machines: a tag and a payload which type depends on a tag.
A natural question is what we get if switch to . Unfortuntely, nothing new:
We get another way to describe pairs.
To summarise:
Let us next try to see how this works out with linear types.
In the intuitionistic linear calculus (ILC, also logic, ILL) we have four binary connectives: linear functions, times, plus and with.
Often an unary bang
is also added to allow writing non-linear programs as well.
Making linear dependent theory is hard, and Quantitative Type Theory is a promising attempt. It seems to work.
And it is not complicated. In fact, as far as we concerned, it still has just two connectives
but slightly modified to include multiplicity (denoted by ):
The multiplicity can be , i.e. linear single use. Or , the unrestricted use, but also , which is irrelevant usage. I find this quite elegant.
The rules are then set up so we don't run into problems with "types using our linear variables", as they are checked in irrelevant context.
As in the non-linear setting, we can recover two "simple" connectives immediately:
Other multiplicities allow us to create some "new" connectives
where is the irrelevant quantification.
You should guess that next we will recover and using booleans. However booleans in linear calculus are conceptually hard, when you start to think about resource interpretation of linear calculus. However, booleans are not resources, they are information. About introduction Atkey says
... no resources are required to construct the constants true and false
but the elimination is a bit more involved. The important bit is, however, that we have if-then-else which behaves reasonably.
Then
and
That behaves as we want. When we match on we learn the tag and payload. As tag has multiplicity 1, we can once match on it to learn the type of the payload. (Note: I should really write the typing rules, and derivations, but I'm quite confident it works this way. Highly likely I'm wrong :)
The with-connective, , is mind-juggling. It's a product (in fact, the product in CT-sense). We can extract parts, but if we have to decide which, cannot do both.
The value of type is a function, and we can only call it once, so we cannot write a value of type , nor the inverse.
So the and the are both product like, but different.
We redraw the table from the previous section. there are no more unelegant duplication:
It's often said that you cannot write
diag :: a -> (a, a)
in linear calculus.
This is true if we assume that tuples are tensors. That is natural assumption as is what makes curry with arrows.
However, the product is . I argue that "the correct" type of diag () is
diag : a -> a & a
diag x = x :&: x
And in fact, the adjointness is the same as in CT-of-STLC, (Idris2 agrees with me):
If we could just normalise the notation, then we'd use
But that would be sooo... confusing.
There is plenty of room for more confusion, it gets better.
Products and coproducts usually have units, so is the case in the linear calculus too.
Spot a source of possible confusion.
We know, that because is the product, its unit is the terminal object, . And now we have to be careful.
Definition: T is terminal object if for every object X in category C there exist unique morphism .
Indeed the in linear logic is such object. It acts like a dumpster. If we don't like some (resource) thing, we can map it to . If we already have (there is no way to get rid of it), we can tensor it with something else we don't like and map the resulting "pair" to another . Bottomless trash can!
In category theory we avoid speaking about objects directly (it is point-free extreme). If we need to, we speak about object , we rather talk about morphism (constant function). This works because, e.g. in Sets category:
There the use of comes from it being the unit of used to internalize arrows, i.e. define objects (and binary functions, currying, etc).
In linear logic, the "friend" of is, however, , and its unit is not terminal object.
So we rather have
which is again confusing, as you can confuse for initial object, , which it isn't. To help avoid that I used the subscript.
The takeaway is that and in linear logic are different objects, and you have to be very careful so ordinary lambda calculus (or e.g. Haskell) intuition doesn't confuse you.
I wish there were a category where linear stuff is separate. In Sets . Vector spaces are close, but they have own source of confusion (there , direct sum, which is a product, and coproduct).
All above is nicely encodable in Idris 2. If you want to play with linear logic concepts, I'd say that Idris2 is the best playground at the moment.
module QTT
-----------------------------------------------------------------------
-- Pi and Sigma
-----------------------------------------------------------------------
Pi1 : (a : Type) -> (a -> Type) -> Type
Pi1 a b = (1 x : a) -> b x
data Sigma1 : (a : Type) -> (a -> Type) -> Type where
Sig1 : (1 x : a) -> (1 y : b x) -> Sigma1 a b
-----------------------------------------------------------------------
-- Lollipop
-----------------------------------------------------------------------
Lollipop : Type -> Type -> Type
Lollipop a b = Pi1 a \_ => b
-- handy alias
(-@) : Type -> Type -> Type
(-@) = Lollipop
infixr 0 -@
-- for constructor, just write \x => expr
-- Lollipop elimination, $
lollipopElim : Lollipop a b -@ a -@ b
lollipopElim f x = f x
-----------------------------------------------------------------------
-- Times
-----------------------------------------------------------------------
Times : Type -> Type -> Type
Times a b = Sigma1 a \_ => b
-- Times introduction
times : a -@ b -@ Times a b
times x y = Sig1 x y
-- Times elimination
timesElim : Times a b -@ (a -@ b -@ c) -@ c
timesElim (Sig1 x y) k = k x y
-----------------------------------------------------------------------
-- With
-----------------------------------------------------------------------
With : Type -> Type -> Type
With a b = Pi1 Bool \t => if t then a else b
-- With elimination 1
fst : With a b -@ a
fst w = w True
-- With elimination 2
snd : With a b -@ b
snd w = w False
-- There isn't really a way to write a function for with introduction,
-- let me rather write diag.
diag : a -@ With a a
diag x True = x
diag x False = x
-- Also note, that even if With would be a built-in, it should
-- be non-strict (and a function is).
-- We may use the same resource in both halfs differently,
-- and the resource cannot be used until user have selected the half.
-----------------------------------------------------------------------
-- Plus
-----------------------------------------------------------------------
Plus : Type -> Type -> Type
Plus a b = Sigma1 Bool \t => if t then a else b
-- Plus introduction 1
inl : a -@ Plus a b
inl x = Sig1 True x
-- Plus introduction 2
inr : b -@ Plus a b
inr y = Sig1 False y
-- Plus elimination, either... with a with twist
-- Give me two functions, I'll use one of them, not both.
plusElim : With (a -@ c) (b -@ c) -@ Plus a b -@ c
plusElim f (Sig1 True x) = f True x
plusElim f (Sig1 False y) = f False y
-----------------------------------------------------------------------
-- Extras
-----------------------------------------------------------------------
-- plusElim is reversible.
-- Plus -| Diag
plusElimRev : (Plus a b -@ c) -@ With (a -@ c) (b -@ c)
plusElimRev f True = \x => f (inl x)
plusElimRev f False = \y => f (inr y)
-- Diag -| With
adjunctFwd : (c -@ With a b) -@ With (c -@ a) (c -@ b)
adjunctFwd f True = \z => f z True
adjunctFwd f False = \z => f z False
adjunctBwd : With (c -@ a) (c -@ b) -@ (c -@ With a b)
adjunctBwd f c True = f True c
adjunctBwd f c False = f False c
-----------------------------------------------------------------------
-- Hard exercise
-----------------------------------------------------------------------
-- What would be a good way to imlement Top, i.e unit of With.
--
-- fwd : a -@ With Top a
-- bwd : With Top a -@ a
--
-- I have ideas, I'm not sure I like them.