### CSE 428: Solutions to exercises on Types

The superscript "(d)" stands for "difficult". Exercises similar to those marked with "(d)" might appear in candidacy exams, but not in the standard exams of CSE 428.

1. For each of the following ML expressions, give its most general type
1. ```   fn f => fn g => fn x => f (g x);
```
2. ```   fn f => fn (x,y) => f x;
```
3. ```   fn x => fn f => (x, (f x));
```

### Solution

1. ```   ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
```
2. ```   ('a -> 'b) -> 'a * 'c -> 'b
```
3. ```   'a -> ('a -> 'b) -> 'a * 'b
```

2. For each of the following functions, say whether it is typeable in ML, and, in the positive case, give its most general type.
1. ```   fun f g x = g (g x);
```
2. ```   fun f g x = (g g) x;
```
3. ```   fun f g x y = g(y,x);
```
4. ```   fun f g x = if x then true else g (f g true) x;
```
5. ```   fun f g x y = if x then y else g (x + y);
```
3. ### Solution

1. ```   ('a -> 'a) -> 'a -> 'a
```
2. Not typeable, because of the application of g to itself.
3. ```   ('a * 'b -> 'c) -> 'b -> 'a -> 'c
```
4. ```   (bool -> bool -> bool) -> bool -> bool
```
5. Not typeable, because x is used both as an integer and as a boolean.

4. For each of the following functions, say whether it is typeable in ML, and, in the positive case, give its most general type.
1. ```   fun f nil = nil
| f (x :: l) = (x :: nil) :: (f l);
```
2. ```   fun f nil = nil
| f (g :: l) = g (f l);
```
3. ```   fun f nil = nil
| f (nil :: l) = nil :: nil
| f l = l;
```
4. ```   fun f nil = nil
| f (nil :: l) = l :: nil
| f l = l;
```
5. ```   fun f nil k = nil
| f l nil = nil
| f (x :: l) (y :: k) = (x,y) :: (f l k);
```
5. ### Solution

1. ```   'a list -> 'a list list
```
2. ```   ('a list -> 'a list) list -> 'a list
```
3. ```   'a list list -> 'a list list
```
4. Not typeable, because the second and the third clauses are incompatible: l should be at the same time an 'a list and also an 'a list list.
5. ```   'a list -> 'b list -> ('a * 'b) list
```

6. For each of the following ML types, say whether it is inhabited or not. Justify the answer.
1. ```   ('a -> ('b -> 'c)) -> ('a -> 'b) -> ('a -> 'c)
```
2. ```   ('a -> 'b) -> ('b -> 'a)
```
3. ```   ('a * 'b) -> 'a
```
4. ```   'a -> ('a * 'b)
```
5. ```   ('a -> ('b -> 'c)) -> (('a * 'b) -> 'c)
```
6. ```   'a -> 'b -> 'a * 'b
```
7. ```   'a -> 'b -> 'a
```
8. ```   ('a * 'b) -> ('a -> 'c) -> ('c * 'b)
```

Hint: To show that a type A is inhabited, it is sufficient to show that there exists an ML term M which has type A.
To show that a type A is not inhabited, one can proceed in two ways:

• Argue (informally) that such a term M cannot be constructed, or
• Use the fact that a type can be inhabited only if, interpreted as a propositional formula, it is a tautology. Remember that, in the interpretation of types as formulas, -> stand for "logical implication" and * for "logical and". Note that this appraoch cannot be used to show that a type is inhabited, because being a (classical) tautology is only a necessary condition, but not sufficient.
7. ### Solution

1. Inhabited. It's the type of the function
```   fn f => fn g => fn x => (f x) (g x);
```
2. Not inhabited. In fact, the corresponding formula is not a tautology, as it is false for'a = false and 'b = true.
3. Inhabited. It's the type of the function
```   fn (x,y) => x;
```
4. Not inhabited. In fact, the corresponding formula is not a tautology, as it is false for 'a = true and 'b = false.
5. Inhabited. It's the type of the uncurry function:
```   fun uncurry f (x,y) = f x y;
```
6. Inhabited. It's the type of the function
```   fn x => fn y => (x,y);
```
7. Inhabited. It's the type of the function
```   fn x => fn y => x;
```
8. Inhabited. It's the type of the function
```   fn (x,y) => fn f => (f x, y);
```

8. Consider the following datatype declarations in ML:
```   datatype color = white | red | green | blue;
datatype 'a btree = emptybt | consbt of 'a * 'a btree * 'a btree;
datatype 'a tree = ctree of 'a * 'a tree list;
```
For each of the following functions, say whether it is typeable in ML (given the above declarations), and, in the positive case, give its most general type.
1. ```   fun f white = []
| f c = [consbt(c,emptybt,emptybt)];
```
2. ```   fun f emptybt = white
| f t = red;
```
3. ```   fun f emptybt = white
| f (ctree(c,l)) = c;
```
4. ```   fun f (ctree(c,l)) = c :: (f_aux l)
and
f_aux [] = []
| f_aux (t :: l) = (f t) @ (f_aux l);
```
9. ### Solution

1. ```   color -> color btree list
```
2. ```   'a btree -> color
```
3. Not typeable: the first clauses specifies a binary tree as argument of f, the second clause specifies a generic tree.
4. f has type
```   'a tree -> 'a list
```
f_aux has type
```   'a tree list -> 'a list
```