プログラミング言語 Standard ML 入門 (問題の解答例)

3.2 型の多相性と多相関数

問 3.2

fn x => id id x の型を以下の手順で求め，’a -> ’a となることを確認せよ．

1.

id の型が ’a -> ’a であることを用いて， id id の型を求めよ．
2.

一般に，関数 $f$ が型 $\tau_{1}$ -> $\tau_{2}$ を持てば， fn x => $f$ x も型 $\tau_{1}$ -> $\tau_{2}$ を持つこと確かめよ．
3.

以上から，全体の型を求め，’a -> ’a となることを確認せよ．

解答例

1.

idの型は’a -> ’aである．ここで，’aは任意の型を表す多相型変数である．そこでid idの1番目のidと２番目のidの型をそれぞれ X -> XおよびY -> Yと置くことができる．前者が後者に適用されているので，X = Y -> Yであり，かつこの式全体の型はXである．よってid idの型はY -> Yと書ける．
2.

関数fが型A -> Bを持つとする．式f xの型が正しいとするとxの型はAであり，かつ式f xの型はBである．よって，式fn x => f xの型はA -> Bである．
3.

以上より，式fn x => id id xの型はid id xの型と同じ型，すなわちY -> Yである．さらに，Yは任意の型であるから，多相型変数を使うと，’a -> ’aと表される．

問 3.3

以下の各型を推定し，実際の型と比較せよ．

1.

twice cube
2.

fn x => twice id x
3.

fun thrice f x = f (f (f x))

解答例省略。

問 3.4

MLシステムは，各引数の型に関するすべての条件を満たす最も一般的な解を計算することによって，関数の最も一般的な多相型を計算する． twice の最も一般的な多相型が (’a -> ’a) -> ’a -> ’a であることを以下の手順で確かめよ．

1.

twice の定義に現れる各式の型をそれぞれ以下のように仮定する．

$\mbox{{\tt fun}}\ \underline{\mbox{{\tt twice}}}_{\tau_{1}}\ \underline{\mbox{% {\tt f}}}_{\tau_{2}}\ \underline{\mbox{{\tt x}}}_{\tau_{3}}=\underline{\mbox{{% \tt f\ \mbox{$\underline{\mbox{{\tt(f\ x)}}}_{\tau_{4}}$}}}}_{\tau_{5}}\mbox% {{\tt;}}$
2.

関数適用 $\underline{\mbox{{\tt(f\ x)}}}_{\tau_{4}}$ が型エラーを起こさないためには（1） f の型 $\tau_{2}$ は $\alpha$ -> $\beta$ の形をした関数型であり，（2）型 $\alpha$ は x の型 $\tau_{3}$ と等しく，（3）型 $\beta$ は (f x) の型の結果の $\tau_{4}$ と等しくなければならない．したがって，以下の等式が成立しなければならない．

$\tau_{2}=\tau_{3}\ \mbox{\tt->}{}\ \tau_{4}$

以上のような分析を他の要素についても行い，型の間に成り立つべき関係すべてを等式として書き出せ．
3.

2で生成した型に関する等式の $\tau_{1}$ に関する最も一般的な解を考え，それが twice の型(’a -> ’a) -> ’a -> ’aであることを確かめよ．

解答例 twiceの各変数に対して仮定された型 $\tau_{1},\ldots,\tau_{5}$ が満たすべき等式を以下のように書き下すことができる。

$\displaystyle\tau_{1}$	$\displaystyle=$	$\displaystyle\tau_{2}\longrightarrow\tau_{3}\longrightarrow\tau_{5}$
$\displaystyle\tau_{2}$	$\displaystyle=$	$\displaystyle\tau_{3}\longrightarrow\tau_{4}$
$\displaystyle\tau_{2}$	$\displaystyle=$	$\displaystyle\tau_{4}\longrightarrow\tau_{5}$

2番目と3番目の等式から、以下のような等式集合が導ける。

$\displaystyle\tau_{1}$	$\displaystyle=$	$\displaystyle\tau_{2}\longrightarrow\tau_{3}\longrightarrow\tau_{5}$
$\displaystyle\tau_{2}$	$\displaystyle=$	$\displaystyle\tau_{3}\longrightarrow\tau_{4}$
$\displaystyle\tau_{3}$	$\displaystyle=$	$\displaystyle\tau_{4}$
$\displaystyle\tau_{4}$	$\displaystyle=$	$\displaystyle\tau_{5}$

