# “General Recursion using Coinductive Monad” Got Right

In the previous post I talked about encoding general recursion in Agda using a coinductive monad. One oddity was that Agda does not automatically unfold coinductive definitions, and a solution was to manually unfold them when we need. Therefore, instead of proving, for example, for coinductively defined `f`:

```n<k⇒fkn↓=k : forall k n -> n<′′ k -> f k n ↓= k ```

we prove a pair of (possibly mutually recursive) properties:

```n<k⇒⟨fkn⟩↓=k : forall k n -> n<′′ k -> unfold (f k n) ↓= k n<k⇒fkn↓=k : forall k n -> n <′′ k -> f k n ↓= k ```

where `unfold` (a user-defined function) performs the unfolding, and the second property follows from the first by `≡-subst` and the fact that `unfold (f k n) ≡ f k n`.

While the use of `unfold` appears to be a direct work around, one may argue that this is merely treating the symptom. To resolve this and some other oddities, Anton Setzer argued in his letter “Getting codata right” (hence the title of this post) to the Agda mailing list that we should go back to a category theoretical view of codata, and Dan Doel soon successfully experimented the ideas. The following, however, are based on my current understanding of their work, which may not be matured yet.

### What `codata` Really Is

Inductive datatypes are defined by describing how a value is constructed. The following inductive definition:

```data List (a : Set) : Set where    [] : List a    _∷_ : a -> List a -> List a ```

states that `[]` is a list and, given an element `x` and a list `xs`, one can construct a list `x ∷ xs`.

Coinductive datatypes, on the other hand, are specified by how a covalue can be observed. The following definition of stream:

```codata Stream (a : Set) : Set where    [] : Stream a    _∷_ : a -> Stream a -> Stream a ```

while looking almost identical to `List` apart from the use of keyword `codata`, is in fact a definition very different from that of `List` in nature. Setzer suggests seeing it as a short-hand for the following collection of definitions (in Setzer’s proposed notation but my naming scheme):

`mutual`

```  coalg Stream (a : Set) : Set where     _* : Stream a -> StObserve a ```

``` data StObserve (a : Set) : Set where     empty : StObserve a     nonempty : a -> Stream a -> StObserve a ```

Notice that `Stream a` appears in the domain, rather than the range of `_*` because we are defining a coalgebra and `_*` is a deconstructor. My interpretation is that `_*` triggers an obserivation. Given a stream `xs`, an observation `xs *` yields two possible results. Either it is `empty`, or `nonempty x xs'`, in the latter case we get its head `x` and tail `xs'`. The stream “constructors”, on the other hand, can be defined by:

```[] : {a : Set} -> Stream a [] * = empty```

``` ```

```_∷_ : {a : Set} -> a -> Stream a -> Stream a (x ∷ xs) * = nonempty x xs ```

which states that `[]` is the stream which, when observed, yields `empty` and `x ∷ xs` is the stream whose observation is `nonempty x xs`.

A coinductive definition:

`f x ~ e`

is a shorthand for

`(f x)* = e *`

That is, `f x` defines an coinductive object whose observation shall be the same as that of `e`. Setzer proposes explicit notation (e.g. `~ (x ∷ xs)`) for pattern matching covalue. Back to current Agda, we may seen pattern matching covalue as implicitly applying `_*` and pattern-match the result. For example, the Agda program:

``` f : {a : Set} -> Stream a -> ... f [] = ... f (x ∷ xs) = ... ```

can be seen as syntax sugar for:

```f : {a : Set} -> Stream a -> ... f ys with ys * ... | empty = ... ... | nonempty x xs = ... ```

### Covalue-Indexed Types

What about (co)datatypes that are indexed by covalues? Take, for example, the codatatype `Comp a` for possibly non-terminating computation, define in my previous post:

```codata Comp (a : Set) : Set where    return : a -> Comp a    _⟩⟩=_ : Comp a -> (a -> Comp a) -> Comp a ```

and the datatype `_↓=_` claiming that certain computation terminates and yields a value:

```data _↓=_ {a : Set} : Comp a -> a -> Set where    ↓=-return : forall {x} -> (return x) ↓= x    ↓=-bind : forall {m f x y} ->          m ↓= x -> (f x) ↓= y -> (m ⟩⟩= f) ↓= y ```

What is the definition actually trying to say? Given `m : Comp a` and `x`, `m ↓= x` is a type. In the case that `m` is `return x`, there is an immediate proof, denoted by `↓=-return`, of `(return x) ↓= x` (that is, `return x` terminates with value `x`). For the case `m ⟩⟩= f`, we can construct its termination proof, denoted by constructor `↓=-bind`, from termination proofs of `m` and `f x`. Setzer suggests the following definition, which corresponds more literally to the verbal description above:

```mutual  _↓=_ : {a : Set} -> Comp a -> a -> Set  return x ↓= y = ↓=-Return x y  (m ⟩⟩= f) ↓= x = ↓=-Bind m f x ```

```  data ↓=-Return {a : Set} : a -> a -> Set where    ↓=-return : forall {x} -> ↓=-Return x x ```

``` data ↓=-Bind {a : Set} : Comp a -> (a -> Comp a) -> a -> Set where    ↓=-bind : forall {m f x y} ->        m ↓= x -> (f x) ↓= y -> ↓=-Bind m f y```

Now `↓=-return` and `↓=-bind` are the only constructors of their own types, and `_↓=_` maps `Comp a` typed covalues to their termination proofs according to their observations. Notice that `↓=-Return` is exactly the built-in identity type `_≡_`: `return x` terminates with `y` if and only if `x` equals `y`.

For more examples, compare the valueless termination type `_↓` in the previous post:

