Quotient Inductive Types & Their Dual

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 (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:

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)

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.

Advertisements

2 thoughts on “Quotient Inductive Types & Their Dual

  1. 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.

    Like

    • 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:

      codata A
        B :  A -> Int
        C : A -> A
        D : (x : A) -> B x = B (C x)
      end

      But this is an ECT:

      codata A
          B : A -> Int
          C : A -> A
          D : (x : A) -> x = C x
      end

      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

      Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s