[Agda] The joys and sorrows of abstraction

Martin Escardo m.escardo at cs.bham.ac.uk
Wed May 16 21:03:46 CEST 2018



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


More information about the Agda mailing list