In reference to the section about Using a grammar to generate grammatically correct sentences, check out Strachey’s generator of love letters and the generator of mathematical proofs. (Make sure to reload these web pages a few times.)
Assuming the inference rule
| NOT | G |- e : bool | |
| G |- not e : bool |
and in a type environment where x has type int and y has type char, does the expression fun x -> not x have type bool -> bool or is it ill-typed?
Harald: Well, this exercise looks unproblematic.
Alfrothul (pragmatic): Let’s start at the root of the tree:
(x : int), (y : char), . |- fun x -> not x : bool -> bool
Harald: This looks right – the type environment features the type of x and of y, the expression is fun x -> not x, and the type is bool -> bool.
Brynja: Right, but wait. The following root is just as plausible:
(y : char), (x : int), . |- fun x -> not x : bool -> bool
Alfrothul: True, but it doesn’t matter since x and y are distinct.
Harald: Right. If the type environment is, e.g., (z : char), (z : string), . then the expression z has type char, whereas it has type string in the type environment (z : string), (z : char), .. To wit, here is the first proof tree, applying LOOKUP_FOUND, where x is instantiated with z, t is instantiated with char, G is instantiated with (z : string), ., x is instantiated with z, and t is instantiated with char:
LOOKUP_FOUND ---------------------------------------
(z : char), (z : string), . |- z : char
Alfrothul: And here is the second proof tree, also applying LOOKUP_FOUND, where x is instantiated with z, t is instantiated with string, G is instantiated with (z : char), ., x is instantiated with z, and t is instantiated with string:
LOOKUP_FOUND -----------------------------------------
(z : string), (z : char), . |- z : string
Brynja: OK, so it doesn’t matter which root we start with. Let’s take yours, Alfrothul.
Alfrothul: Thank you. There is only one typing rule we can apply, namely FUN, where G is instantiated with (x : int), (y : char), ., x is instantiated with x, e is instantiated with not x, t1 is instantiated with bool, and t2 is instantiated with bool:
(x : bool), (x : int), (y : char), . |- not x : bool
FUN ---------------------------------------------------------
(x : int), (y : char), . |- fun x -> not x : bool -> bool
Harald: And now there is only one typing rule we can apply, namely NOT, where G is instantiated with (x : bool), (x : int), (y : char), . and e is instantiated with x:
(x : bool), (x : int), (y : char), . |- x : bool
NOT ----------------------------------------------------
(x : bool), (x : int), (y : char), . |- not x : bool
FUN -------------------------------------------------------------------
(x : int), (y : char), . |- fun x -> not x : bool -> bool
Alfrothul: There is still only one typing rule we can apply, namely LOOKUP_FOUND, where G is instantiated with (x : int), (y : char), ., x is instantiated with x, and t is instantiated with bool:
LOOKUP_FOUND ------------------------------------------------
(x : bool), (x : int), (y : char), . |- x : bool
NOT ----------------------------------------------------
(x : bool), (x : int), (y : char), . |- not x : bool
FUN -------------------------------------------------------------------
(x : int), (y : char), . |- fun x -> not x : bool -> bool
Harald: And we are done. The proof tree is complete, which proves that in the type environment (x : int), (y : char), ., the expression fun x -> not x is well typed and has type bool -> bool.
Alfrothul: If we had started with Brynja’s root, we would have done through the same steps and would have reached the same conclusion, i.e., in the type environment (y : char), (x : int), ., the expression fun x -> not x is well typed and has type bool -> bool.
Brynja: What is the point of this exercise?
Mimer: The point is to crystallize that the type environment is extended on its left, not on its right, which is something that beginners tend to do somehow.
Brynja: Eeek. If the environment was extended on the right, the expression would be deemed to be ill-typed.
Harald: Beg pardon?
Brynja: The point is that we would come up with:
(x : int), (y : char), (x : bool), . |- not x : bool
Harald: I see, but the environment is incorrectly extended.
Brynja: And that is the point of this exercise. We could then only apply the NOT rule, where G is instantiated with (x : int), (y : char), (x : bool), . and e is instantiated with bool:
(x : int), (y : char), (x : bool), . |- x : bool
NOT ----------------------------------------------------
(x : int), (y : char), (x : bool), . |- not x : bool
Alfrothul: Right. And then we could only apply the LOOKUP_FOUND rule, except that we could not since x has type int in the type environment, and therefore it cannot have type bool.
Brynja: Still about Exercise 18, what if we didn’t have the NOT rule, but not was declared in the type environment?
Harald: The question would then be, in a type environment where x has type int and not has type bool -> bool, does the expression fun x -> not x have type bool -> bool or is it ill-typed. That looks unproblematic too.
Alfrothul (pragmatic): Let’s start at the root of the tree:
(x : int), (not : bool -> bool), . |- fun x -> not x : bool -> bool
Harald: This looks right – the type environment features the type of x and of not, the expression is fun x -> not x, and the type is bool -> bool.
Brynja: Right, and since not and x are distinct, the order in the type environment does not matter.
Alfrothul: There is only one typing rule we can apply, namely FUN, where G is instantiated with (x : int), (not : bool -> bool), ., x is instantiated with x, e is instantiated with not x, t1 is instantiated with bool and t2 is instantiated with bool:
(x : bool), (x : int), (not : bool -> bool), . |- not x : bool
FUN -------------------------------------------------------------------
(x : int), (not : bool -> bool), . |- fun x -> not x : bool -> bool
Harald: And now there is only one typing rule we can apply, namely APP, where G is instantiated with (x : bool), (x : int), (not : bool -> bool), ., e0 is instantiated with not, e1 is instantiated with x, t1 is unspecified yet, so let’s call it uy, and t2 is instantiated with bool:
(x : bool), (x : int), (not : bool -> bool), . |- not : uy -> bool (x : bool), (x : int), (not : bool -> bool), . |- x : uy
APP ------------------------------------------------------------------------------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not x : bool
FUN -------------------------------------------------------------------
(x : int), (not : bool -> bool), . |- fun x -> not x : bool -> bool
Alfrothul: Unspecified, unspecified – uy can only be bool.
Harald (calmly): You are probably right, but let’s not try to dance faster than the music. Let’s continue to play the game and consider the left branch.
Alfrothul (interrupting): How about we consider the right branch first? Because the LOOKUP_FOUND applies straight away, where x is instantiated with x, t is instantiated with bool, G is instantiated with (x : int), (not : bool -> bool), ., x is instantiated with x, and t is instantiated with uy.
Harald: True that:
LOOKUP_FOUND --------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not : uy -> bool (x : bool), (x : int), (not : bool -> bool), . |- x : uy
APP -------------------------------------------------------------------------------------------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not x : bool
FUN -------------------------------------------------------------------
(x : int), (not : bool -> bool), . |- fun x -> not x : bool -> bool
Alfrothul: And since in the application of LOOKUP_FOUND, t is instantiated both with bool and with uy, uy is constrained to be bool.
Harald: So I guess we can either update the tree, or remember that uy stands for bool.
Brynja (prudent): Rather the latter – let’s not mess up with the tree.
Harald: Be that as it may, we can consider the left branch. We can only apply LOOKUP_NOT_FOUND_YET, where x' is instantiated with x, t' is instantiated with bool, G is instantiated with (x : int), (not : bool -> bool), ., x is instantiated with not, and t is instantiated with uy -> bool:
(x : int), (not : bool -> bool), . |- not : uy -> bool
LOOKUP_NOT_FOUND_YET ------------------------------------------------------------------ LOOKUP_FOUND --------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not : uy -> bool (x : bool), (x : int), (not : bool -> bool), . |- x : uy
APP -------------------------------------------------------------------------------------------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not x : bool
FUN -------------------------------------------------------------------
(x : int), (not : bool -> bool), . |- fun x -> not x : bool -> bool
Harald (continuing): You’re sure you don’t want to change uy to bool?
Brynja: Quite sure – we are bound to miss an occurrence or to overwrite one of the occurrences of another variable, and then what.
Alfrothul (unabated): Well, we can still only apply LOOKUP_NOT_FOUND_YET, where x' is instantiated with x, t' is instantiated with int, G is instantiated with (not : bool -> bool), ., x is instantiated with not, and t is instantiated with uy -> bool:
(not : bool -> bool), . |- not : uy -> bool
LOOKUP_NOT_FOUND_YET ------------------------------------------------------
(x : int), (not : bool -> bool), . |- not : uy -> bool
LOOKUP_NOT_FOUND_YET ------------------------------------------------------------------ LOOKUP_FOUND --------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not : uy -> bool (x : bool), (x : int), (not : bool -> bool), . |- x : uy
APP -------------------------------------------------------------------------------------------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not x : bool
FUN -------------------------------------------------------------------
(x : int), (not : bool -> bool), . |- fun x -> not x : bool -> bool
Harald: Aha, and now we can apply LOOKUP_FOUND, where x is instantiated with not, t is instantiated with bool -> bool, G is instantiated with ., x is instantiated with not, and t is instantiated with uy -> bool, which is OK since uy stands for bool:
LOOKUP_FOUND -------------------------------------------
(not : bool -> bool), . |- not : uy -> bool
LOOKUP_NOT_FOUND_YET ------------------------------------------------------
(x : int), (not : bool -> bool), . |- not : uy -> bool
LOOKUP_NOT_FOUND_YET ------------------------------------------------------------------ LOOKUP_FOUND --------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not : uy -> bool (x : bool), (x : int), (not : bool -> bool), . |- x : uy
APP -------------------------------------------------------------------------------------------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not x : bool
FUN -------------------------------------------------------------------
(x : int), (not : bool -> bool), . |- fun x -> not x : bool -> bool
Alfrothul: And we are pretty much done, since the proof tree is complete. For clarity, let us draw it again by replacing uy with bool:
LOOKUP_FOUND -------------------------------------------
(not : bool -> bool), . |- not : bool -> bool
LOOKUP_NOT_FOUND_YET --------------------------------------------------------
(x : int), (not : bool -> bool), . |- not : bool -> bool
LOOKUP_NOT_FOUND_YET -------------------------------------------------------------------- LOOKUP_FOUND ----------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not : bool -> bool (x : bool), (x : int), (not : bool -> bool), . |- x : bool
APP -----------------------------------------------------------------------------------------------------------------------------------------------
(x : bool), (x : int), (not : bool -> bool), . |- not x : bool
FUN -------------------------------------------------------------------
(x : int), (not : bool -> bool), . |- fun x -> not x : bool -> bool
Harald: The existence of this tree proves that in the type environment (x : int), (not : bool -> bool), ., the expression fun x -> not x is well typed and has type bool -> bool.
Fixed a typo [07 Feb 2020]
Added Exercise 18 and its solution as well as the subsequent interlude [01 Feb 2020]
Added Exercise 0 [31 Jan 2020]
Created [03 Feb 2019]