[Agda] Coinductive families

[Thorsten Altenkirch]

On 7 Oct 2010, at 22:19, Andreas Abel wrote:

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

I hope not. As I have said it is very strange not to be allowed to use records in recursive definitions.

I'd rather get rid of eta equality.

Thorsten


> 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/
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101007/e4b3c79d/attachment-0001.html