Please write your solutions as clearly and concisely as possible.

1. (10 pts) Consider the grammar for types

      Type ::= TVar | Type -> Type
   

   Say whether it is true that, for an arbitrary type T

   if T is inhabited, then there exists exactly one lambda term M in normal form with type T.

2. (25 pts) For each of the following terms in the grammar defined in Lecture 12 (see corresponding lecture notes) say whether it is typeable or not, and, in the positive case, give its principal type. Justify your answer by constructing the proof, if the term is typeable, or by showing that a proof cannot be constructed. You don't need to illustrate in detail all the steps of the unification algorithm, but please point out clearly the system of equations to be solved, and its most general unifier, or show why the unification fails.
   1. \f x y. (f x)(f y)
   2. \f g. (f g)(g f)
   3. \f x y. (f x,f y)
   4. \f x. f (fst x)(snd x)
   5. \f x y. f (inl x)(inr y)

   Note: the type of a term can easily be found out by using the ML compiler. For this reason, a correct answer without justification will not get any credit.

3. (30 pts) For each of the following types, say whether it is inhabited or not. Justify your answer by showing a term which such type, or by proving that such term cannot exist.
   1. A * B -> A + B
   2. A + B -> A * B
   3. (A + B -> C) -> (A -> C)
   4. (A -> B * C) -> (A -> B)
   5. (A -> B -> C) -> ((A -> B) -> C)

4. (20 pts) Define in ML the following functions:
   1. curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c, which takes a function f : 'a * 'b -> 'c and transforms it in its curried version (f takes a pair of arguments; its curried version takes the same arguments, but one after the other.)
   2. uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c, the inverse of curry. Namely, we want that, for every f and g of appropriate type, curry (uncurry f) = f and uncurry (curry g)) = g
   3. swap : ('a * 'b -> 'c) -> 'b * 'a -> 'c, which takes a function f : 'a * 'b -> 'c and transforms it into a function of type 'b * 'a -> 'c which gives the same result as f after swapping the arguments. Example: (swap append) (x,y) = append(y,x).
   4. the functions fst and snd of the grammar given in Lecture 12. Determining their type is part of the exercise.

5. (15 pts) Define in ML a data type "weight", whose elements represent weight measurements, either expressed in the English system (i.e. pounds and ounces), or in the metric system (i.e. kilos). Example: 12 pounds and 3 ounces, 10.5 kilos, etc. You can assume that 1 ounce is the smallest unit for the English system, i.e. we are not interested in representing weights like 3.2 ounces.

   Furthermore, define a function difference : weight -> weight -> weight that takes two weights and gives as result their difference. It does not matter whether the result is expressed in the metric or in the English system, but it's important to represent it as an object of type weight.

   Hint: define weight as a disjoint union type and use the my_case function defined in Lecture 12.