Coinduction

Coinductive Records

It is possible to define the type of infinite lists (or streams) of elements of some type A as follows:

record Stream (A : Type) : Type where
  coinductive
  field
    hd : A
    tl : Stream A

As opposed to inductive record types, we have to introduce the keyword coinductive before defining the fields that constitute the record.

It is interesting to note that it is not necessary to give an explicit constructor to the record type Stream.

Now we can use copatterns to create Streams, like one that repeats a given element a infinitely many times:

repeat : {A : Type} (a : A) -> Stream A
hd (repeat a) = a
tl (repeat a) = repeat a

We can also define pointwise equality (a bisimulation and an equivalence) of a pair of Streams as a coinductive record:

record _≈_ {A} (xs : Stream A) (ys : Stream A) : Type where
  coinductive
  field
    hd-≡ : hd xs ≡ hd ys
    tl-≈ : tl xs ≈ tl ys

Using copatterns we can define a pair of functions on Streams such that one returns the elements in the even positions and the other the elements in the odd positions:

even : ∀ {A} → Stream A → Stream A
hd (even xs) = hd xs
tl (even xs) = even (tl (tl xs))

odd : ∀ {A} → Stream A → Stream A
odd xs = even (tl xs)

split : ∀ {A} → Stream A → Stream A × Stream A
split xs = even xs , odd xs

as well as a function that merges a pair of Streams by interleaving their elements:

merge : ∀ {A} → Stream A × Stream A → Stream A
hd (merge (xs , ys)) = hd xs
tl (merge (xs , ys)) = merge (ys , tl xs)

Finally, we can prove that merge is a left inverse for split:

merge-split-id : ∀ {A} (xs : Stream A) → merge (split xs) ≈ xs
hd-≡ (merge-split-id _)  = refl
tl-≈ (merge-split-id xs) = merge-split-id (tl xs)

Coinductive Record Constructors

It is possible to give an explicit constructor to coinductive record types like Stream:

record Stream' (A : Type) : Type where
  coinductive
  constructor cons
  field
    hd : A
    tl : Stream' A

However, this constructor cannot be pattern-matched:

-- Get the third element of a stream
third : ∀{A} → Stream' A → A

-- Not allowed:
-- third (cons _ (cons _ (cons x _))) = x

Instead, you can use the record fields as projections:

third str = str .tl .tl .hd

The constructor can be used as usual in the right-hand side of definitions:

-- Prepend a list to a stream
prepend : ∀{A} → List A → Stream' A → Stream' A
prepend [] str = str
prepend (a ∷ as) str = cons a (prepend as str)

However, it doesn’t count as ‘guarding’ for the productivity checker:

-- Make a stream with one element repeated forever
cycle : ∀{A} → A → Stream' A

-- Does not termination-check:
-- cycle a = cons a (cycle a)

Instead, you can use copattern matching:

cycle a .hd = a
cycle a .tl = cycle a

It is also possible to use copatterns in a Pattern lambda:

cycle' : ∀{A} → A → Stream' A
cycle' a = λ where
  .hd → a
  .tl → cycle' a

For more information on these restrictions, see this pull request, and this commit.

The ETA pragma

Agda does not permit the eta-equality directive in coinductive record declarations, since η for coinductive types is unsafe in general and can make the type checker loop. For instance, the following code would lead to infinite η expansion when checking test:

record R : Type where
 coinductive; eta-equality
 field force : R
open R

foo : R
foo .force .force = foo

test : foo .force ≡ foo
test = refl

If you know what you are doing, you can override Agda and force a coinductive record to support η via the ETA pragma.

{-# ETA R #-}

Note however that ETA is not allowed in --safe mode, for reasons mentioned above. This pragma is intended for experiments and not recommended in production code. It might be removed in future versions of Agda.