1 files changed, 1 insertions(+), 1 deletions(-)

M static/typing-is-hard.html

@@ 66,7 66,7 @@
 <h3 id="dependent-types">Dependent types</h3>
 <p>In simple terms dependent types allow types to depend not only on other types, but on values. This is best understood by an example: Normally we can only encode very coarse information, such as “x is of integer type”. Dependent types allow us to define more detailed types. For example we could then create a type “even integer”, whose only inhabitants are even integers. This is strictly more powerful than the previous setting: Dependent types in general make type inference undecidable as <a href="https://link.springer.com/content/pdf/10.1007%2FBFb0037103.pdf">can be shown</a> by reduction to the <a href="https://en.wikipedia.org/wiki/Post_correspondence_problem">Post Correspondence Problem</a>.</p>
 <h3 id="System F">System F</h3>
-<p><a href="https://en.wikipedia.org/wiki/System_F">System F</a> is an extension of the <a href="https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus">simply typed lambda calculus</a> which allows quantification over types via type variables. An example is the identity function (in pseudo-Haskell): <code>id :: a -&lt; a</code>, which is shorthand for <code>id :: forall a. a -&lt; a</code>. In this example <code>forall</code> binds the type variable <code>a</code>, and hence <code>id</code> is quantified over all types.</p>
+<p><a href="https://en.wikipedia.org/wiki/System_F">System F</a> is an extension of the <a href="https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus">simply typed lambda calculus</a> which allows quantification over types via type variables. An example is the identity function (in pseudo-Haskell): <code>id :: a -&lt; a</code>, which is shorthand for <code>id :: forall a. a -&lt; a</code>. In this example <code>forall</code> binds the type variable <code>a</code>, and hence <code>id</code> is quantified over all types. <a href="https://www.sciencedirect.com/science/article/pii/S0890540112001150">Type inference in System F is always undecidable</a>, while the question whether type-checking is decidable depends on lower-level details.</p>
 <h2 id="how-hard-is-type-checking-your-favorite-language">How Hard is Type-Checking Your Favorite Language?</h2>
 <p>Below I’ve compiled a list of languages and how hard type checking/type inference is in these languages. If you find a mistake or are missing a language please <a href="https://todo.sr.ht/~bfiedler/typing-is-hard">file an issue</a> with your language, its type checking complexity and optimally a resource that supports your claim. I do not claim completeness nor correctness of the properties shown here, it is mainly an amalgamation of blog posts I’ve been collecting.</p>
 <h3 id="c">C++</h3>