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.

The superscript "(s)" stands for "solution provided". You can find the solution of these exercises here.

1. ^(s) 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));
   

2. ^(s) 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. ^(s) 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);
      

4. ^(s) 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.
5. ^(s) 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);