# Foundations of Bidirectional Programming III: The Logic of Lenses

See parts I and II of this series. There is also now a source repo!

In this post we will make probably the single most important step from a generic type theory to one specialised to bidirecional programming.

In a bidirectional language there are 2 kinds of variables: ones travelling forwards in time, and ones travelling backwards in time. I will refer to the types of these variables *covariant* and *contravariant* for short (or at least shorter). Variables of covariant type are the ones we are used to: they behave according to ordinary *cartesian* scoping rules, which means they can be implicitly deleted (referred to zero times) and implicitly copied (referred to more than once).

Variables of *cocartesian* type are the weird ones. They can also be implicitly copied and deleted, but because they are going backwards, from the forwards perspective it looks like they can be implicitly *merged* and *spawned*. By *spawned* I mean they can be bound zero times and still referred to; and by *merged* I mean they can be bound twice without the later binding shadowing the earlier binding. On the other hand they can *not* be implicitly copied or deleted. Their scoping rules are *cocartesian*.

I can now reveal that my *party trick* in the last section of my first post where I built a cocartesian language was secretly not in fact a party trick after all, but was all along in preparation for this exact moment.

Now suppose we take a tensor product of a covariant type and a contravariant type. Now we have a variable referring to a bundle of a cartesian value, which can be deleted and copied but not spawned or merged, and a cocartesian value, which can be spawned and merged but not deleted or copied. Since doing any of these operations to a pair means doing it to both, our variable cannot be deleted or copied or spawned or merged, which means it is a *linear* variable. I will refer to such a tensor product type as *invariant*. Secretly, all of the types in my second post were invariant, since that language was linear.

There is a secret fourth thing, which is variables with *bicartesian* scoping rules, so they can be deleted and copied and spawned and merged. I will refer to these types as *bivariant*. It would be entirely reasonable to not include these, but I have a secret plan for them that will be revealed in the next post. For now, the only bivariant type will be the monoidal unit.

## The 4 kinds of things

Just as terms are classified by types, types are classified by *kinds*, which means I have been talking about kinds the whole time. But these are not kinds as we know them from languages like Haskell. We have the added complication that kinds control the scoping rules of variables of the types they classify; but on the other hand we have the added simplification that there are *exactly* 4 kinds, rather than an infinite supply of them. I have to thank Michael Arntzenius, who visited Zanzi and me a few weeks ago, for planting the idea of a 4-element lattice of kinds.

Let’s start with the easy parts:

```
Kind : Type
Kind = (Bool, Bool)
data Ty : Kind -> Type where
Unit : Ty (True, True)
Ground : Ty (True, False)
Not : Ty (cov, con) -> Ty (con, cov)
```

I implement the 4-element lattice as the product `(Bool, Bool)`

, where the first flag tracks whether the type is covariant and the second whether it is contravariant. I anticipate that much later, probably when I add type polymorphism, it will become necessary to take seriously that there are subkind relationships here, but I will cross that particular bridge when it is in front of me. `Unit`

is a bivariant type, `Ground`

is a covariant type (it is still a placeholder, and in the next post will be replaced with a proper system for base types). The `Not`

operator acts on the underlying kind by interchanging the covariant and contravariant capabilities; so strictly covariant types become strictly contravariant and vice versa, whereas the bivariant and invariant kinds are both stable under negation.

There is an alternative way of implementing it, but it is much more tedious: instead of representing kinds explicitly, have 4 different versions of `Ty`

for each of the 4 kinds. That leads to a proliferation of type operators - 4 operators for `Not`

and 16 for `Tensor`

(which we’re coming to next), 1 for each combination of kinds of the 2 inputs. I really hope that won’t be necessary, but it’s something I’m keeping in my back pocket just in case I run into an insurmountable problem with this encoding.

Now we come to the hard part: tensor products. A tensor product is covariant if both parts are covariant, and is contravariant if both parts are contravariant. In a world with a sufficiently smart typechecker we would simply write this:

```
Tensor : Ty (covx, conx) -> Ty (covy, cony)
-> Ty (covx && covy, conx && cony)
```

But we already know how to handle this situation, it’s the same idea as for list concatenation in the first post. We define the relation corresponding to the boolean conjunction function, and a section of it:

```
data And : Bool -> Bool -> Bool -> Type where
True : And True b b
False : And False b False
(&&) : (a : Bool) -> (b : Bool) -> (c : Bool ** And a b c)
True && b = (b ** True)
False && b = (False ** False)
```

