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

M static/typing-is-hard.html

@@ 65,6 65,8 @@
 <p>The Hindley-Milner (HM) type system is a type system for the simple typed lambda calculus with parametric polymorphism, which is used as a base for many functional languages. Type-checking for HM is decidable and efficient, its complexity is linear in the size of the program. Type inference is more difficult than type checking, since the compiler has to solve the type constraints incurred for expressions in the program. It is <strong>decidable</strong> for the HM type system, however the problem itself is PSPACE-hard and EXPTIME-complete, meaning that in the worst case it needs at least a polynomial amount of extra space and exponential time relative to the input size. Fortunately, the type inference algorithm is linear when the nesting depth of polymorphic variables is bounded, as is the case for most applications. There exist many type inference algorithms, the best known one is the so-called <em>Algorithm W</em>. Many functional programming languages implement variants of the HM type system.</p>
 <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>
 <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>