[Agda] Newbie questions after reading Dependently Typed Programming in Agda

[Thorsten Altenkirch]

>> record EmptyRec : Set where
>> constructor blub
>> field
>> bla : EmptyRec
>> 
>> elim-EmptyRec : ∀ {A : Set} → EmptyRec → A
>> elim-EmptyRec (blub y) = elim-EmptyRec y
> 
> And drop eta, of course, otherwise that's

Indeed eta and recursive records don't seem to get on very well.

> 
>> somehow one would think that
>> 
>> elim-EmptyRec y = elim-EmptyRec (EmptyRec.bla y)
> 
> in disguise.
> 
>> 
>> should work, but I think this can destroy normalisation.
> 
> Combining eta-expansion with strict constructor matching breaks
> subject reduction.

Indeed. But even without eta we loose normalisation, which is annoying because we can't prove
that EmptyRec is empty even though it clearly is.

One way to fix this would be to allow recursive records only when guarded by ∞. But this may hard to check.
Also it may be too restrictive.

For the time being, maybe we should have a pragma "recursive-records" which also disables eta for records.

Cheers,
Thorsten



> 
> Plus ça change
> 
> Conor
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda