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);
      

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.

---

3. 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);
      

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
      

---

4. 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.

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);
      

---

5. 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);
      

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