~bfiedler/website

8ef5346f7fd2b7285d07530930781dc282b004b1 — Ben Fiedler 24 days ago d452cc7
Add explanation why decidability of Idris type checking is surprising
1 files changed, 1 insertions(+), 1 deletions(-)

M static/typing-is-hard.html
M static/typing-is-hard.html => static/typing-is-hard.html +1 -1
@@ 82,7 82,7 @@
<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>
<p><strong>decidable</strong>, surprisingly. Idris has dependent types, which in general have undecidable type-checking, 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>
<p><strong>undecidable</strong>, because <a href="https://arxiv.org/pdf/1605.05274.pdf">Java Generics are Turing complete</a>. Java 5 or later is <strong>unsound</strong>, as shown by <a href="https://dl.acm.org/doi/pdf/10.1145/2983990.2984004">Amin and Tate (2015)</a></p>
<h3 id="ocaml">OCaml</h3>