Inductive Types with Path Constructors
Recall the previous post, in which we had higher dimensional paths (squares) and we can use path application to reduce their dimensions.
Recall our classical integer definition (click the
Int to see):
It's (kind of) bad as it's not symmetric -- Taking the number two as an example, positive two is
pos 2, while negative two is
negsuc 1. Proving the associative law on the addition operation of this integer is a pain in the ass due to the lack of symmetry (take a glance at here) on this integer (the definition is not symmetric, therefore the operations are naturally not symmetric as well).
We may want a symmetric version of integers -- imagine something like this:
but now we're having two zeros --
pos 0 and
neg 0. We define the classical integer not symmetrically intentionally to avoid the presence of two zeros, as mathematically we claim that zero is neither positive nor negative (we can say it in another way that there's positive zero but not negative).
Question: can we tell Agda that
pos 0 is equal to
neg 0? If so, the above definition will be usable!
The answers is yes yes yes, YES!
Recall that paths are:
Defined as functions whose domains are intervals and codomains are the endpoints' types
Treated as an equivalence relation
we can add constructors that are paths, to a datatype, like adding
pos 0 ≡ neg 0, which is a path (and if there's a definition of such path, it's gonna be a function from interval to Int), to
If we rewrite the type of
zro using a function type (while
zro itself has a path type) we get a constructor-ish type (whose return type is the type it's constructing):
zro returns an
Int and it's a constructor, we call it "path constructor". Before introducing some advanced properties of path constructors, we can already have a lot of fun stuffs like this:
What's special about path constructors is that they also constraint your pattern matching clauses when a datatype with path constructors appear at the left-hand-side of the pattern matching clauses. I'll go with an example -- the
succ function. When we write the
succ function for
Int, we'll need to pattern match over the path constructor:
Well, the rule for the path constructor case is that, we can return anything satisfying (taken this
Int for instance):
We may call this property for short "the path endpoints are respected".
and because both
succ (pos 0) and
succ (neg 0) equals to
pos 1, the only possible body for the
zro case will be
In fact, Agda's constraint solver is abled to solve some clauses of the function. We can write the above function with holes:
Load this blog in your Agda editor and try using "Auto" on them. Both holes can be solved.
Due to the presence of the path constructor whose type is
pos 0 ≡ neg 0, Agda knows
succ' (neg zero) is equal to
succ' (pos zero), where
succ' (pos x) is defined as
pos (suc x), applying the pattern with
pos zero results in
pos (suc zero), which is
Similarly, we can define the
Given the standard Integer definition, we can prove that the HIT (short for higher-inductive types, that are inductive types with path constructors) integer is isomorphic to it. To prove isomorphism under type theory, we need to provide two function that (in fact, only known to us) are inverse to each other, and prove this inverse relation (to convince Agda that they are inverse).
Int, we turn
neg ∘ suc:
On the other hand, due to the absence of path constructors in the standard definition, we map
zro i to
Let's try to prove the two functions are actually inverse to each other. One side of the isomorphism is trivial:
This is provable because our two patterns substitutes
Int->StdInt (StdInt->Int n) into
Int->StdInt (StdInt->Int (spos n)) and
Int->StdInt (StdInt->Int (nsuc n)), which unfolds to
spos n and
nsuc n, identical to the right-hand-side of the path in the return type.
Two cases of the other side of the isomorphism is a bit harder, I'll talk about'em one by one (Agda cell will follow below).
This clause is the first non-trivial case. If we substitute
Int->StdInt n with
neg zero, we get
spos 0, while substituting
StdInt->Int n with
spos 0 we get
pos 0. Therefore this clause has type
pos 0 ≡ neg 0, which is exactly the type of
Then we fill another trivial case.
The last case is also a bit complicated, we're introducing a lemma here for readability. Doing some simple substitution we can come up with the following signature:
This is a path with an interval variable in the context, which can be seen as a path between paths. The two sides of the paths are
pos 0 and
zro i, while
pos 0 (the
j = i0 side -- I mean the
x = y (
x is an interval variable,
i1) side by the
y endpoint of the path indexed by
x) is a constant value but
zro i (the
j = i1 side) has two different sides
pos 0 (the
i = i0 side) and
neg 0 (the
i = i1 side).
To solve a cubical problem, we observe it by graphing it:
This is exactly the
minSq introduced in the previous blog post (substituting
neg 0)! Recall that the
minSq is defined with the
min operator, we apply the same technique here:
Isomorphism and Path
A nice thing that the Cubical Type Theory can bring you is that you can create a path between isomorphic types. The theory behind is beyong the topic of this blog, but we can have a try on the library function based on the theory:
There's another integer type defined as HIT:
It's defined as one natural substracted by another. This is a brand new HIT, so I recommend readers to define some common operations for it and prove their properties to get familiar with this HIT.
We can imagine a lemma of which like this:
a ⊝ b is equal to
suc a ⊝ suc b, we can generalize this equality relation over an interval (which is exactly the
cancelDiamond function). But how do we prove this? Try graphing
cancelDiamond, we see a square, but it's neither a min nor a max square.
The answer will be revealed in the next blog post using new cubical operations.
This and the original version of this blog are licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.