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 adata 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 xdata ↓=-Return {a : Set} : a -> a -> Set where
↓=-return : forall {x} -> ↓=-Return x xdata ↓=-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 fdata ↓-Return {a : Set} : a -> Set where
↓-return : forall {x} -> ↓-Return xdata ↓-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 finvoked-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 fcodata ↑-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 ∷ oneslength-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
_≤′′_
.