右辺の型に対するさらなる等式がない、解けた形の等式 $\tau_{4}=\tau_{5}$ を使い、変数 $\tau_{4}$ を消去すると、

$\displaystyle\tau_{1}$	$\displaystyle=$	$\displaystyle\tau_{2}\longrightarrow\tau_{3}\longrightarrow\tau_{5}$
$\displaystyle\tau_{2}$	$\displaystyle=$	$\displaystyle\tau_{3}\longrightarrow\tau_{5}$
$\displaystyle\tau_{3}$	$\displaystyle=$	$\displaystyle\tau_{5}$

を得る。これを繰り返すと、

\tau_{1}=(\tau_{5}\longrightarrow\tau_{5})\longrightarrow\tau_{5}% \longrightarrow\tau_{5}

を得る。 $\tau_{5}$ は、何も等式が存在しない自由変数である。この型を型変数’aとすると、

   twice : (’a -> ’a) -> ’a -> ’a

を得る。

問 3.5

以下の各プログラムについて，もしそれが型を持たなければ（つまり型エラーを含めば）その理由を説明し，型を持てばそのの最も一般的な多相型を推定せよ．

1.

fun S x y z = (x z) (y z)
2.

fun K x y = x
3.

fun A x y z = z y x
4.

fun B f g = f g g
5.

fun C x = x C
6.

fun D p a b = if p a then (b,a) else (a,b)

解答例

1.
fun S x y z = (x z) (y z)
SML#は以下のような型を推論する．
```
   # fun S x y z = (x z) (y z);
   val S = fn : [’a,’b,’c.(’a  -> ’b  -> ’c)  -> (’a  -> ’b)  -> ’a  -> ’c]
```
(補足）このSは，コンビネータ論理においてSコンビネータとして知られる基本関数である．さらに，この関数は，構成的論理学では，ヒルベルトシステムの公理 $(A\supset B\supset C)\supset(A\supset B)\supset(A\supset C)$ に対応している．興味のある読者は，大堀，ガリグ，西村，「コンピュータサイエンス入門，アルゴリズムとプログラミング言語」（岩波書店）の第2部を参照されたい．
2.
fun K x y = x
SML#は以下のような型を推論する．
```
   # fun K x y = x;
   val K = fn : [’a .’a  -> [’b .’b  -> ’a]]
```
(補足）このKは，コンビネータ論理においてKコンビネータとして知られる基本関数である．さらに，この関数は，構成的論理学では，ヒルベルトシステムの公理 $A\supset B\supset A$ に対応している．

fun A x y z = z y x
SML#は以下のような型を推論する．

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

fun B f g = f g g
SML#は以下のような型を推論する．

   # fun B f g = f g g;
   val B = fn : [’a,’b.(’a  -> ’a  -> ’b)  -> ’a  -> ’b]

5.

fun C x = x C
この式は，Cはを引数とする関数でありかつxはCを引数とする関数であることを要求している．したがって．Cの型は，Cを引数とする関数を引数とする関数となり，自分自身を部分に含む型となってしまい，そのような性質をもつ型は有限な範囲では存在しない．

fun D p a b = if p a then (b,a) else (a,b)
SML#は以下のような型を推論する．

   # fun D p a b = if p a then (b,a) else (a,b);
   val D = fn : [’a .(’a  -> bool)  -> ’a  -> ’a  -> ’a * ’a]

問 3.6

以下の関数およびプログラムはどのような型を持つか．
fun f x = f x; f 1; さらに，2番目の式の計算結果について考察せよ．

解答例 SML#は以下のような型を推論する．

   # fun f x = f x;
   val f = fn : [’a,’b.’a  -> ’b]

式f 1の定義から，f 1を呼び出し続ける無限ループ式であることがわかる．

この性質は，式の型からも分析することができる． fの型から，f 1の型は’aであることがわかる．この型は，f 1の結果がすべての型を持ちうることを示している．したがって，この式の計算が修了し，結果を返せば，その結果は総ての型をもつ値である．しかし，すべての型どころか，int型とreal型を同時にもつような値さえ存在しない．したがって，この式の計算が修了し結果を返すことはない．