[Agda] Coinductive families

[Andreas Abel]

Ok, this works, but anyway, I think inductive records are doomed.

Eta-expansion does not terminate for inductive record like List so I  
guess there will be soon a check to rule them out.

On Oct 6, 2010, at 10:41 PM, Nicolas Pouillard wrote:

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

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/