Exercises for Week 04

Exercise 00

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.

3. Briefly explain, in your own words, the concept of commuting diagram, as presented in the postlude of Chapter Towards OCaml.

   For one more example (which could be connected to Exercise 08.i):

   

4. For your general culture, check out the author’s tribute to Peter Landin.

Mandatory exercises

• Exercise 00: perusing the index and checking the updates
• Exercise 03: implementing and testing exclusive disjunction
• Exercise 06: implementing and testing exclusive disjunction
• Exercise 07: exhibiting expressions of a given polymorphic type
• Exercise 08: exhibiting more expressions of a given polymorphic type
• Exercise 09: lexical scope at work
• Exercise 13: an all-too-common error
• Exercise 14 implementing and testing polynomials of degree 4
• Exercise 15: tinkering with the generator of random proofs
• Exercise 17: associating left and right

Recommended exercises

• Exercise 10: exhibiting even more expressions of a given polymorphic type
• Exercise 12: a gorgeous unit-test function for string concatenation

Exercise for the over-achievers (this means you)

• Exercise 20: exhibiting a family of expressions of a family of given types; did we see these types before?

Exercise 17

A question about the design of OCaml:

• in its language of expressions, applications implicitly associate to the left, i.e., String.get "hello world" 0 is parsed as (String.get "hello world") 0;
• in its language of types, function types implicitly associate to the right, i.e., string -> int -> char is parsed as string -> (int -> char).

Justify this choice.

Hint: contemplate the APP typing rule.

Richard Feynman: I believe that has some significance for [y]our problem.

Mimer: Professor Feynman! Thanks for stopping by!

Halcyon (whispering to Vigfus): Is he joking? Mr. Feynman I mean.

Vigfus (whispering back): I am not sure.

Mimer: Huh, by the by, would you mind autographing my copy of your book?

Exercise 18

Consider the following definition:

let length_of_string_self_concatenation s =
  String.length (s ^ s) = 2 * String.length s;;

What is the result of applying length_of_string_concatenation to any string?

• true, always?
• false, always?
• sometimes true, sometimes false?

Justify your answer.

Solution for Exercise 18

The answer is true, always, because concatenating a string to itself yields a string which is twice as long.

The computation carried out by length_of_string_self_concatenation can be depicted with the following commuting diagram:

Exercise 19

Consider the following definition:

let length_of_string_concatenation s1 s2 =
  String.length (s1 ^ s2) = String.length s1 + String.length s2;;

What is the result of applying length_of_string_concatenation to any two strings?

• true, always?
• false, always?
• sometimes true, sometimes false?

Justify your answer.

Exercise 20

1. Exhibit an expression of type ('a * 'b * 'c * 'd * 'e -> 'f) -> unit -> 'a * 'b * 'c * 'd * 'e -> 'f. Justify your answer.
2. Exhibit an expression of type ('a * 'b * 'c * 'd * 'e -> 'f) -> 'a -> 'b * 'c * 'd * 'e -> 'f. Justify your answer.
3. Exhibit an expression of type ('a * 'b * 'c * 'd * 'e -> 'f) -> 'a * 'b -> 'c * 'd * 'e -> 'f. Justify your answer.
4. Exhibit an expression of type ('a * 'b * 'c * 'd * 'e -> 'f) -> 'a * 'b * 'c -> 'd * 'e -> 'f. Justify your answer.
5. Exhibit an expression of type ('a * 'b * 'c * 'd * 'e -> 'f) -> 'a * 'b * 'c * 'd -> 'e -> 'f. Justify your answer.
6. Exhibit an expression of type ('a * 'b * 'c * 'd * 'e -> 'f) -> 'a * 'b * 'c * 'd * 'e -> unit -> 'f. Justify your answer.

Déjà vu, anyone?

Strange.

—Grace Jones

Exercise 21

Let us revisit the FUN, APP, and LET typing rules:

FUN	G, (x1 : t1) |- e2 : t2
	G |- fun x1 -> e2 : t1 -> t2

APP	G |- e0 : t1 -> t2	G |- e1 : t1
	G |- e0 e1 : t2

LET	G |- e1 : t1	(x1 : t1), G |- e2 : t2
	G |- let x1 = e1 in e2 : t2

For the sake of this exercise, let us assume that for any name x1 and for any expression e1 and e2, a let-expression such as let x1 = e1 in e2 is syntactic sugar for (fun x1 -> e2) e1, a principle of correspondence due to Peter Landin. Is this syntactic sugar compatible with the typing rules just above? In other words, can the LET typing rule be derived out of the FUN and APP typing rules?

Version

Completed [06 Feb 2022]

Created [04 Feb 2022]