See part I of this series

In this post we’ll begin designing a kernel language in which all programs are optics. What I mean by a “kernel language” is that it will serve as a compiler intermediate representation, with a surface language compiling down to it. I intend the surface language to be imperative style like the current Open Game Engine (with an approximately Python-like syntax), but the kernel language will reflect the category theory as closely as possible. I plan the kernel language to be well typed by construction, something that seems like overkill until I think about the problem of figuring out how pattern matching should work in a bidirectional language.

My first design choice is that object language types denote pairs of metalanguage types, with one denoting the forward part (sometimes I might call it the covariant denotation) and the other denoting the backward part (the contravariant denotation).

Cov : Ty -> Type
Con : Ty -> Type

The interpretation of a term will be a lens:

eval : Term xs y -> All Cov xs -> (Cov y, Con y -> All Con xs)

Here All is an Idris standard library function that combines a type-level map with cartesian product:

data All : (a -> Type) -> List a -> Type where
  Nil : All p []
  (::) : p x -> All p xs -> All p (x :: xs)

(Idris has what in Haskell would be called rebindable syntax switched on by default, so we can use the usual syntactic sugar for lists to refer to elements of All.)

eval is a well typed interpreter, and is a placeholder while we prototype: much later, this is where the backend of the compiler will begin.

The logic of lenses

My second design choice is that I want the basic product former to be interpreted as the tensor product of lenses, which is pairwise cartesian product on the covariant and contravariant parts. This is an uncontroversial choice, but importantly this product is symmetric monoidal but not cartesian, so it means that we are designing some kind of linear type theory.

My third design choice is that I want negation to be interpreted as swapping the covariant and contravariant parts. This sounds uncontroversial at first - many well known semantic categories do the same thing - until we notice that it is not functorial. That is to say, if we have a lens $(X, X’) \to (Y, Y’)$ then in general we can’t make a lens between $(X’, X)$ and $(Y’, Y)$ in either direction. Years ago I wrote a paper called Coherence for lenses and open games in which this non-functorial pair swapping featured heavily, and I still stake everything on the claim that it is the right way to go.

At this point we have enough to build a term language and its interpretation. I will add a single ground type which will be interpreted as purely covariant.

data Ty : Type where
  Unit : Ty
  Ground : Ty
  Not : Ty -> Ty
  Tensor : Ty -> Ty -> Ty

mutual
  Cov : Ty -> Type
  Cov Unit = Unit
  Cov Ground = Nat
  Cov (Not x) = Con x
  Cov (Tensor x y) = (Cov x, Cov y)

  Con : Ty -> Type
  Con Unit = Unit
  Con Ground = Unit
  Con (Not x) = Cov x
  Con (Tensor x y) = (Con x, Con y)

Let’s think through the consequences of these choices. We think of Tensor as linear conjunction, so its neutral element Unit is linear truth. The interpretation of Unit is the pair $(1, 1)$, and so Not Unit - which we would think of as linear falsity - has the same interpretation. So we have a linear logic where falsity and truth coincide semantically. Similarly, the de Morgan dual of Tensor, which we would call linear disjunction, coincides with it semantically. So we have an inconsistent interpretation of linear logic. This is nowhere near as bad as it sounds, since many reasonable semantic categories do the same, but we need to keep it in mind.

Since Tensor is a perfectly cromulent symmetric monoidal product, its introduction and elimination rules will be exactly the same as the ones in my previous post. But the negation rules are going to be quite a puzzle.

Our interpretation of negation is strictly involutive - swapping twice is a no-op - something we can call a classical linear negation. This means our semantics validates the principles of double negation introduction and double negation elimination: both of them are interpreted as an identity lens.

The principle of explosion says that $p$ and $\neg p$ together entail falsity, for every proposition $p$. Since falsity and truth coincide, for us the principle of explosion says that $p$ and $\neg p$ together entail truth. This is a valid principle in our semantics. Suppose $p$ is interpreted as $(X, X’)$, then $p \otimes \neg p$ is interpreted as $(X \times X’, X’ \times X)$. There is indeed a canonical lens $(X \times X’, X’ \times X) \to (1, 1)$, namely the “turnaround” lens, which I normally call a counit.

