Cross-posted from Zanzi’s blog

This is the first post in a new series documenting my work developing a bidirectional programming language, in which all programs are interpreted as optics. This is something I’ve been thinking about for a long time, and eventually I became convinced that there were enough subtle issues that I should take things extremely slowly and actually learn some programming language theory. As a result, this post will not be about categorical cybernetics at all, but is a foundation to a huge tower of categorical cybernetics machinery that I will build later.

The first issue is that because the tensor product of optics is not cartesian, a language for optics is necessarily substructural. So this post is about a way to implement substructural languages in a way that avoids hidden pitfalls. The code in this post is Idris2, a dependently typed language.

We begin with a tiny language for types, with monoidal products (a neutral name because later we will be making it behave like different kinds of product), a unit type to be the neutral element of the monoidal product, and a “ground” type that is intended to contain some nontrivial values.

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

Cartesian terms

Although we have used the name “tensor”, suppose we want to make an ordinary cartesian language where variables can be implicitly copied and discarded. Here is a standard way to do it: it is an intuitionistic natural deduction calculus.

data Term : List Ty -> Ty -> Type where
  -- A variable is a term if we can point to it in scope
  Var : Elem x xs -> Term xs x
  -- Unit is always a term in every scope
  UnitIntro : Term xs Unit
  -- Pattern matching on Unit, redunant here but kept for comparison to later
  UnitElim : Term xs Unit -> Term xs x -> Term xs x
  -- A pair is a term if each side is a term
  TensorIntro : Term xs x -> Term xs y -> Term xs (Tensor x y)
  -- Pattern matching on a pair, adding both sides to the scope
  TensorElim : Term xs (Tensor x y) -> Term (x :: y :: xs) z -> Term xs z

The constructor for Var uses Elem, a standard library type that defines pointers into a list:

