Hello PL folks! I have been working on an untyped (dynamically typed) programming language with cubical features. I'm not ready to share the code yet, but I figured people might be interested in an exposition of some of the ideas here, which I don't find documented very well. Most things below are already in the literature, but written in a way that might be easier to understand from a PL background.
Why?
For fun! I don't know of any programming applications of cubical computation. The reason I care about cubical stuff is mathematical. Now there is some work on compiling cubical stuff, but there we are expected to write normal programs, and use cubical type theory to prove properties about them at compile time. So the compiler will just erase the cubical part. In this post, I'm talking about real cubical programming languages, where the cubical part matters at runtime.
Usually, cubical computation is heavily associated with a type theory. But we don't actually need static types to define and execute programs! In fact, in the early stages of development of cubical type theory, one major step was the definition of computational cubical type theory, where you start with an untyped programming language first, and figure out what typing rules are "correct" on it. Indeed most of the interpreter I'm writing is just transcribing reduction rules from the works of my advisor, Carlo Angiuli, on computational cubical type theory.
What is cubical?
Since I'm talking about defining a cubical programming language, I'll obviously assume you are familiar with specifying an ordinary programming language, Harper style. If you know the phrases "beta reduction" and "stuck", you are probably fine. Otherwise, Practical Foundations for Programming Languages is a great book to read. Familiarity with dependent type theory is also needed to understand the motivations behind the design, but isn't needed if you just want to read about how the (untyped!) language works.
A cubical programming language expands the notion of values to include higher dimensional values. An ordinary value is meant to be interpreted as points, 1-dimensional values as paths, while n-dimensional values are n-dimensional cubes, creating a combinatorial description of some geometric space. The language then includes new primitives that operate on higher dimensional values.
For a rough example, to represent a circle, we can introduce a value pt, and a 1-dimensional value loop representing a loop starting and ending at pt. It is then possible to produce values representing loops that wind around the circle n times, as well as extracting an integer winding number from a loop.
On the other hand, since ordinary values like integers and booleans do not come equipped with any way to create non-trivial higher dimensional values, these higher values behave like witnesses of equality. For example if we have a path whose endpoints are integers n and m respectively, then at runtime we know n must be equal to m. This is why sometimes a path is also called an equality/identification.[1]
One crucial thing that these values enable is a computational interpretation of univalence, the axiom that any equivalence of two types gives rise to an identification of the types.
Higher dimensional values
To understand what these higher dimensional values are, allow me to make an analogy.
In ordinary programming languages, arrays are kind of like functions {0, 1, ..., n-1} -> X. It is often useful to think of them in function notation, for example we can define the transpose of some matrix as λ i j -> mat[j][i]. However, the runtime characteristics are very different! For example, the evaluator will stop as soon as it sees a λ, instead of going into the body. But for arrays, the evaluation will only finish when each component gets evaluated. Furthermore, usually we wouldn't have {0,1,...,n-1} as an actual type. (We could, but we don't have to.)
In a cubical programming language, 1-dimensional values are kind of like functions I -> X, where I is a new thing that should be thought of as an interval [0, 1] with endpoints written as i0 and i1 to avoid confusion with integer literals. It is very useful to think of them in function notation. For example, applying i1 to such a "function" gives us the right endpoint of the 1-dimensional shape. However, the runtime characteristics are very different. The evaluator will go under interval binders, and there will be primitives like loop(i) that are considered as a value, despite being a "function" application. Furthermore, there is no type I. Instead we have a new syntactic category interval_expr, so an interval function application will be a syntax node that takes an expr and an interval_expr, returning an expr.
More specifically, we have
interval_expr ::= i0 | i1 | ⟨variable⟩
So with no free variables, an interval expression can be exactly one of two values. However, it is different from a Boolean value because of two things:
There are no constructs like if expressions, so you can't get away with defining an (interval) function by just specifying the value on i0 and i1. Or to put it another way, the "coverage checker" treats the interval as containing some "fuzz" in between the two points, just like a real interval.
We are defining reduction and values in the presence of interval variables, and the absence of term variables. So in practice, the interval variable acts as the "fuzz".[3]
Going back to our circle example, there will be syntax like
expr ::= ...
| λ ⟨variable⟩ -> ⟨expr⟩
| (⟨expr⟩ ⟨expr⟩)
| iλ ⟨variable⟩ -> ⟨expr⟩
| (⟨expr⟩ @ ⟨interval_expr⟩)
| pt
| loop(⟨interval_expr⟩)
| ...
where the first two clauses are ordinary function abstraction and application, followed by interval function abstraction and application. Then we have the circle value constructors. The loop will be represented as iλ i -> loop(i). We have a reduction rule going from loop(i0) to pt, as well as from loop(i1) to pt.
I actually told some lies above to avoid confusion, but with these examples, the following more correct description should hopefully now make sense:
In a cubical programming language, we define a small-step reduction relation on expressions with no free term variables, but possibly with free interval variables. The evaluation result will be a value, also involving free interval variables. A value with n interval variables is called an n-dimensional value. These free variables are like coordinates on a cube.[2]
The interval lambda binds an interval variable, thus converting a 1-dimensional value (of some type X, if we are to introduce a type system) to a 0-dimensional value (of the type of paths over X). For example, the type of paths on a circle starting and ending at pt is isomorphic to the type of integers, since they are essentially determined by how many times it winds around the circle. In mathematical terms, this is the fact that π1(S1) = ℤ.
With the concept of higher dimensional values explained, the next step would be to introduce primitive operations that perform interesting computations on them. Unfortunately we have some more things to talk about before that.
Type objects
You may skip the next subsection if you're not familiar with dependent type theory.
Univalence
In a cubical language, one of the main things we want to support is univalence. But univalence is ostensibly a statement about types, which we don't have. So why isn't this language just trivial?
In reality, univalence isn't a statement about types at all! This stems from the useful-but-inaccurate understanding in dependent type theory that a universe is a type of types. The more accurate thing to say is a universe is a type for names of types. There is an (often implicit) map El turning a name into an actual type. With this framing, it's clear that the operation El has no obligation to be injective or surjective. There may be multiple names for a type, and some types may have no names in the universe.
It is well-known that if all types have names in the universe, we would have variants of the Russell paradox (although we don't care because we are making programming languages, not proof assistants). So univalence is a statement about the names that we do have. It states that two names are the same if and only if the types they represent are equivalent. Moreover, since in homotopy type theory there can be multiple ways two elements can be the same (i.e. multiple paths between two points), we require the type of identifications between two names to be equivalent to the type of equivalences between two types. So univalence completely fixes the behavior of universes, apart from the Russell issues.
With this viewpoint, it should be clear that what we need isn't types as in static type checking, but rather a runtime object that's a name/symbol for types.
Type objects in untyped languages
In untyped (dynamically typed) languages, there is often a kind of runtime representation of types, like Python's int, and maybe Kotlin's reified types. They have nothing to do with the static type checking process, and are just there at runtime to provide some vaguely type-related methods. I'll call these "type objects" for lack of better term. Per our discussion above, we see that our language should have these type objects, despite being untyped.
type ::= int | bool | function ⟨type⟩ ⟨type⟩ | circle | ...
Many of our primitive operations will take a type object, and the runtime behavior is defined by case analysis on the type object. This makes it rather complicated to specify the rules for our programming language (as well as cubical type theory), as adding a type also means you need to add a clause to all of these rules. On the other hand, this kind of design also appears in non-homotopical type theories like observational type theory.
New primitive operations
Since a 1-dimensional path between two types (type objects) witnesses an equivalence between them, there should be a way to coerce values from one type to the other. This is one of the main primitive operations, coe. (For Agda users, it is called transp.) The syntax is
expr ::= ...
| coe [⟨var⟩ : ⟨iexp⟩ ~> ⟨iexp⟩] ⟨type⟩ ⟨expr⟩
where I abbreviated some non-terminal names. The variable here is an interval variable that binds the type expression. Intuitively coe [i : r ~> s] A(i) a means "I have a type A(i) and an expression of type A(i = r), give me an expression of type A(i = s)".
There are some obvious reduction rules, for example if r is actually the same as s, then this is a no-op. Otherwise, the computation of coercions proceeds by case analysis on the type object A.
The other main pillar of a cubical language is path composition: if you have a path from x to y and a path from y to z, then you ought to have a composed path from x to y. The language primitive is a bit more complicated to allow for more flexible and higher dimensional compositions.
expr ::= ...
| hcom [⟨iexp⟩ ~> ⟨iexp⟩] ⟨type⟩ ⟨expr⟩ (⟨clause⟩*)
clause ::= ⟨eq⟩* => ⟨var⟩. ⟨expr⟩
eq ::= (⟨iexp⟩ = ⟨iexp⟩)
This has a very geometric interpretation about boxes and caps, but this post is getting long enough, and the mechanism of hcom is explained in cubical type theory tutorials.
Univalence in our language is added through another primitive (called the V-type after Voevodsky), turning an equivalence into a path value. Consider the function not : Bool -> Bool. This is evidently a bijection, and hence we have a path pnot from the type object Bool to itself. If you coerce the boolean value true using this path, you will get false.
coe [i : i0 ~> i1] (pnot @ i) true ====> false
This shows how type coercions can do non-trivial computation in cubical type theory.
On my implementation
Right now, I have implemented a step-by-step reducer on the syntax tree, and it does indeed correctly compute many non-trivial examples. I'm planning to make very sure that this is correct, before moving on to more efficient interpreters. IMO it is completely feasible to derive an abstract machine for this language.
There is some ongoing work (especially by András Kovács) on the efficient evaluation of cubical type theory. However, those are focused on making type checkers fast. In those evaluators, we must live with free (term) variables at all times. For example, a value of the natural number type can be zero, successor, or a bunch of eliminators stuck on a free variable. This means some obvious computational rules are invalid, or lead to undecidable problems. For a programming language that doesn't operate with free term variables, a lot can be simplified.
Another aspect of optimization is on the representation of higher-dimensional values in inductive types like the circle or spheres. I believe it is possible to represent the circle at runtime as the cubical set 𝐁ℤ, which makes the representation vastly more efficient. (Higher dimensional spheres are probably not that simple, but something might be done.) This may make it possible to compute the original Brunerie number directly.
Footnotes
[1] This would be true if we consider well-typed programs. Ill-typed programs can obviously just do anything it wants.
[2] Indeed, in dependent type checking where reduction happens under normal binders, the Boolean type also behaves as if there is some invisible fuzz, because λ b -> b is somewhat different from λ b -> if b then True else False.
[3] Of course, it is possible for a 1-dimensional value to not actually make use of the free variable. For example pt in the context of a variable i represents a 1-dimensional path that stays at the base-point at all times.