[Agda] Agda's coinduction incompatible with initial algebras

[Ulf Norell]

On Tue, Oct 4, 2011 at 1:25 PM, Nils Anders Danielsson <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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111004/7b26d60c/attachment.html