From dc00f24b097a9125680584cae98821a858d95d58 Mon Sep 17 00:00:00 2001 From: Ben Fiedler Date: Thu, 8 Jul 2021 17:12:57 +0200 Subject: [PATCH] fix orientation of angle brackets --- 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 fcebeb8..c3e61c2 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. Type inference in System F is always undecidable, while the question whether type-checking is decidable depends on lower-level details.

+

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