[Agda] Agda's coinduction incompatible with initial algebras

[Andreas Abel]

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

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/