```data _↓ {a : Set} : Comp a -> Set where   ↓-return : forall {x} -> (return x) ↓   ↓-bind : forall {m f} ->       m ↓ -> (forall x -> m ↓= x -> f x ↓) -> (m ⟩⟩= f) ↓ ```

and its “correct” representation:

`mutual`

```  data _↓ : {a : Set} -> Comp a -> Set     return x ↓ = ↓-Return x     (m ⟩⟩= f) ↓ = ↓-Bind m f  data ↓-Return {a : Set} : a -> Set where     ↓-return : forall {x} -> ↓-Return x ```

``` data ↓-Bind {a : Set} : Comp a -> (a -> Comp a) -> Set where     ↓-bind : forall {m f} ->      m ↓ -> (forall x -> m ↓= x -> f x ↓) -> ↓-Bind m f```

Here is a non-recursive example. The datatype `Invoked-By` characterising sub-computation relation is written:

```data Invoked-By {a : Set} : Comp a -> Comp a -> Set where   invokes-prev : forall {m f} -> Invoked-By m (m ⟩⟩= f)   invokes-fun : forall {m f x} -> m ↓= x -> Invoked-By (f x) (m ⟩⟩= f) ```

Like above, we define a function for dispatching `Comp a` covalues according to their observation:

```data Invoked-By-Bind {a : Set} : Comp a -> Comp a -> (a -> Comp a) -> Set where   invokes-prev : forall {m f} -> Invoked-By-Bind m m f   invokes-fun : forall {m f x} -> m ↓= x -> Invoked-By-Bind (f x) m f```

``` ```

```invoked-by : {a : Set} -> Comp a -> Comp a -> Set invoked-by m (return x) = ⊥ invoked-by m (n ⟩⟩= f) = Invoked-By-Bind m n f ```

Indeed, `return x` consists of no sub-computations, therefore `invoked-by m (return x)` is an empty relation. On the other hand, there are two possibilities `invoked-by m (n ⟩⟩= f)`, represented by the two cases of `Invoked-By`.

### Termination Proof

The lengthy discussion above is of more than pedantic interest. While the mutually exclusive indexed type definitions may look rather confusing to some, the effort pays off when we prove properties about them. Redoing the exercises in the previous post using the new definitions, the first good news is that the definitions of `Safe`, `↓-safe`, `eval-safe`, and `eval` stay almost the same. Second, we no longer have to split the termination proofs into pairs.

Take for example the McCarthian Maximum function:

```f : ℕ -> ℕ -> Comp ℕ f k n with k ≤′′? n ... | inj₁ k≤n ~ return n ... | inj₂ n<k ~ f k (suc n) ⟩⟩= \x -> f k x ```

Its termination proof is based on two lemmas, together they state that `f k n` terminates with the maximum of `k` and `n`:

```k≤n⇒fkn↓=n : forall k n -> k ≤′′ n -> f k n ↓= n k≤n⇒fkn↓=n k n k≤n with k ≤′′? n ... | inj₁ _ = ↓=-return ... | inj₂ n<k = ⊥-elim (¬[m<n∧n≤m] (n<k , k≤n)) ```

``` ```

```n<k⇒fkn↓=k : forall k n -> n <′′ k -> f k n ↓= k n<k⇒fkn↓=k k n n<k with k ≤′′? n n<k⇒fkn↓=k k n n<k | inj₁ k≤n = ⊥-elim (¬[m<n∧n≤m] (n<k , k≤n)) n<k⇒fkn↓=k ._ n _ | inj₂ ≤′′-refl =     ↓=-bind {_}{f (suc n) (suc n)}{\x -> f (suc n) x}{suc n}       (k≤n⇒fkn↓=n (suc n) (suc n) ≤′′-refl)       (k≤n⇒fkn↓=n (suc n) (suc n) ≤′′-refl) n<k⇒fkn↓=k ._ n ≤′′-refl | inj₂ (≤′′-step 2+n≤n) =     ⊥-elim (¬1+n≤n 2+n≤n) n<k⇒fkn↓=k k n (≤′′-step 2+n≤k) | inj₂ (≤′′-step _) =     ↓=-bind {_}{f k (suc n)}{\x -> f k x}{k}       (n<k⇒fkn↓=k k (suc n) 2+n≤k)       (k≤n⇒fkn↓=n k k ≤′′-refl) ```

### Divergence Proof

For some reason (lack of space, perhaps?), Megacz did not talk about divergence in his PLPV paper. For completeness, let us give it a try.

A `return` command always terminates. On the other hand, `m ⟩⟩= f` diverges if either `m` does, or `m ↓= x` and `f x` diverges. This is expressed as:

```mutual   _↑ : {a : Set} -> Comp a -> Set   return x ↑ = ⊥   (m ⟩⟩= f) ↑ = ↑-Bind m f```

``` ```

``` codata ↑-Bind {a : Set} : Comp a -> (a -> Comp a) -> Set where    ↑-prev : forall {m f} -> m ↑ -> ↑-Bind m f    ↑-fun : forall {m f} ->         (forall x -> m ↓= x -> f x ↑) -> ↑-Bind m f ```

For an example, the following is a proof that `length` diverges when applied to an infinite stream:

```length : {a : Set} -> Stream a -> Comp ℕ length [] ~ return zero length (x ∷ xs) ~ length xs ⟩⟩= \n -> return (suc n)```

``` ones : Stream ℕ ones ~ 1 ∷ ones ```

```length-ones↑ : length ones ↑ length-ones↑ ~ ↑-prev {_}{length ones} length-ones↑ ```

The implicit argument `length ones` must be given. Otherwise `length-ones↑` fails to typecheck when the file is loaded, although it does typecheck when `length-ones↑` was stepwisely constructed using the “Give” command. I do not know whether it is a bug in Agda.