[Agda] Agda's coinduction incompatible with initial algebras

[Ulf Norell]

On Tue, Oct 4, 2011 at 11:18 PM, Dan Doel <dan.doel at gmail.com> wrote:

> On Tue, Oct 4, 2011 at 2:07 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
> wrote:
> > But the principle of sized types can also be applied to coinduction,
> under
> > the interpretation of "size" as "depth", i.e., number of guarding
> > constructors.  Corecursion is sound if it increases the guardedness of
> the
> > result in the body surrounding the recursive call (rather than increasing
> > the size of the function argument as in the recursion case).
> >
> > Yet that does not happen here.
>
> It doesn't appear to happen anywhere to me. The sized type checker
> doesn't seem to recognize Agda's coinductive definitions at all
> (currently). You just get whatever is better at the time. If you write
> an obviously guarded corecursive definition, it's accepted by the
> guardedness checker. If you write a size-decreasing function, it's
> also accepted, even though the type may be coinductive due to the
> presence of the built-in.
>
> So, one could probably argue that the bug is in assuming that Mu F is
> an initial algebra without knowing what F is. Knowing only that it is
> a functor is not enough in Agda. You need to know whether or not it's
> a magic functor that turns things into codata.
>

This. The problem isn't allowing co to be a functor, you can do this with
only sanctioned uses of co (only applied to recursive occurrences of the
type(s) we are defining):

  -- Streams of alternating ⊤ and A
  data Stream′ A : Set
  data Stream A : Set

  data Stream′ A where
    _∷_ : A → co (Stream A) → Stream′ A
  data Stream A where
    _∷_ : ⊤ → co (Stream′ A) → Stream A

  map  : ∀ {A B : Set} → (A → B) → Stream A → Stream B
  map′ : ∀ {A B : Set} → (A → B) → Stream′ A → Stream′ B
  map f  (_ ∷ xs) = _ ∷ ♯ map′ f (♭ xs)
  map′ f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

  boos : Stream (Mu Stream ∞)
  boo  : Mu Stream ∞
  boos = _ ∷ (♯ (boo ∷ ♯ boos))
  boo = inn boos

  hd′ : ∀ {A} → Stream′ A → A
  hd′ (x ∷ _) = x

  hd : ∀ {A} → Stream A → A
  hd (_ ∷ xs) = hd′ (♭ xs)

  false : ⊥
  false = iter map hd boo

Basically, the way things currently work in Agda, Mu will be
inductive or coinductive depending on the choice of F, but the
sized types machinery treats it as always inductive.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111005/cd405336/attachment-0001.html