17

This paper establishes that type inference (called "typability" in the paper) in System F is undecidable. What I've never heard mentioned elsewhere is the second result of the paper, namely that "type checking" in F is also undecidable. Here the "type checking" question means: given a term t, type T and typing environment A, is the judgment A ⊢ t : T derivable? That this question is undecidable (and that it's equivalent to the question of typability) is surprising to me, because it seems intuitively like it should be an easier question to answer.

But in any case, given that Haskell is based on System F (or F-omega, even), the result about type checking would seem to suggest that there is a Haskell term t and type T such that the compiler would be unable to decide whether t :: T is valid. If that's the case, I'm curious what such a term and type are... if it's not the case, what am I misunderstanding?

Presumably comprehending the paper would lead to a constructive answer, but I'm a little out of my depth :)

3
  • 5
    Haskell uses a resitricted edition of System F called [Hindley Milner][en.wikipedia.org/wiki/Hindley–Milner]. AFAIK it is possible to deduce the type of any expression that has a type. Making type-checks impossible is a matter of turning on enough strange extensions.
    – fuz
    Oct 4, 2011 at 9:26
  • 2
    @FUZxxl: I believe that by enabling only RankNTypes and ImpredicativeTypes one would have the full power of System F (and then some, since Haskell also supports abstraction over type operators). Oct 4, 2011 at 15:38
  • 1
    That's what I tried to say by "Making type-checks impossible is a matter of turning on enough strange extensions."
    – fuz
    Oct 4, 2011 at 15:41

2 Answers 2

12

Type checking can be made decidable by enriching the syntax appropriately. For example, in the paper, we have lambdas written as \x -> e; to type-check this, you must guess the type of x. However, with a suitably enriched syntax, this can be written as \x :: t -> e instead, which takes the guess-work out of the process. Similarly, in the paper, they allow type-level lambdas to be implicit; that is, if e :: t, then also e :: forall a. t. To do typechecking, you have to guess when and how many forall's to add, and when to eliminate them. As before, you can make this more deterministic by adding syntax: we add two new expression forms /\a. e and e [t] and two new typing rule that says if e :: t, then /\a. e :: forall a. t, and if e :: forall a. t, then e [t'] :: t [t' / a] (where the brackets in t [t' / a] are substitution brackets). Then the syntax tells us when and how many foralls to add, and when to eliminate them as well.

So the question is: can we go from Haskell to sufficiently-annotated System F terms? And the answer is yes, thanks to a few critical restrictions placed by the Haskell type system. The most critical is that all types are rank one*. Without going into too much detail, "rank" is related to how many times you have to go to the left of an -> constructor to find a forall.

Int -> Bool -- rank 0?
forall a. (a -> a) -- rank 1
(forall a. a -> a) -> (forall a. a -> a) -- rank 2

In particular, this restricts polymorphism a bit. We can't type something like this with rank one types:

foo :: (forall a. a -> a) -> (String, Bool) -- a rank-2 type
foo polymorphicId = (polymorphicId "hey", polymorphicId True)

The next most critical restriction is that type variables can only be replaced by monomorphic types. (This includes other type variables, like a, but not polymorphic types like forall a. a.) This ensures in part that type substitution preserves rank-one-ness.

It turns out that if you make these two restrictions, then not only is type-inference decidable, but you also get minimal types.

If we turn from Haskell to GHC, then we can talk not only about what is typable, but how the inference algorithm looks. In particular, in GHC, there are extensions that relax the above two restrictions; how does GHC do inference in that setting? Well, the answer is that it simply doesn't even try. If you want to write terms using those features, then you must add the typing annotations we talked about all the way back in paragraph one: you must explicitly annotate where foralls get introduced and eliminated. So, can we write a term that GHC's type-checker rejects? Yes, it's easy: simply use un-annotated rank-two (or higher) types or impredicativity. For example, the following doesn't type-check, even though it has an explicit type annotation and is typable with rank-two types:

{-# LANGUAGE Rank2Types #-}
foo :: (String, Bool)
foo = (\f -> (f "hey", f True)) id

* Actually, restricting to rank two is enough to make it decidable, but the algorithm for rank one types can be more efficient. Rank three types already give the programmer enough rope to make the inference problem undecidable. I'm not sure whether these facts were known at the time that the committee chose to restrict Haskell to rank-one types.

5
  • 3
    Re. "So the question is:" ... no, that's actually not the question. I didn't ask whether by annotating function parameters or restricting to rank-2 polymorphism we can make type checking decidable; I know the answer to that is yes. My question is, can you exhibit a term t and type T such that t :: T confounds the type checker. I should've made clear that t should be a term in the untyped lambda calculus (it should contain no type ascriptions), and T can contain any number of embedded foralls. Oct 4, 2011 at 17:19
  • @pelotom Okay, sorry for the misunderstanding. The question you ask is a much harder one: it involves a very intricate knowledge of the exact type-checking algorithm used by the particular compiler you're interested in. It's not possible to go from a proof of undecidability of a problem to an unsolvable instance of that problem without inspecting the algorithm being used to approximate a solution to the problem. Oct 4, 2011 at 21:08
  • @pelotom I've added two sections, one on the other important restriction (predicativity), and one that is an attempt to answer your actual question for the specific case of GHC's type-checker: giving a term and type which GHC can't currently verify. Is that better? Oct 5, 2011 at 14:53
  • Rank 2 types do not have minimal types
    – JTanner
    Oct 7, 2020 at 20:59
  • @JTanner Correct. Type inference with rank-2 types is necessarily a whole-program operation. Do you believe that is contradicted by anything in the answer as written? If so, what, exactly? Oct 7, 2020 at 23:04
3

Here is an example for a type level implementation of the SKI calculus in Scala: http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

The last example shows an unbounded iteration. If you do the same in Haskell (and I'm pretty sure you can), you have an example for an "untypeable expression".

1
  • I'd like to see the equivalent in Haskell.
    – Dan Burton
    Oct 5, 2011 at 1:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.