From 238747f86bfca3693601939eae0bffa808bc65b5 Mon Sep 17 00:00:00 2001 From: Ben Fiedler Date: Thu, 8 Jul 2021 17:13:35 +0200 Subject: [PATCH] Update toc as well --- static/typing-is-hard.html | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/static/typing-is-hard.html b/static/typing-is-hard.html index c3e61c2..7a776d9 100644 --- a/static/typing-is-hard.html +++ b/static/typing-is-hard.html @@ -27,6 +27,7 @@
• Decidability
• Hindley-Milner Type System
• Dependent types
• +
• System F
• How Hard is Type-Checking Your Favorite Language?
• C++
• @@ -65,7 +66,7 @@

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 decidable 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 Algorithm W. Many functional programming languages implement variants of the HM type system.

### Dependent types

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 can be shown by reduction to the Post Correspondence Problem.

-

+

### System F

System F is an extension of the simply typed lambda calculus which allows quantification over types via type variables. An example is the identity function (in pseudo-Haskell): `id :: a -> a`, which is shorthand for `id :: forall a. a -> a`. In this example `forall` binds the type variable `a`, and hence `id` is quantified over all types. Type inference in System F is always undecidable, while the question whether type-checking is decidable depends on lower-level details.

## How Hard is Type-Checking Your Favorite Language?

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 file an issue 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.

-- 2.32.0