let polymorphism

let polymorphismというのは，MLやHaskellで使われてる多相型を導入する方法で，多相型をletで束縛された値についてのみ推論する，という方針のこと．

let f = fun g x -> g x

という定義について，fの型は∀'a'b . ('a -> 'b) -> 'a -> 'bという多相型になる．しかし，その右辺fun g x -> ...の型自体は，実は多相型じゃない．('a -> 'b) -> 'a -> 'bという単相型だったりする．普通のプログラミングではこの制限はあんまり気にならないんだけど，たまに気になることもある．

人工的な例だけど，

% ocaml
# let hoge f = f (fun x -> x + 1) 1;
               f (fun x -> x ^ "a") "abc" in
    hoge (fun g x -> g x);;
This expression has type int but is here used with type string

こんなことになる．これはfがletで束縛された値じゃなくて引数だから，その型が多相型になれなかった，ということ．

さらに問題になるのは再帰的な定義．

# let rec f x = y
  and x () = f 1
  and y () = f "a";;
This expression has type string but is here used with type int

こんなことが起きる．このプログラムでは，fの型というのは，∀'a. 'a -> 'aになるんだけど，それはletの束縛が全て終ったあとなので，xとyの定義の最中では，letの型は単相型だったりする．そうすると，1の型intと"a"の型stringの間で矛盾になってしまう．*1

さて，上のプログラムを良く見ると，実はこれで良い．

# let f x = y;;
  let x () = f 1;;
  let y () = f "a";;

実は別に再帰的な定義になっていないんだから，別々のletに分解してあげれば，問題が無くなる．(HaskellのletはOCamlのlet recと同じ．OCamlの(rec)じゃないletは再帰的定義を許さないようになっている．)

というのが上のエントリの説明．

MLだとさらに値多相の制限もあるんだけど，Haskellだと関係無い．

*1:とここまで書いてから，これはlet polymorphismとは違う制限のような気もしてきた．細かく言えば，この制限はpolymorhic recursionが許されない，という制限なんだけど，let polymorphismとはもしかしたら直接関係無いかもしれない．