[Agda] Agda's coinduction incompatible with initial algebras

[Martin Escardo]

In any category, for any endo-functor that has a both an initial algebra 
and a final co-coalgebra, there is a canonical map from the initial 
algebra to the final co-algebra. If this morphism is an isomorphism, 
then this is called a bi-free algebra (Peter Freyd originally called 
this a hermafrodite algebra). Freyd calls a category "algebraicly 
compact" if "every" endo-functor has a bi-free algebra.
(Domains with strict continuous maps are algebraicly compact with 
respect to continuous endo-functors.)

It seems that you have shown that this extension of Agda with 
co-inductive types is actually an algebraicly compact extension of Agda.

For the functor 1+(-), you get bi-natural numbers. By initiality, they 
have iteration, and by finality they have a point infty. Combining these 
two things, iterating infty-many times, you get fixed points, and so 
inhabitedness of all objects (by taking fixed points of identities).

(I am glad that I didn't define the co-natural numbers by co-induction 
in my Agda proof of their omniscience (I was tempted to). :-) )

Anyway, can anyone summarize exactly what is going wrong? I am not 
familiar with sized types etc. Can this be explained without too many 
technicalities or need to know "experimental features"?

Also: what was wrong with the older "codata"?

Moreover: then clearly the category of sets is not a model. Can one 
explain this directly, in order to see in an implementation-free way 
what goes wrong with the current proposal? I guess that there is no 
sensible way of interpreting sharp and flat. But why exactly?

Thanks!

Martin

On 04/10/11 17:26, Andreas Abel wrote:
> The only thing I am using sized types here is to establish a generic
> initial algebra for a functor F.
>
> If you believe that it makes sense for a functor F with functorial action
>
> map : {A B : Set} -> (A -> B) -> F A -> F B
>
> to have an initial algebra Mu F with
>
> introduction : inn : F (Mu F) -> Mu F
> elimination : iter : {A : Set} -> (F A -> A) -> Mu F -> A
> computation : iter s (inn t) = s (map (iter s) t)
>
> (I guess so far I am with the vast majority), and introduction is a
> *constructor*, then you can reconstruct my counterexample by setting F =
> co and there is no need for sized types whatsoever.
>
> Sized types come into the game because they are a means to persuade Agda
> that actually such initial algebras exist.
>
> So, I disagree (strongly) that sized types are to blame.
>
> The culprit is that co is treated as a functor. To fix the situation, we
> should no longer accept co as just a term of type Set -> Set (or the
> polymorphic version of it). If you look at the type of map for co,
>
> map : ∀ {A B : Set} → (A → B) → co A → co B
> map f a = ♯ f (♭ a)
>
> you see that co is applied to arbitrary sets A and B. There is no
> restriction in place that they may only be data types (or maybe record
> types).
>
> Treating co as special would solve the problem. I recall similar
> discussions on previous Agda meetings.
>
> Cheers,
> Andreas
>
> On 04.10.11 1:33 PM, Ulf Norell wrote:
>>
>>
>> On Tue, Oct 4, 2011 at 1:25 PM, Nils Anders Danielsson <nad at chalmers.se
>> <mailto:nad at chalmers.se>> wrote:
>>
>> On 2011-10-04 12:26, Andreas Abel wrote:
>>
>> I'd like to open a new round of false-golfing, below is my entry
>> to the
>> tournament. My favorite target is Agda's coinduction mechanism.
>> Partially it's flaws are known, but I cannot remember anyone
>> presenting
>> an outright proof of the absurdity.
>>
>>
>> Cool. However, you've only established that the present mechanism is
>> incompatible with sized types (and the usual kind of semantics of data
>> types, but this is not surprising). Can you do this without using sized
>> types?
>>
>>
>> I'm challenging the claim that sized types is not at fault. You don't
>> _need_ sized
>> types to work with initial algebras. Here's the standard trick
>> (specialising map
>> to iter):
>>
>> module NoInf where
>> -- Just an ordinary datatype.
>> data ∞ (A : Set) : Set where
>> ♯_ : A → ∞ A
>> ♭ : {A : Set} → ∞ A → A
>> ♭ (♯ x) = x
>>
>> data Mu : Set where
>> inn : ∞ Mu → Mu
>>
>> -- Not using coinduction. Passes termination checking (as expected).
>> iter : ∀ {A : Set} → (∞ A → A) → Mu → A
>> map-iter : ∀ {A : Set} → (∞ A → A) → ∞ Mu → ∞ A
>>
>> iter s (inn t) = s (map-iter s t)
>> map-iter f (♯ a) = ♯ iter f a
>>
>> However, trying the same trick on the coinductive version doesn't pass
>> termination/productivity:
>>
>> module Inf where
>> open import Coinduction
>> data Mu : Set where
>> inn : ∞ Mu → Mu
>>
>> -- Using coinduction. Doesn't pass (which it shouldn't).
>> iter : ∀ {A : Set} → (∞ A → A) → Mu → A
>> map-iter : ∀ {A : Set} → (∞ A → A) → ∞ Mu → ∞ A
>>
>> iter s (inn t) = s (map-iter s t)
>> map-iter s a = ♯ iter s (♭ a)
>> The problem, as I see it, is that sized types doesn't work with
>> coinduction, which we already knew.
>>
>> / Ulf
>