<div dir="ltr">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</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 16 May 2018 at 15:33, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2018-05-16 18:28, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
So, I have an equality that is proved under abstraction, that fails<br>
when the abstraction is removed. Isn't that also a failure of subject<br>
reduction, or stability under substitution, or some other important<br>
property that we care about?<br>
</blockquote>
<br></span>
Do you really have code of the form<br>
<br>
  abstract<br>
<br>
    <code><br>
<br>
that fails (ignoring resources) if abstract is removed?<br>
<br>
I would not be surprised to see code of the following form fail when<br>
abstract is removed:<br>
<br>
  abstract<br>
<br>
    <code><br>
<br>
  <code><br>
<br>
However, this seems less problematic to me. Type-checking involves<br>
computation, and when you remove abstract you change the computational<br>
behaviour of the code.<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br></div>