[Agda] The joys and sorrows of abstraction

[Philip Wadler]

Thanks, Martin. So which fragment do you recommend? 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 16:03, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:

>
>
> On 16/05/18 20:37, Philip Wadler wrote:
>
>> 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
>>
>
> It is because of things such as this that I prefer to restrict my usage of
> Agda to a fragment corresponding to a well-understood type theory.
>
> This may be limiting in terms of expressivity, conciseness, and
> efficiency, but at least one can tell whether something is a bug or not,
> rather than a bug or a feature.
>
> :-)
> Martin
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/2c1138aa/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/2c1138aa/attachment.ksh>