Navigation

Exercises for Week 03

Exercise 0

  1. At the top right and at the bottom right of the present page, there is a clickable word, “index”, to access the index of the current version of the lecture notes. Click on it and then peruse the index, making 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 for Intro to CS, updates). Make sure to check them out regularly, as they reflect the development of the lecture.

Mandatory exercises

  • Exercise 0: perusing the index and checking the updates
  • Exercise 7: finding the type of a given expression
  • Exercise 9: finding an expression of a given type
  • Exercise 10: a unit test for the successor function
  • Exercise 11: a unit test for the negation function
  • Exercise 13: a unit test for the twice-less-than comparison function
  • Exercise 15: a unit test for the function summing the first consecutive odd natural numbers

Exercise 18

Assuming the inference rule

NOTG |- 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 18

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.

Interlude

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.

Version

Created [30 Jan 2021]

Table Of Contents

Previous topic

Using emacs to interact with the OCaml processor

Next topic

Lecture Notes, Week 04

Navigation

© Copyright 2021, Olivier Danvy. Created using Sphinx 1.2.2.