[Agda] Coinductive families

[Andreas Abel]

On Oct 5, 2010, at 2:52 PM, Thorsten Altenkirch wrote:

> 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?


Not always, since record patterns are translated away sometimes.

Cheers,

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/