[Agda] The joys and sorrows of abstraction

[Philip Wadler]

Thanks for following up. It is the latter case. But I don't understand why
it should be ok for that to fail. Removing abstract should just replace
some abstract terms by their concretions, which have already been type
checked. Everything that was provably equal before should still be equal,
so why is it ok for the proof of equality to now fail? Doesn't this violate
stability under substitution? Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 16 May 2018 at 15:33, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 2018-05-16 18:28, Philip Wadler wrote:
>
>> So, I have an equality that is proved under abstraction, that fails
>> when the abstraction is removed. Isn't that also a failure of subject
>> reduction, or stability under substitution, or some other important
>> property that we care about?
>>
>
> Do you really have code of the form
>
>   abstract
>
>     <code>
>
> that fails (ignoring resources) if abstract is removed?
>
> I would not be surprised to see code of the following form fail when
> abstract is removed:
>
>   abstract
>
>     <code>
>
>   <code>
>
> However, this seems less problematic to me. Type-checking involves
> computation, and when you remove abstract you change the computational
> behaviour of the code.
>
> --
> /NAD
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/86043591/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/86043591/attachment.ksh>