Exercises for Week 03

Exercise 00

1. The index of concepts for this week is in a separate chapter. Peruse it and make sure that its entries make sense to you (otherwise, click on them to check them out).
2. The lecture notes start with updates (Chapter Lecture Notes, updates). Make sure to check them out regularly, as they reflect the development of the lecture.
3. What is the difference between syntax and semantics?
4. What is a type error?
5. What is the difference between a dynamically typed programming language and a statically typed programming language?

Resources

• A template .ml file for the exercises of this week (latest version: 19 Mar 2023).

Mandatory exercises

• Exercise 00: perusing the index, checking the updates, and reflecting about concepts
• Exercise 01: revisiting the commuting diagram for batch computations
• Exercise 04: playing with tuples
• Exercise 06: tupling the unit value
• Exercise 11: finding the type of a given expression
• Exercise 12: finding an expression of a given type
• Exercise 14: a unit test for the successor function
• Exercise 15: a unit test for the negation function
• Exercise 17: a unit test for the twice-less-than comparison function
• Exercise 19: a unit test for the function summing the first consecutive odd natural numbers

Recommended exercises

• Exercise 13: drawing a proof tree
• Exercise 18: a unit test for the function summing the first consecutive natural numbers

Exercise 22

Assuming the typing 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?

Solution for Exercise 22

Anton: 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

Anton: 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.

Dana: 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.

Anton: 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

Dana: 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

Anton: 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

Anton: 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 Dana’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.

Dana: 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.

Dana: Eeek. If the environment was extended on the right, the expression would be deemed to be ill-typed.

Anton: Beg pardon?

Dana: The point is that we would come up with:

(x : int), (y : char), (x : bool), . |- not x : bool

Anton: I see, but the environment is incorrectly extended.

Dana: 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.

Interlude

Dana: Still about Exercise 22, what if we didn’t have the NOT rule, but not was declared in the type environment?

Anton: 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

Anton: 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.

Dana: 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

Anton: 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.

Anton (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.

Anton: 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.

Anton: So I guess we can either update the tree, or remember that uy stands for bool.

Dana (prudent): Rather the latter – let’s not mess up with the tree.

Anton: 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

Anton (continuing): You’re sure you don’t want to change uy to bool?

Dana: 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

Anton: 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

Anton: 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.

Resources

• A template .ml file for the exercises of this week (latest version: 19 Mar 2023).

Version

Updated the template .ml file with more structure for the answers [19 Mar 2023]

Updated the template .ml file with correct exercise numbers [02 Feb 2023]

Created [26 Aug 2022]