[Agda] Coinductive families

[Nicolas Pouillard]

On Wed, 6 Oct 2010 11:03:08 +0200, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 
> On Oct 5, 2010, at 5:29 PM, Nils Anders Danielsson wrote:
> 
> > On 2010-10-05 14:14, Andreas Abel wrote:
> >> Currently records are hybrids, because we have record patterns. If  
> >> all
> >> record patterns could be translated away, we could understand  
> >> records in
> >> terms of &. But currently we allow record patterns that cannot be
> >> translated away, such as where record patterns are mixed with data
> >> constructor patterns.
> >
> > I'm fairly certain that we can translate away these patterns, but  
> > there
> > is no immediate need to do so, because the translation would be
> > observationally indistinguishable from what we generate now (modulo  
> > any
> > bugs).
> 
> 
> How would you translate away the patterns in Thorsten's example?
> 
> record List (A : Set) : Set where
>    constructor list
>    field
>      isCons : Bool
>      hd : T isCons → A
>      tl : T isCons → List A
> 
> 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

[...]

> Anyway, for now the termination checker rejects all versions of append  
> given here,  shout if you disagree!

One may consider this as cheating but by boxing the recursive occurence
of (List A) one can please the termination checker:

data Box (A : Set) : Set where
  box : A → Box A

record List (A : Set) : Set where
  constructor list
  field
    isCons : Bool
    hd : T isCons → A
    tl : T isCons → Box (List A)

open List

append : ∀ {A} → List A → List A → List A
append l bs with isCons l | hd l | tl l
... | false | _ | _ = bs
... | true  | h | t with t _
...                 | box t' = list true h (λ _ → box (append t' bs))

By replacing Box by ∞ one get CoList.

Best regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr