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

Programs

• CoinductiveRecursionRight.agda: the main program.
• DownwardLeq.agda: definition and properties of _≤′′_.