Codatatypes and comatching

A codatatype is superficially similar to a record type: it has a list of fields (which in this case we sometimes call methods), each with a type, which are projected out (or “called”) using the same syntax x .method. The primary differences are:

  1. Codatatypes can be (co)recursive: the output type of each method can involve the codatatype itself. (Such occurrences ought to be strictly positive, but currently there is no check for that. In fact, there is not yet even a check that rules out recursion in record types, but there will be.)

  2. Codatatypes do not satisfy η-conversion (this being undecidable in the recursive case).

  3. Elements of codatatypes are defined by comatches, which are like tuples but can be recursive, use a syntax more akin to matches, and are restricted to case trees.

Defining codatatypes

Here is a corecursive definition of the codatatype of infinite streams:

def Stream (A:Type) : Type ≔ codata [
| x .head : A
| x .tail : Stream A
]

That is, we use brackets and bars instead of parentheses and commas. Moreover, instead of writing field names like variables as in a record type, we write them as method calls applied to a variable. This variable is then bound in the body to belong to the codatatype, and the values of previous fields are accessed through it. For instance, a codata version of Σ-types would be written

def codata-Σ (A : Type) (B : A → Type) : Type ≔ codata [
| x .fst : A
| x .snd : B (x .fst)
]

It is often helpful to think of a codatatype as akin to an interface in an object-oriented programming language, in which case the variable x is like the this or self pointer by which an object refers to itself. Of course an interface in a simply-typed language does not need a self-pointer to specify the types of its methods, but in a dependently typed language it does. In higher-dimensional type theories, the presence of this variable can be used in other ways than simply accessing previously declared methods, such as in the definition of semi-simplicial types using Displayed coinductive types.

Copattern matching

Elements of coinductive types are introduced by comatches, which are like tuples except for the syntax and the fact that they can be (co)recursive:

def Fibonacci (a b : ℕ) : Stream ℕ ≔ [
| .head ↦ a
| .tail ↦ Fibonacci b (ℕ.plus a b)
]

In addition, unlike tuples, comatches are a part of case trees but not of ordinary terms. Thus, they never evaluate to anything until a method is called. This is essential to ensure termination in the presence of corecursion; otherwise Fibonacci 1 1 would spin forever computing the entire infinite sequence. (It is also why codatatypes do not have η-conversion.) It is often helpful to think of a constant defined by comatching as an (immutable) object implementing an interface, with the parameters of that constant being its “private member variables”.

(As a bit of syntactic trivia, note that [] is ambiguous: it could denote either a pattern-matching lambda on a datatype with no constructors, or a copattern-match into a codatatype with no methods. Fortunately, since both possibilities are checking rather than synthesizing, and function-types and codatatypes are disjoint, the ambiguity is resolved by bidirectional typechecking.)