<br><br><div class="gmail_quote">On Sun, Jun 14, 2009 at 8:18 PM, Eugene Kirpichov <span dir="ltr">&lt;<a href="mailto:ekirpichov@gmail.com">ekirpichov@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
The idea looks cool, but perfect strictness analysis is not possible,<br>
t.i. the problem of determining whether f _|_ = _|_ is undecidable,<br>
since it is a non-trivial property of f (there exist f&#39;s for which it<br>
is true, and ones for which it is false) and non-trivial properties<br>
are undecidable, thanks to Rice theorem.</blockquote><div><br>Unless you remove _|_ from the language.  If you have a &quot;total&quot; functional programming language[1] it becomes a trivial property, right?  I guess this would also extend to some dependently typed languages too.<br>
<br>[1] <a href="http://lambda-the-ultimate.org/node/2003">http://lambda-the-ultimate.org/node/2003</a><br><br>Jason<br></div></div><br>