It doesn’t type

The goal of this lecture note it to point out why some expressions do not have a type. Obviously, if a function expects an integer and it is applied to a Boolean, that is a type error: this application does not have a type, and neither does the expression that contains this application. Less obviously, an expression where a name is applied to itself does not have a type.

Interlude

Anton: An expression where a name is applied to itself does not have a type?

Alfrothul: Apparently not:

# fun x -> x x;;
Characters 11-12:
  fun x -> x x;;
             ^
Error: This expression has type 'a -> 'b
       but an expression was expected of type 'a
       The type variable 'a occurs inside 'a -> 'b
#

Anton: Do you understand this error message?

Alfrothul: Er... No.

Anton: Let’s build a proof tree then, picking t0 as the name of the putative type:

----------------------
. |- fun x -> x x : t0

Alfrothul: We have no other choice but applying the FUN rule, which means that t0 must denote a function type, let’s say t1 -> t2, picking t1 as the name of the domain and t2 as the name of the co-domain.

Pablito: Let me make a note of that: t0 = t1 -> t2. Again.

Alfrothul: Thanks. Now for applying the FUN rule:

    (x : t1), . |- x x : t2
FUN -----------------------
    . |- fun x -> x x : t0

Anton: We have no other choice but applying the APP rule, which means that the type of x must be that of a function with t2 as codomain, let’s say t3 -> t2.

Pablito: Let me make a note of that: t1 = t3 -> t2.

Anton: Thanks. Now for applying the APP rule:

    (x : t1), . |- x : t3 -> t2    (x : t1), . |- x : t3
APP ----------------------------------------------------
    (x : t1), . |- x x : t2
FUN -----------------------
    . |- fun x -> x x : t0

Alfrothul: For the left subgoal, we have no other choice but applying the LOOKUP_FOUND rule, which means that t1 and t3 -> t2 must be the same.

Pablito: Let me make a note of that: t1 = t3 -> t2, wait, I already did it.

Alfrothul: Thanks. Now for applying the LOOKUP_FOUND rule:

LOOKUP_FOUND ---------------------------
             (x : t1), . |- x : t3 -> t2    (x : t1), . |- x : t3
         APP ----------------------------------------------------
             (x : t1), . |- x x : t2
         FUN -----------------------
             . |- fun x -> x x : t0

Anton: For the right subgoal, we also have no other choice but applying the LOOKUP_FOUND rule, which means that t1 and t3 must be the same.

Pablito: Let me make a note of that: t1 = t3.

Anton: Thanks. Now for applying the LOOKUP_FOUND rule:

LOOKUP_FOUND ---------------------------    LOOKUP_FOUND ---------------------
             (x : t1), . |- x : t3 -> t2                 (x : t1), . |- x : t3
         APP -----------------------------------------------------------------
             (x : t1), . |- x x : t2
         FUN -----------------------
             . |- fun x -> x x : t0

Alfrothul: Our tree is now complete.

Pablito: So let’s look at the constraints we gathered on the way:

t0 = t1 -> t2

t1 = t3 -> t2

t1 = t3

Anton: The two last constraints imply the constraint t1 = t1 -> t2.

Alfrothul: Aha, this constraint has no more a solution than the equation x = x + 1 has one in algebra.

Anton: So fun x -> x x does not have a type.

Alfrothul: And in hindsight, the reason why is actually the one reported in the error message:

# fun x -> x x;;
Characters 11-12:
  fun x -> x x;;
             ^
Error: This expression has type 'a -> 'b
       but an expression was expected of type 'a
       The type variable 'a occurs inside 'a -> 'b
#

Dana: Cognitive bootstrapping, here we come.

Version

Created [10 Jan 2023]