data Elem : a -> List a -> Type where
  Here : Elem x (x :: xs)
  There : Elem x xs -> Elem x (x' :: xs)

Here are some examples of programs we can write in this language:

-- \x => ()
delete : CartesianTerm [a] Unit
delete = UnitIntro

-- \(x, y) => x
prjl : CartesianTerm [a, b] a
prjl = Var Here

-- \(x, y) => y
prjr : CartesianTerm [a, b] b
prjr = Var (There Here)

-- \x => (x, x)
copy : CartesianTerm [a] (Tensor a a)
copy = TensorIntro (Var Here) (Var Here)

-- \(x, y) => (y, x)
swap : CartesianTerm [a, b] (Tensor b a)
swap = TensorIntro (Var (There Here)) (Var Here)

The thing that makes this language cartesian and allows us to write these 3 terms is the way that the context xs gets shared by the inputs of the different term constructors. In the next section we will define terms a different way, and then none of these examples will typecheck.

Planar terms

Next let’s go to the opposite extreme and build a fully substructural language, in which we cannot delete or copy or swap. I learned how to do this from Conor Mc Bride and Zanzi. Here is the idea:

data Term : List Ty -> Ty -> Type where
  -- A variable is a term only if it is the only thing in scope
  Var : Term [x] x
  -- Unit is a term only in the empty scope
  UnitIntro : Term [] Unit
  -- Pattern matching on Unit consumes its scope
  UnitElim : Term xs Unit -> Term ys y -> Term (xs ++ ys) y
  -- Constructing a pair consumes the scopes of both sides
  TensorIntro : Term xs x -> Term ys y -> Term (xs ++ ys) (Tensor x y)
  -- Pattern matching on a pair consumes its scope
  TensorElim : Term xs (Tensor x y) -> Term (x :: y :: ys) z -> Term (xs ++ ys) z

This is a semantically correct definition of planar terms and it would work if we had a sufficiently smart typechecker, but for the current generation of dependent typecheckers we can’t use this definition because it suffers from what’s called green slime. The problem is that we have types containing terms that involve the recursive function ++, and the typechecker will get stuck when this function tries to pattern match on a free variable. (I have no idea how you learn this if you don’t happen to drink in the same pubs as Conor. Dependently typed programming has a catastrophic lack of books that teach it.)

The fix is that we need to define a datatype that witnesses that the concatenation of two lists is equal to a third list - a witness that the composition of two things is equal to a third thing is called a simplex. The key idea is that this datatype exactly reflects the recursive structure of ++, but as a relation rather than a function:

data Simplex : List a -> List a -> List a -> Type where
  Right : Simplex [] ys ys
  Left : Simplex xs ys zs -> Simplex (x :: xs) ys (x :: zs)

Now we can write a definition of planar terms that we can work with:

data Term : List Ty -> Ty -> Type where
  Var : Term [x] x
  UnitIntro : Term [] Unit
  UnitElim : Simplex xs ys zs 
          -> Term xs Unit -> Term ys y -> Term zs y
  TensorIntro : Simplex xs ys zs 
             -> Term xs x -> Term ys y -> Term zs (Tensor x y)
  TensorElim : Simplex xs ys zs 
            -> Term xs (Tensor x y) -> Term (x :: y :: ys) z -> Term zs z

This language is so restricted that it’s hard to show it doing anything, but here is one example of a term we can write:

-- \(x, y) => (x, y)
foo : Term [a, b] (Tensor a b)
foo = TensorIntro (Left Right) Var Var

Manually defining simplicies, which cut a context into two halves, is very good as a learning exercise but eventually gets irritating. We can direct Idris to search for the simplex automatically:

data Term : List Ty -> Ty -> Type where
  Var : Term [x] x
  UnitIntro : Term [] Unit
  UnitElim : {auto prf : Simplex xs ys zs} 
          -> Term xs Unit -> Term ys y -> Term zs y
  TensorIntro : {auto prf : Simplex xs ys zs} 
             -> Term xs x -> Term ys y -> Term zs (Tensor x y)
  TensorElim : {auto prf : Simplex xs ys zs} 
            -> Term xs (Tensor x y) -> Term (x :: y :: ys) z -> Term zs z

foo : Term [a, b] (Tensor a b)
foo = TensorIntro Var Var

This works, but I find that the proof search gets confused easily (although it works fine for the baby examples in this post), so let’s pull out the big guns and write a tactic:

concat : (xs, ys : List a) -> (zs : List a ** Simplex xs ys zs)
concat [] ys = (ys ** Right)
concat (x :: xs) ys = let (zs ** s) = concat xs ys in (x :: zs ** Left s)

This function takes two lists and returns their concatenation together with a simplex that witnesses this fact. Here ** is Idris syntax for both the type former and term former for dependent pair (aka. Sigma) types.

data Term : List Ty -> Ty -> Type where
  Var : Term [x] x
  UnitIntro : Term [] Unit
  UnitElim : {xs, ys : List Ty} 
          -> {default (concat xs ys) prf : (zs : List Ty ** Simplex xs ys zs)}
          -> Term xs Unit -> Term ys y -> Term prf.fst y
  TensorIntro : {xs, ys : List Ty} 
              -> {default (concat xs ys) prf : (zs : List Ty ** Simplex xs ys zs)}
              -> Term xs x -> Term ys y -> Term prf.fst (Tensor x y)
  TensorElim : {xs, ys : List Ty} 
            -> {default (concat xs ys) prf : (zs : List Ty ** Simplex xs ys zs)} 
            -> Term xs (Tensor x y) -> Term (x :: y :: ys) z -> Term prf.fst z

foo : {a, b : Ty} -> Term [a, b] (Tensor a b)
foo = TensorIntro Var Var

I find Idris’ default syntax to be a bit awkward, but it feels to me like a potentially very powerful tool, and something I wish Haskell had for scripting instance search.

Context morphisms

Unfortunately, going from a planar language to a linear one - that is, ruling out copy and delete but allowing swaps - is much harder. I figured out a technique for doing this that turns out to be very powerful and give very fine control over the scoping rules of a language.

The idea is to isolate a category of context morphisms (technically a coloured pro, that is a strict monoidal category whose monoid of objects is free). Then we will parametrise a planar language by an action of this category. The good news is that this is the final iteration of the definition of Term, and we’ll be working with it for the rest of this blog post.

Structure : Type -> Type
Structure a = List a -> List a -> Type

data Term : Structure Ty -> List Ty -> Ty -> Type where
  Var : Term hom [x] x
  Act : hom xs ys -> Term hom ys x -> Term hom xs x
  UnitIntro : Term hom [] Unit
  UnitElim : {xs, ys : List Ty} 
          -> {default (concat xs ys) prf : (zs : List Ty ** Simplex xs ys zs)}
          -> Term hom xs Unit -> Term hom ys y -> Term hom prf.fst y
  TensorIntro : {xs, ys : List Ty}
             -> {default (concat xs ys) prf : (zs : List Ty ** Simplex xs ys zs)}
             -> Term hom xs x -> Term hom ys y -> Term hom prf.fst (Tensor x y)
  TensorElim : {xs, ys : List Ty} 
            -> {default (concat xs ys) prf : (zs : List Ty ** Simplex xs ys zs)} 
            -> Term hom xs (Tensor x y) -> Term hom (x :: y :: ys) z 
            -> Term hom prf.fst z

First, let’s recover planar terms. To do this, we want to define a Structure where hom xs ys is a proof that xs = ys:

data Planar : Structure a where
  Empty : Planar [] []
  Whisker : Planar xs ys -> Planar (x :: xs) (x :: ys)

Now let’s deal with linear terms. For that, we want to define a Structure where hom xs ys is a proof that ys is a permutation of xs. We can do this in two steps:

-- Insertion x xs ys is a witness that ys consists of xs with x inserted somewhere
data Insertion : a -> List a -> List a -> Type where
  -- The insertion is at the head of the list
  Here : Insertion x xs (x :: xs)
  -- The insertion is somewhere in the tail of the list
  There : Insertion x xs ys -> Insertion x (y :: xs) (y :: ys)

data Symmetric : Structure a where
  -- The empty list has a unique permutation to itself
  Empty : Symmetric [] []
  -- Extend a permutation by inserting the head element into the permuted tail
  Insert : Insertion x ys zs -> Symmetric xs ys -> Symmetric (x :: xs) zs

(Incidentally, this is the point where I realised that although Idris looks like Haskell, programming in it feels a lot closer to programming in Prolog.)

Now we write swap as term:

swap : {a, b : Ty} -> Term Symmetric [a, b] (Tensor b a)
swap = Act (Insert (There Here) (Insert Here Empty)) (TensorIntro Var Var)

Explicitly cartesian terms

Now we can come full circle and redefine cartesian terms in a way that uniformly matches the way we do substructural terms.

data Cartesian : Structure a where
  -- Delete everything in scope
  Delete : Cartesian xs []
  -- Point to a variable in scope and make a copy on top
  Copy : Elem y xs -> Cartesian xs ys -> Cartesian xs (y :: ys)

With this, we can rewrite all the terms we started with:

delete : {a : Ty} -> Term Cartesian [a] Unit
delete = Act Delete UnitIntro

prjl : {a, b : Ty} -> Term Cartesian [a, b] a
prjl = Act (Copy Here Delete) Var

prjr : {a, b : Ty} -> Term Cartesian [a, b] b
prjr = Act (Copy (There Here) Delete) Var

copy : {a : Ty} -> Term Cartesian [a] (Tensor a a)
copy = Act (Copy Here (Copy Here Delete)) (TensorIntro Var Var)

swap : {a, b : Ty} -> Term Cartesian [a, b] (Tensor b a)
swap = Act (Copy (There Here) (Copy Here Delete)) (TensorIntro Var Var)

Let’s end with a party trick. What would a cocartesian language look like - one where we can’t delete or copy, but we can spawn and merge?

Co : Structure a -> Structure a
Co hom xs ys = hom ys xs

-- spawn : Void -> a
-- spawn = \case {}
spawn : {a : Ty} -> Term (Co Cartesian) [] a
spawn = Act Delete Var

-- merge : Either a a -> a
-- merge = \case {Left x => x; Right x => x}
merge : {a : Ty} -> Term (Co Cartesian) [a, a] a
merge = Act (Copy Here (Copy Here Delete)) Var

-- injl : a -> Either a b
-- injl = \x => Left x
injl : {a, b : Ty} -> Term (Co Cartesian) [a] (Tensor a b)
injl = Act (Copy Here Delete) (TensorIntro Var Var)

-- injr : b -> Either a b
-- injr = \y => Right y
injr : {a, b : Ty} -> Term (Co Cartesian) [b] (Tensor a b)
injr = Act (Copy (There Here) Delete) (TensorIntro Var Var)

Since at the very beginning we added a single generating type Ground, and the category generated by one object and finite coproducts is finite sets and functions, this language can define exactly the functions between finite sets. For example, there are exactly 4 functions from booleans to booleans:

id, false, true, not : Term (Co Cartesian) [Ground, Ground] (Tensor Ground Ground)
id = Act (Copy Here (Copy (There Here) Delete)) (TensorIntro Var Var)
false = Act (Copy Here (Copy Here Delete)) (TensorIntro Var Var)
true = Act (Copy (There Here) (Copy (There Here) Delete)) (TensorIntro Var Var)
not = Act (Copy (There Here) (Copy Here Delete)) (TensorIntro Var Var)

That’s enough for today, but next time I will continue using this style of term language to start dealing with the difficult issues of building a programming language for optics.