[Agda] Agda's coinduction incompatible with initial algebras

[Ulf Norell]

On Tue, Oct 4, 2011 at 6:26 PM, Andreas Abel <andreas.abel at ifi.lmu.de>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)
>

But the thing is, the only thing that lets you treat co as a functor is
sized types. Termination of iter relies crucially on the fact that the map
operation is applying it's first argument to things that are smaller than
the second argument. That simply doesn't hold for map on co, which is
revealed if you actually try to get it past the termination checker without
resorting to sized types.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111004/8d9e1954/attachment.html