[Agda] Agda's coinduction incompatible with initial algebras

[Andreas Abel]

On 04.10.11 7:33 PM, Ulf Norell wrote:
> On Tue, Oct 4, 2011 at 6:26 PM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto: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.

No, co is a functor because Agda treats it as monotone (preserving 
strict positivity) and because I can program the map function.  No sized 
types involved here.

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

Yes.  But iter can be justified for *any* functor.  There is tons of 
models for this, like categories, impredicative encodings, etc.  Yet to 
exploit the functoriality to its fullness *in Agda*, meaning to 
construct the initial algebra, I need, at least currently, sized types. 
  Someone might extend Agda by a native check for functoriality and 
accept Mu and iter without sized types.  And then letting co be a 
functor blows the system.

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

I hope I have explained myself properly now.  To reveal the 
inconsistency, you need initial algebras with a *constructor* inn. 
Nothing wrong about that.  In current Agda, you get initial algebras via 
sized types.  Nothing wrong with that either.

That Agda's coinduction without sized types is (maybe) consistent is no 
more than a coincidence for me.  At least it does not scale to 
extensions, such as generic initial algebras.

Cheers,
Andreas

-- 
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/