(Here’s I’m having fun with Idris’ ability to disambiguate names based on typing information, something I really wish I could do in Haskell.)

Now we can write the actual definition of tensor products, which is much more complicated looking than it should be, but this is just what we have to deal with until the day when somebody builds a typechecker that can handle trivial equational reasoning:

```
Tensor : {covx, covy, conx, cony : Bool}
-> {default (covx && covy) cov : _} -> {default (conx && cony) con : _}
-> Ty (covx, conx) -> Ty (covy, cony) -> Ty (cov.fst, con.fst)
```

## The scoping rules

Now we come to the main topic of this post: how kinds influence scoping rules. In the first post we saw how to implement context morphisms for planar, linear, cartesian and cocartesian languages. Those definitions were all polymorphic over arbitrary lists. Then in the second post we defined context morphisms that could introduce and elimination double negations, which was no longer polymorphic but specialised to a particular language of types, and this will continue.

Now that types are indexed by kinds, everything else becomes more complicated: everything we do from now on becomes additionally indexed by kinds, starting with this.

(Note, I decided to reuse the name `Structure`

, since this should be the last one we ever need.)

Let’s start with the linear rules:

```
data Structure : All Ty kas -> All Ty kbs -> Type where
Empty : Structure [] []
Insert : {a, b : Ty (cov, con)} -> {as : All Ty kas} -> {bs : All Ty kbs}
-> Parity a b -> IxInsertion a as as' -> Structure as bs -> Structure as' (b :: bs)
```

Here `IxInsertion`

is an indexed version of the `Insertion`

datatype from the previous post, relationally defining insertions into an `All`

type indexed by an underlying list:

```
data IxInsertion : {0 x : a} -> p x
-> {0 xs : List a} -> All p xs
-> {0 ys : List a} -> All p ys -> Type where
Z : IxInsertion {x} a {xs} as {ys = x :: xs} (a :: as)
S : IxInsertion {x} a {xs} as {ys} bs
-> IxInsertion {x = x} a {xs = y :: xs} (b :: as) {ys = y :: ys} (b :: bs)
```

I’m not going to explain all of the syntax and semantics of Idris happening here because it would take us too far afield, and despite appearances this is not intended to be a tutorial series on Idris programming. Suffice to say, defining indexed versions of standard datatypes is *significantly* harder than defining the originals.

The definition of `Parity`

, which handles double negations, is unchanged from the previous post besides adding the kind indexes:

```
data Parity : Ty (cov, con) -> Ty (cov, con) -> Type where
Id : Parity a a
Raise : Parity a b -> Parity a (Not (Not b))
Lower : Parity a b -> Parity (Not (Not a)) b
```

The Idris typechecker is, at least, smart enough to figure out that double negation leaves the kind unchanged. This is one reason that I write out kinds as pairs of booleans everywhere rather than defining a function `swap : Kind -> Kind`

, since that causes Idris to get stuck here.

One thing to note is that I reversed the polarity of the `Insert`

constructor from the previous post, so that it now conses on the codomain and inserts on the domain rather than the other way round. The previous post was “supply driven”, saying where everything in the domain goes in the codomain, whereas this version is “demand driven”, saying where everything in the codomain came from in the domain. This was a late change after I experienced manually defining terms in this core syntax and found that this way makes manual proof search much easier. If it later turns out that the original supply driven version makes writing elaborators easier, it’s an easy change to turn it back.

Next we have the rules for delete and copy, which can be applied only to covariant types. We don’t care whether the type is also contravariant, ie. we can use it for both strictly covariant types and bivariant types. This is the other reason I define kinds to be pairs of booleans rather than their own dedicated language, because otherwise we would have twice as many constructors here.

```
Delete : {a : Ty (True, con)} -> Structure as bs -> Structure (a :: as) bs
Copy : {a : Ty (True, con)} -> {as : All Ty xs}
-> IxElem a as -> Structure as bs -> Structure as (a :: bs)
```

Here `IxElem`

is, of course, an indexed version of the `Elem`

datatype, which I won’t bother to write here but was also painful to define. (If you want to you can find it in the IxUtils module of the source repo.)

With that, defining the constructors for spawn and merge is easy, and completes our definition of `Structure`

once and for all.

```
Spawn : {b : Ty (cov, True)} -> Structure as bs -> Structure as (b :: bs)
Merge : {b : Ty (cov, True)} -> {bs : All Ty ys}
-> IxElem b bs -> Structure as bs -> Structure (b :: as) bs
```

## The full logic of lenses

