解答例  たとえばSML#の推論結果以下の通りである．

   # fun f x y z = x y z : int;
   val f = fn : [’a,’b.(’a  -> ’b  -> int)  -> ’a  -> ’b  -> int]
   # fun f x y z = x (y z) : int;
   val f = fn : [’a .(’a  -> int)  -> [’b .(’b  -> ’a)  -> ’b  -> int]]
   # fun f x y z = (x y z) : int;
   val f = fn : [’a,’b.(’a  -> ’b  -> int)  -> ’a  -> ’b  -> int]
   # fun f x y z = x y (z : int);
   val f = fn : [’a,’b.(’a  -> int  -> ’b)  -> ’a  -> int  -> ’b]
   # fun f x y z = x (y z : int);
   val f = fn : [’a .(int  -> ’a)  -> [’b .(’b  -> int)  -> ’b  -> ’a]]

解答例  Kは２番目の引数を捨てて1番目の引数を返す関数であるから， fun f x = K x (fn y => x (x 1)) はxを受け取りxを返す関数である． 従って，xの型をAとすると，fの型は A -> Aである． ただし，(fn y => x (x 1))があるため xの型はint -> intに制限される． そこで，fの型は(int -> int) -> int -> intとなる．

解答例 

1. 1.

   簡単には，
   if true then exp else $E{}_{\tau }$ とすればよい． if分を使わずに，より純粋なラムダ式で表現したければ，以下の手順で構築できる． 式$exp$の型を式$E{}_{\tau }$の型と強制的に一致させるには，それら二つの式 を，それらの型が等式で結ばれるような式の中に埋め込めばよい．以下はその典 型的な例である．
   (fn y => fn z => z (y $E{}_{\tau }$) (y $exp$)) この関数は$exp$と同一の動作をせず，要求を満さない． 求める式は，評価すると$exp$が得られるような式でなければならない． そこで，上記の$exp$の部分を引数とし，
   (fn x => ... (fn y =>fn z => z (y $E{}_{\tau }$) (y $exp$)) ... ) $exp$ と変形することを考える． 関数の本体全体はxと同一の意味をもつ式である必要がある． そこで，val K = fn x => fn y => xを使い，型を一致させるだ けに導入した上記の部分を捨て，$exp$自身を返すようにすればよい． 以下が要求を満す式の例である．
   (fn x => K x (fn y =>fn z => z (y E_τ) (y exp))) exp

2. 2.

   上記を応用すれば，以下のような例が考えられる．
   fn x => K x (fn y =>fn z => z (y $E{}_{\tau }$) (y x)) たとえば，fn x => K x (fn y =>fn z => z (y 1) (y x))¿は int -> int型の関数である．

解答例  以下にコード例とSML#で推論された型を示す。

   # fun higherTwice f x = f (f (K x (fn y => (y x, y id))));
   val higherTwice = fn : [’a .((’a  -> ’a)  -> ’a  -> ’a)  -> (’a  -> ’a)  -> ’a  -> ’a]