On Mon, Mar 9, 2009 at 10:37 AM, Eugene Kirpichov <span dir="ltr">&lt;<a href="mailto:ekirpichov@gmail.com">ekirpichov@gmail.com</a>&gt;</span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I mean, there is no way to write a firstCoord function so that it<br>
would work, for example, on &#39;\y -&gt; P 42 y&#39; and yield 42.<br>
<br>
Except for this one:<br>
<br>
firstCoord proj = case (proj undefined) of P x y -&gt; x<br>
<br>
However, this requires proj to be non-strict in its remaining argument.<br>
But this will actually work if you pass &quot;P x&quot; to it for some x,<br>
because it *is* non-strict in the remaining argument.</blockquote><div><br>That&#39;s brilliant.  Any function which behaves like &quot;P x&quot; but is strict in the second argument is in fact a different function.  So this trick is a semidecidable pattern for this function.<br>
<br>Bring in the unamb, so we can do interesting things with semidecidable predicates :-)   (I still don&#39;t like the proof obligation of unamb, and would like to see it picked up to a higher level of abstraction where the usage is always correct)<br>
<br>Luke<br><br></div></div><br>