[Agda] The joys and sorrows of abstraction

[Philip Wadler]

Thank you to Wolfram and Nils!

Wolfram's suggestion worked!

Nils's suggestions C-u C-c C-n is great for testing, but doesn't help if I
want to document the results of the test in the file. I'm writing a
textbook, so including examples in the file is important! It would also be
important if one wanted to include tests for documentation and reliability.

Nils's suggestion to disable reduction with () is neat, but possibly not
the best pedagogy for a textbook.

However, there is no way to
> turn off abstract while type-checking (because this could lead to
> problems with subject reduction).


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?

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 02:52, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 2018-05-16 00:27, Philip Wadler wrote:
>
>> Is there any way to *both* be able to compute fresh names *and* retain
>> my related proofs, in particular, the proof that `fresh x xs`
>> generates a name not in `xs`?
>>
>
> When normalising an expression you can make abstract definitions compute
> by using C-u C-c C-n instead of C-c C-n. However, there is no way to
> turn off abstract while type-checking (because this could lead to
> problems with subject reduction).
>
> There are other ways to control reduction. Wolfram suggested one.
> Another is to match on a value of the unit type, and not supply a
> concrete constructor until you want the code to compute.
>
> --
> /NAD
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/bf7c3417/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/bf7c3417/attachment.ksh>