{-# OPTIONS --guardedness #-} -- this flag is needed for negative coinduction.
-- Documentation: Enable constructor-based guarded corecursion
module Coinductive where      -- top-level module, must have same name as file.

Preliminaries

A fresh Agda module starts with nothing (not even a notion of equality), so we need to import some things that we don’t want to implement ourselves.

The syntax is open import <module> using <list of things you want to use>.

  open import Data.Nat using (ℕ; zero; suc)
  open import Data.Bool using (Bool; true; false)
  open import Data.List using (List; []; _∷_)
  open import Relation.Binary.PropositionalEquality using (_≡_; refl) -- this is the equality type, defined as expected (inductive datatype with constructor refl)

There are two ways to define corecursive types, they don’t really have names but one is usually called the old way and one the new way. I would say that the old way corresponds to positive coinductive types and the new way to negative ones.

Before we look at positive coinductive types here’s a disclaimer from the documentation:

This is the old way of coinduction support in Agda. You are advised to use Coinductive Records instead.

Positive coinductive types

The documentation describes (positive) corecursion as follows:

Values of coinductive types can be constructed using corecursion, which does not need to terminate, but has to be productive. As an approximation to productivity the termination checker requires that corecursive definitions are guarded by coinductive constructors.

So a similar notion of guardedness as in Coq, but we also need to use this funny musical notation to denote corecursive occurences:

  module MusicalNotation where
    postulate
      ∞  : ∀ {a} (A : Set a) → Set a   -- denotes suspended computation of type A
      ♯_ : ∀ {a} {A : Set a} → A → ∞ A -- delay
      ♭  : ∀ {a} {A : Set a} → ∞ A → A -- force

Note: I use modules here to separate different topics, they can be understood like the Section mechanism in Coq, so if I dont write open MusicalNotation these postulates will be invisible in the following.

These postulates are actually contained in the stdlib, so we shouldn’t define them ourselves.

  module Positive where
    open import Codata.Musical.Notation using (∞; ♯_; ♭)

Defining streams in a positive corecursive way should look familiar to Haskell programmers, with one small caveat: the corecursive argument of the constructor has to be marked with ∞.

    data stream (A : Set) : Set where
      cons : A → ∞ (stream A) → stream A -- ∞ marks that the stream is a coinductive argument

As in Coq we can define hd and tl and some functions.

    hd : ∀ {A : Set} → stream A → A
    hd (cons h _) = h
    tl : ∀ {A : Set} → stream A → stream A
    tl (cons _ t) = ♭ t -- t has type `∞ (stream A)` so we need to force it to type `stream A`

    zeroes : stream ℕ
    zeroes = cons  (♯ zeroes) -- the corecursive call to zeroes has to be marked (actually lifted should be the correct word) with ♯ 

    approx : ∀ {A : Set} → stream A → ℕ → List A
    approx s zero = []
    approx (cons h t) (suc n) = h ∷ approx (♭ t) n -- here we need to force t again

    map : ∀ {A B : Set} → (A → B) → stream A → stream B
    map f (cons h t) = cons (f h) (♯ (map f (♭ t))) -- and here we need to force t and lift the result of map

    -- mutual corecursion
    mutual
      trues-falses : stream Bool
      falses-trues : stream Bool
      
      trues-falses = cons true (♯ falses-trues)
      falses-trues = cons false (♯ trues-falses)

Coinduction with positive coinductive types

Let’s look at the same example, two streams containing only 1.

    ones : stream ℕ
    ones = cons  (♯ ones)
    ones' : stream ℕ
    ones' = map suc zeroes

As in Coq the initial attempt of proving equality fails, ≡ is the (not strictly builtin) type of equality with the constructor refl.

    -- ones-eq-fail : ones ≡ ones'
    -- ones-eq-fail = refl -- same as reflexivity. 
    -- > "error ... when checking that the expression refl has type ones ≡ ones'|

Instead we need a notion of stream-equality that is defined much like in Coq, with the added use of ♭ and ∞.

    data _≈_ {A : Set} : stream A → stream A → Set where
      ≈-cons : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → cons x xs ≈ cons x ys -- this business of forcing and lifting is not intuitive to me

The proof is then done by using the constructor of ≈ and calling ones-eq coinductively.

    ones-eq : ones ≈ ones'
    ones-eq = ≈-cons  (♯ ones-eq)

Negative coinductive types

Negative coinductive types are defined via coinductive records (like in Coq, but syntactically more clear imo). This is the intended way to do coinduction in Agda right now.

  module Negative where
    record stream (A : Set) : Set where
      coinductive
      field
        hd : A
        tl : stream A
    open stream -- make the destructors accessible

Now we can define functions corecursively exactly like we did in ThProg!

    zeroes : stream ℕ
    hd zeroes =  
    tl zeroes = zeroes

    map : ∀ {A B : Set} → (A → B) → stream A → stream B
    hd (map f s) = f (hd s)
    tl (map f s) = map f (tl s)

    -- mutual corecursion again
    mutual
      trues-falses : stream Bool
      falses-trues : stream Bool

      hd trues-falses = true
      tl trues-falses = falses-trues
      hd falses-trues = false
      tl falses-trues = trues-falses

Coinduction with negative coinductive types

Let’s proof the same thing as before.

    ones : stream ℕ
    hd ones = 
    tl ones = ones

    ones' : stream ℕ
    ones' = map suc zeroes

    record _≈_ {A : Set} (s t : stream A) : Set where
      coinductive
      field
        hd-≈ : hd s ≡ hd t
        tl-≈ : tl s ≈ tl t
    open _≈_

The proof is then wonderfully simple and has the same structure as coinductive proofs had in ThProg (i.e. you need to show equality for heads and bisimilarity for tails).

    ones-eq : ones ≈ ones'
    hd-≈ ones-eq = refl      -- case where you have to show that the heads are equal
    tl-≈ ones-eq = ones-eq   -- case where you need to show that the tails are bisimilar/"stream-equal"