We can now put the pieces together and make the first real definition of our kernel language. I hope that nothing here will change, only be added to in the future.

Of course everything is kind indexed:

```
data Term : All Ty ks -> Ty k -> Type where
Var : Term [x] x
Rename : Structure as bs -> Term bs x -> Term as x
```

I renamed `Act`

to `Rename`

since the last post, since somebody pointed out that’s what it is.

Unit introduction and elimination rules work as they did before:

```
UnitIntro : Term [] Unit
UnitElim : {as : All Ty kas} -> {bs : All Ty kbs} -> {default (ixSimplex as bs) cs : _}
-> Term as Unit -> Term bs x -> Term (cs.snd.fst) x
```

Here `ixSimplex`

is the tactic corresponding to a datatype `IxSimplex`

which is the relational version of the indexed version of `++`

, operating on `All`

rather than `List`

. This one is worth writing down because it returns a twice-iterated Sigma type, so we have to extract the part we need with `.snd.fst`

:

```
data IxSimplex : {0 xs : List a} -> All p xs
-> {0 ys : List a} -> All p ys
-> {0 zs : List a} -> All p zs -> Type where
Z : IxSimplex [] bs bs
S : IxSimplex {xs} as {ys} bs {zs} cs
-> IxSimplex {xs = x :: xs} (a :: as) {ys = ys} bs {zs = x :: zs} (a :: cs)
ixSimplex : {xs : List a} -> (as : All p xs)
-> {ys : List a} -> (bs : All p ys)
-> (zs : List a ** cs : All p zs ** IxSimplex as bs cs)
ixSimplex {xs = []} [] {ys} bs = (ys ** bs ** Z)
ixSimplex {xs = x :: xs} (a :: as) {ys} bs
= let (zs ** cs ** n) = ixSimplex {xs = xs} as {ys = ys} bs
in (x :: zs ** a :: cs ** S n)
```

Now we come to the negation rules, and the final twist of this post. In the language we reached at the end of the previous post, which amounts to the fragment of this language for only invariant types, there was no not-introduction rule - correctly so. As I speculated there, there are indeed some valid instances of not-introduction, but they are not sufficient to prove general double negation introduction or elimination - and they can’t even be expressed without the kind system we developed in this post.

It turns out that we have two not-introduction rules, one that is valid for covariant types and one that is valid for contravariant types. This introduces a sort of incompatibility between negation and tensor, since the tensor product of two variables with a valid not-introduction rule can fail to have one.

```
NotIntroCov : {a : Ty (True, con)} -> Term (a :: as) Unit -> Term as (Not a)
NotIntroCon : {a : Ty (cov, True)} -> Term (a :: as) Unit -> Term as (Not a)
NotElim : {as : All Ty kas} -> {bs : All Ty kbs} -> {default (ixSimplex as bs) cs : _}
-> Term as (Not x) -> Term bs x -> Term (cs.snd.fst) Unit
```

I would say that this is the first case where my well typed by construction methodology enabled me to do something that I think I would have failed at otherwise. I figured out these rules at the same time as the corresponding cases of the well typed evaluator (which will be the topic of the next post). Although they look like they are among the simplest rules in the language, they are the ones I understand by far the least.

If we have a bivariant type then both of these rules can be applied to produce the same result. It seems tempting to try to roll these two rules into one, which can be applied when *either* `cov`

or `con`

is `True`

. This is a bit tricky to do, but it turns out to also be a bad idea: although these rules are *logically* equivalent, they are not *type-theoretically* equivalent: they have completely different operational semantics! And by that I don’t mean something like different evaluation strategies, I mean that they actually output different results.

Now there’s only the tensor rules, and for once there is nothing to say about them, they are the indexed versions of the tensor rules from the last 2 posts.

```
TensorIntro : {as : All Ty kas} -> {bs : All Ty kbs} -> {default (ixSimplex as bs) cs : _}
-> Term as x -> Term bs y -> Term (cs.snd.fst) (Tensor x y)
TensorElim : {as : All Ty kas} -> {bs : All Ty kbs} -> {default (ixSimplex as bs) cs : _}
-> Term as (Tensor x y) -> Term (x :: y :: bs) z -> Term (cs.snd.fst) z
```

And that’s it!

Like I said, in the next post we will build a well typed evaluator, which means we will also write and run our first programs - and we can already do some interesting things, like basic automatic differentiation. The only small thing that will need to be added to the language from this post is a mechanism for adding basic types and basic terms, such as arithmetic operators between doubles.