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:

dataInt Zero : Int Succ : Int -> Int Pred : Int -> Int SuccPred : (z : Int) -> Succ (Pred z) = z PredSucc : (z : Int) -> Pred (Succ z) = zend

This is a quotient inductive definition of `Int`

. There are three “point” constructors (`Zero`

, `Succ`

, and `Pred`

) which construct all the `Int`

values, and two “path” constructors (`SuccPred`

and `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: `Succ`

,`Pred`

, and `Double`

are used to transform both values and equalities. When `f`

is a function with domain `A`

and `p : x = y`

is an equality in type `A`

, then `f p : f x = f y`

is the congruence generated by applying `f`

to `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:

codataTape 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) = xend

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)

And `PositionTape`

returns a `Tape Int`

that has value `i`

at position `i`

:

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 `Tape`

.

**Exercise.** Show that `Tape t`

is isomorphic to `Int -> t`

.

Interesting post! One thing I don’t quite get, though: it seems to me that the novel thing in your definition of

`Tape`

is dependency on the value being destructed. The syntax used here would seem to allow for fields with type`(x : Tape) -> P x`

for arbitrary`P`

. So I’m left wondering what it has to do with equality. I would have expected a higher coinductive type to define extra destructors of paths, though I don’t know whether that can be justified.All that said, the parallel between Nat/Stream and Int/Tape is clear, so this must be right.

Minor:

`UniformTape`

definition contains a few mentions of`Uniform`

, which should be`UniformTape`

.LikeLike

Hi James, thank you for the reply and for spotting that mistake.

The novel thing about ECTs is not the dependency on the value being constructed, because that’s quite typical for dependently-typed records and for codata more generally. The thing ECTs bring is the ability to destruct into the equality type of the type being defined. The natural notion of equality for coinductive types is bisimulation, so there is something tricky happening — we are destructing a value into a bisimulation over related values (i.e. values accessible via other destructors).

For example, this isn’t an ECT:

But this is an ECT:

Although they are morally equivalent.

I don’t really have an opinion on what “Higher Coinductive Types” should be. I avoid that terminology here because it’s associated with HoTT, and I’m definitely going for a more OTT-like theory, where equality is propositional. In this context, it doesn’t make sense to introduce extra destructors at the path level because equality is propositional. But it also seems to me that the duality between quotients and equalizers would make Higher Coinductive Types be similar to ECTs, in that they would allow one to destruct values into paths over related values.

Thanks,

Fran

LikeLike