[Agda] Coinductive families

[Thorsten Altenkirch]

On 5 Oct 2010, at 12:42, Dan Doel wrote:

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

But if I replace my record with the isomorphic data type, then it is fine.

data List (A : Set) : Set where
  list : (isCons : Bool)
       → (hd : T isCons → A)
       → (tl : T isCons → List A)
       → 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

Could we not view record types as data types with one constructor?

T.


> 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