A Quotient Inductive Type (QIT) is an inductive type that includes some additional equality rules. For example, the type
Int of integers can be defined as a QIT:
data Int Zero : Int Succ : Int -> Int Pred : Int -> Int SuccPred : (z : Int) -> Succ (Pred z) = z PredSucc : (z : Int) -> Pred (Succ z) = z end
This is a quotient inductive definition of
Int. There are three “point” constructors (
Pred) which construct all the
Int values, and two “path” constructors (
PredSucc) which construct additional equalities between the values of
Int. These capture the idea that incrementing then decrementing, or decrementing then incrementing, are the same as doing nothing.
To define a recursive function over Int, one must not only supply cases for the point constructors, but also for the path constructors. For example, suppose we want to write a function to double an Int. Then we need the usual cases for the constructed values:
Double : Int -> Int Double Zero = Zero Double (Succ z) = Succ (Succ (Double z)) Double (Pred z) = Pred (Pred (Double z))
But we also need cases for the constructed equalities:
Double (SuccPred z) = Succ (SuccPred (Pred (Double z))) @ SuccPred (Double z) Double (PredSucc z) = Pred (PredSucc (Succ (Double z))) @ PredSucc (Double z)
In this case,
Double (SuccPred z) must have type
Double (Succ (Pred z)) = Double z, and
Double (PredSucc z) must have type
Double (Pred (Succ z)) = Double z.
There’s a bit of overloading going on:
Double are used to transform both values and equalities. When
f is a function with domain
p : x = y is an equality in type
f p : f x = f y is the congruence generated by applying
p. I call this Congruence Overloading and it makes equalities easier to define. The
@ operator above is just transitivity.
[Some context: The “point constructor” and “path constructor” terminology comes from Homotopy Type Theory (HoTT). In HoTT, there is a similar thing called Higher Inductive Types (HITs). QITs are a version of HITs that is suitable when the type theory doesn’t have higher paths, only plain equalities. They have been used to construct a model of type theory by Altenkirch and Kaposi.]
The natural question for a category theorist is “what’s the dual”? Well the dual of induction is coinduction, and the dual of quotients is equalizers, so maybe we can look at Equaliser Coinductive Types (ECTs).
These are coinductive types, defined by a set of “destructors”, together with a set of “restrictions”, i.e. equalities out of the type. If we think of coinductive data (codata) as behaviour, an ECT is used to place restrictions on behaviour.
Here’s an example. A tape is an infinite sequence of values to the left and to the right. With a tape, you can peek at the current value, move the tape left, or move the tape right. Furthermore, going left and then right, or going right and then left, are the same as doing nothing at all. Thus we define an ECT:
codata Tape t Peek : Tape t -> t Left : Tape t -> Tape t Right : Tape t -> Tape t LeftRight : (x : Tape t) -> Left (Right x) = x RightLeft : (x : Tape t) -> Right (Left x) = x end
How do you construct a
Tape t element? By copattern matching its destructors and restrictions. For instance,
UniformTape returns a tape that is identical everywhere:
UniformTape : t -> Tape t Peek (UniformTape x) = x Left (UniformTape x) = UniformTape x Right (UniformTape x) = UniformTape x LeftRight (UniformTape x) = Refl (UniformTape x) RightLeft (UniformTape x) = Refl (UniformTape x)
PositionTape returns a
Tape Int that has value
i at position
PositionTape : Int -> Tape Int Peek (PositionTape z) = z Left (PositionTape z) = PositionTape (Pred z) Right (PositionTape z) = PositionTape (Succ z) LeftRight (PositionTape z) = PositionTape (PredSucc z) RightLeft (PositionTape z) = PositionTape (SuccPred z)
We used the quotient inductive structure of ints to introduce a tape. Likewise, we can use the equalizer coinductive structure of tapes to eliminate an int:
At : Int -> Tape t -> t At Zero x = Peek x At (Succ z) x = At z (Right x) At (Pred z) x = At z (Left x) At (SuccPred z) x = At z (RightLeft x) At (PredSucc z) x = At z (LeftRight x)
I hope these examples show how natural ECTs are, and how they capture some symmetries in relation to QITs. Indeed, the type
Tape t is isomorphic to
Int -> t, so if you have
Int you may as well have
Exercise. Show that
Tape t is isomorphic to
Int -> t.