In Idris, suppose we have

explosion : {a : Ty} -> Term [a, Not a] Unit

Then we must have

eval explosion : {a : Ty} -> All Cov [a, Not a] -> (Unit, Unit -> All Con [a, Not a])

which up to isomorphism reduces to

eval explosion : {a : Ty} -> (Cov a, Con a) -> (Con a, Cov a)

Of course, we want to implement eval so that this gives us the swap function.

The de Morgan dual of the principle of explosion is the principle of excluded middle, which says that truth entails $p$ or $\neg p$. Remembering that our conjunction and disjunction coincide, if $p$ has interpretation $(X, X’)$ then excluded middle would denote a lens $(1, 1) \to (X \times X’, X’ \times X)$. In general there is no lens of this type, so our semantics does not validate excluded middle.

In Idris, suppose we had

lem : {a : Ty} -> Term [] (Tensor a (Not a))

Then we must have

eval lem : {a : Ty} -> All Cov [] -> ((Cov a, Con a), (Con a, Cov a) -> All Con [])

which up to isomorphism reduces to

eval lem : {a : Ty} -> (Cov a, Con a)

which is impossible as soon as we introduce any types that are not pointed.

A logic puzzle

This suggests a logic puzzle: can we design a proof system for negation that validates double negation introduction, double negation elimination and the principle of explosion, but does not validate excluded middle?

After some tinkering I did indeed invent a system with these properties. Sadly it turned out to be a red herring, since it ended up proving these principles that are valid for lenses in terms of more primitive principles that are not valid for lenses. But I still think it’s an interesting enough sideline to report here.

The system I designed was a 2-sided hybrid of a natural deduction calculus and a sequent calculus, with general right-elimination, and both left-elimination and right-introduction restricted to empty sequents on the right. In standard proof theory syntax I would write it like this:

\[\frac{\Gamma, \varphi \vdash}{\Gamma \vdash \neg \varphi} (RI) \qquad \frac{\Gamma, \neg \varphi \vdash}{\Gamma \vdash \varphi} (LE) \qquad \frac{\Gamma \vdash \varphi, \Delta \qquad \Gamma' \vdash \neg \varphi, \Delta'}{\Gamma, \Gamma' \vdash \Delta, \Delta'} (RE)\]

In Idris:

data Term : List Ty -> List Ty -> Type where
  Var : Term [x] [x]
  LAct : Symmetric xs' xs -> Term xs ys -> Term xs' ys
  RAct : Term xs ys -> Symmetric ys ys' -> Term xs ys'
  NotIntroR : Term (x :: xs) [] -> Term xs [Not x]
  NotElimL : Term (Not x :: xs) [] -> Term xs [x]
  NotElimR : Simplex xs1 xs2 xs3 -> Simplex ys1 ys2 ys3
          -> Term xs1 (y :: ys1) -> Term xs2 (Not y :: ys2) -> Term xs3 ys3

Symmetric is the structure for permutations that I introduced in the previous post.

Here are what our principles look like, together with some non-proofs that are ruled out by the restrictions on right-introduction and left-elimination:

dni : {a : Ty} -> Term [a] [Not (Not a)]
dni = NotIntroR (LAct (Insert (There Here) (Insert Here Empty)) 
                      (NotElimR (Left Right) Right Var Var))

dne : {a : Ty} -> Term [Not (Not a)] [a]
dne = NotElimL (NotElimR (Left Right) Right Var Var)
-- ruled out by NotIntroR restriction
-- dne = NotElimR Right (Left Right) (NotIntroR Var) Var

explosion : {a : Ty} -> Term [a, Not a] []
explosion = NotElimR (Left Right) Right Var Var

lem : {a : Ty} -> Term [] [Not a, a]
-- ruled out by NotIntroR restriction
-- lem = NotIntroR Var
-- ruled out by NotElimL restriction
-- lem = NotElimL (NotElimL (NotElimR (Left Right) Right Var Var))

