~bfiedler/website

d452cc7a06d89c1a5cf5ca45e2cec575dbeb864e — Ben Fiedler 2 months ago 459f4ab
Haskell, extensions: Remove mentions of System F

Type checking may be deciable depending on implementation of System F,
while type inference is always undecidable.
1 files changed, 2 insertions(+), 2 deletions(-)

M static/typing-is-hard.html
M static/typing-is-hard.html => static/typing-is-hard.html +2 -2
@@ 79,8 79,8 @@
<p><strong>decidable</strong>, since type inference is only used for variable initialization</p>
<h3 id="haskell">Haskell</h3>
<p>1998 standard, no extensions: <strong>decidable</strong>, variant of HM</p>
<p>2010 standard, no extensions: <strong>decidable</strong>, restriction of System F</p>
<p>with sufficient<a href="#fn1" class="footnote-ref" id="fnref1"><sup>1</sup></a> extensions: <strong>undecidable</strong>, as type checking in System F is undecidable. There exist <a href="https://www.lochan.org/keith/publications/undec.html">Turing Machines in Haskell types</a>. A simpler variant is to implement the <a href="https://mail.haskell.org/pipermail/haskell/2006-August/018355.html">SKI calculus</a>.</p>
<p>2010 standard, no extensions: <strong>decidable</strong>, restriction of <a href="https://wikipedia.org/wiki/System_F">System F</a></p>
<p>with sufficient<a href="#fn1" class="footnote-ref" id="fnref1"><sup>1</sup></a> extensions: <strong>undecidable</strong>, as there exist <a href="https://www.lochan.org/keith/publications/undec.html">Turing Machines in Haskell types</a>. A simpler variant is to implement the <a href="https://mail.haskell.org/pipermail/haskell/2006-August/018355.html">SKI calculus</a>.</p>
<h3 id="idris">Idris</h3>
<p><strong>decidable</strong>, surprisingly. Idris has dependent types, but <a href="https://docs.idris-lang.org/en/latest/faq/faq.html#evaluation-at-the-repl-doesn-t-behave-as-i-expect-what-s-going-on">at compile time it will only evaluate expressions which it knows to be total (terminating and covering all inputs)</a>.</p>
<h3 id="java">Java</h3>