[Agda] Coinductive families

[Dan Doel]

On Tuesday 05 October 2010 6:35:50 am Thorsten Altenkirch wrote:

> Btw, when trying to define append
> 
> append : ∀ {A} → List A → List A → List A
> append (list true h t) bs = list true h (λ _ → append (t _) bs)
> append (list false _ _) bs = bs
> 
> the termination checker complains. I am not sure why, since (t _) is
> smaller than (list true h t), isn't it?

This theoretically rewrites to something like:

  append l bs with isCons l | hd l | tl l
  ... | true  | h | t = list true h (\_ -> append (t _) bs)
  ... | false | _ | _ = bs

and with the projection rule:

  t = tl l <= l

so, no; it is merely not-bigger (or, possibly, actually bigger if your version 
is old enough; not sure). This is the same rule used to disqualify:

  record R : Set where
    constructor c
    field
      p : R

  foo : R -> R
  foo (c r) = foo r

which *actually* translates internally to:

  foo : R -> R
  foo r = foo (p r)

which won't normalize. append can't be translated, I think, because the match 
on isCons blocks translation to projections (the translation I gave is 
probably a bit much to expect of the checker), but Andreas changed the rule 
for pattern matching on record constructors to make the two consistent, I 
think.

-- Dan