Unfortunately, although my restricted left-elimination and right-introduction rules can be used to prove the semantically valid principles of double negation introduction and elimination, they are themselves not semantically valid. The problems start to appear once we add back in the rules for tensor, which in this 2-sided calculus are

  TensorIntro : Simplex xs1 xs2 xs3 -> Simplex ys1 ys2 ys3
             -> Term xs1 (y1 :: ys1) -> Term xs2 (y2 :: ys2) 
             -> Term xs3 (Tensor y1 y2 :: ys3)
  TensorElim : Simplex xs1 xs2 xs3 -> Simplex ys1 ys2 ys3
            -> Term xs1 (Tensor x y :: ys1) -> Term (x :: y :: xs2) ys2 
            -> Term xs3 ys3

Now we can write a bad term:

bad : {a : Ty} -> Term [] [Not (Tensor a (Not a))]
bad = NotIntroR (TensorElim (Left Right) Right Var explosion)

Although these rules don’t seem to be strong enough to prove the distributive law between tensor and negation, semantically this is the same shape as excluded middle. I think it would be possible to restrict left-elimination and right-introduction differently to rule out this kind of thing, but only at the expense of leaving us with unprovable instances of double negation introduction and elimination.

Structurally involutive negation

Although I would love to come up with a calculus that fulfills my requirements using pure logic, I currently believe that it’s impossible. So instead I will bring out the big guns, and use a Structure. The methodology I introduced in the previous post yields a clean conceptual separation into syntax and logic. If we want to say that two things are syntactically identical, for example permutations of contexts, we use a Structure to encode that. So what we are about to do is to encode a principle that $p$ and $\neg \neg p$ are not merely logically equivalent but syntactically identical.

This is how we do it:

data Parity : Ty -> Ty -> Type where
  Id : Parity x x
  Raise : Parity x y -> Parity x (Not (Not y))
  Lower : Parity x y -> Parity (Not (Not x)) y

data Involutive : Structure Ty where
  Empty : Involutive [] []
  Insert : Parity x y -> Insertion y ys zs -> Involutive xs ys -> Involutive (x :: xs) zs

An element of Involutive xs ys is a witness that ys is a permutation of xs but with an arbitrary number of double negatives inserted or removed.

With double negation introduction and elimination taken care of, all we have to do is to make a logic that validates the principle of explosion and not excluded middle, which is easy: it’s an ordinary 1-sided natural deduction calculus with the negation introduction rule omitted.

data Term : List Ty -> Ty -> Type where
  Var : Term [x] x
  Act : Involutive xs ys -> Term ys t -> Term xs t
  NotElim : {xs, ys : List Ty} -> {default (simplex xs ys) prf : _}
         -> Term xs t -> Term ys (Not t) -> Term prf.fst Unit
  TensorIntro : {xs, ys : List Ty} -> {default (simplex xs ys) prf : _}
             -> Term xs t -> Term ys t' -> Term prf.fst (Tensor t t')
  TensorElim : {xs, ys : List Ty} -> {default (simplex xs ys) prf : _}
            -> Term xs (Tensor x y) -> Term (x :: y :: ys) z -> Term prf.fst z

We can write exactly the terms that we want to:

dni : {a : Ty} -> Term [a] (Not (Not a))
dni = Act (Insert (Raise Id) Here Empty) Var

dne : {a : Ty} -> Term [Not (Not a)] a
dne = Act (Insert (Lower Id) Here Empty) Var

explosion : {a : Ty} -> Term [a, Not a] Unit
explosion = NotElim Var Var

lem : {a : Ty} -> Term [] (Tensor a (Not a))
-- impossible

And it’s now possible to write a well typed interpreter for this definition of terms, although I’ll skip it here because it involves several pages of mostly tedious boilerplate code. In the next post we’ll add the missing scoping rules to our language, so that by the time we come back to the well typed interpreter in post number 4, we’ll be able to use it to do a little bit of differentiable programming.