Date: Thu, 8 Jul 2021 17:09:02 +0200
Subject: [PATCH] Add some more information about System F
---
static/typing-is-hard.html | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/static/typing-is-hard.html b/static/typing-is-hard.html
index 04e40dc..fcebeb8 100644
--- a/static/typing-is-hard.html
+++ b/static/typing-is-hard.html
@@ -66,7 +66,7 @@
### 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.

+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.

### C++

--
2.32.0