[Agda] Coinductive families

[Thorsten Altenkirch]

On 6 Oct 2010, at 13:21, Nils Anders Danielsson wrote:

> On 2010-10-06 10:03, Andreas Abel wrote:
>> How would you translate away the patterns in Thorsten's example?
> 
> I think recursive records should be disallowed, so this example is
> irrelevant (from my perspective).

This would be strange. There are structures which clearly have a record flavour and which show up in the middle of a mutual recursive definition and then I am not allowed to use records? There is also the potential discontinuity: you are start with a non-recursive structure and then make it recursive and now you have to rewrite all your code? This is precisely what happened to me when moving from setoids to globular sets, the latter are a recursive generalisation of the former - why should I be able to use records for one and not the other?

I think it should be clear that eta expansion stops at recursive use of types. In PiSigma this is very clear due to the use of rec. Something like this may also work for Agda.

Cheers,
Thorsten

> 
> However, let's see if we can perform the translation using the case
> trees that Agda uses internally.
> 
>> 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
> 
> Case tree translation (note that this isn't valid Agda surface syntax,
> and doesn't type check without something like smart case):
> 
>  append : ∀ {A} → List A → List A → List A
>  append as bs =
>    case as of
>      list b h t → case b of
>        true  → list true h (λ _ → append (t _) bs)
>        false → bs
> 
> After record patterns have been removed:
> 
>  append : ∀ {A} → List A → List A → List A
>  append as bs =
>    case isCons as of
>      true  → list true (hd as) (λ _ → append (tl as _) bs)
>      false → bs
> 
> With your recent changes to the termination checker the first variant of
> append is accepted only if the last variant is OK, if I understand
> things correctly.
> 
> -- 
> /NAD
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda