OCaml の let と let rec はなぜ別扱いになっているのか、決定版、もしくは OCaml 暦十何年だったか忘れたけど仕事で Haskell を一年使ってみた

OCaml Haskell

はじめに断っておくが、全部Pros/Consのあるデザインチョイスなので、こうじゃなきゃいけないってことではない。ただ、 OCaml はこの選択をした、そいう事だ。

前回の「経験15年の OCaml ユーザーが Haskell を仕事で半年使ってみた」 http://d.hatena.ne.jp/camlspotter/20101212/1292165692 のような易しい文章ではないのでわからない人はとことん判らないだろう。まあ勘弁して欲しい。

あと、面倒だろうが、読む人は全部常体を敬体にして最後に「と思います」をつけて読んでくれ。ください、と思います。

Shadowing は便利であると思っている

OCaml の let は非再帰なので以前定義された名前に別の値の束縛をオーバーライドできる。OCaml の人はこれが便利だと思っており皆普通に使っている。詳しくは http://d.hatena.ne.jp/camlspotter/20091018/1255867603 。一方、let rec の本質は再帰なので当然この shadowing はできない。

非再帰let による shadowing が便利と思うかどうかは宗教の問題だろう。OCaml のある人(これは少なくとも私だ)は shadowing が無いと、もはや必要のない値の束縛にアクセスできるので危険だと思っているし Haskell のある人(これは stackoverflow かどっかで見た)は shadowing は逆に古い値の束縛と混同して危険だと言っている。両者とも、さもそれが唯一無二の真理かの様に語っている。

ちなみに Haskell でもパターンマッチで shadowing は当然可能である。なぜ shadowing のある(当然非再帰な) let があってはいけないのか、上の人の理由ではうまく説明できない。そう突っ込むと、そもそも一時的な名前を使う事自体がいけない、時代は point free ですよ! とか呟いて、短いが誰も読めない暗号コードを書いて悦に入っている。典型的な Haskell ゴルフスパイラル症候群である。当然こういう人と仕事をしてはいけない。変なコードを読まされるのは君だ。

Eager な言語では let rec は原則として即値しか取れない

あまり言い切りは良くないが…

Eager な言語では束縛が行われる際、定義の式の評価が行われる。式が定数や lambda abstraction ならば何も計算は行われない(というと語弊はある、lambda abstraction ならば closure を生成しなければいけないから何かしら CPU が計算を行う。まあ、β reduction を意味論とする視点からは定義式を評価しても βreduction は発生しない、と言えばいいか。)それ以外の関数適用等の形の場合は束縛時に何かしらの計算が(βreduction)が行われる。

束縛時に計算が行われる式、が、その計算中に再帰的に自分自身を使用していると、eager な言語ではその場で無限ループに陥る。例えば let rec x = 1 + x など。よってこのような再帰定義は eager な言語では無意味なので常識的には拒否した方が良い。(別にそこで無限ループになっても気にしないのであれば、拒否しなくても構わない。また世の中に変態言語が一つ増えるだけである。) そのため OCaml ではこの様な式は中間言語へのコンパイル時に(型の問題ではないので型推論の時点ではない)はねられる。　"Error: This kind of expression is not allowed as right-hand side of `let rec'" という奴だ。OCaml の経験がある奴なら一度はこのエラーを見たことがあるだろう。見てなければまだまだ経験が足りないか、完璧駱駝超人に違いない :-P

let と let rec の区別に戻ろう。束縛時の無限ループを避けるために、let rec の右辺には原則として即値しか取れない。計算を行う式の結果を変数に束縛したいなら非再帰の let がどうしても必要だ、これが OCaml が取ったデザインだ。事実計算がある式を let rec の右辺に書くとはねられる。

ちなみに、実際の OCaml ではこの「束縛時に何かしらの計算が行われる式」の定義は βreduction が起こるかどうか、とは完全には一致しない。マニュアルでもあまり詳しく触れず、正確な条件は記載されていない。まあ型理論を知らなくても型に縛られることはできるのと同じで、知る必要もないのだが…詳しくは translcore.ml の check_recursive_lambda を見てもらうしかない。名前使用の解析を行って、束縛時計算で再帰が行われれば、はねる、という実装になっているはずだ。例えば let rec x = 1 + 2 は計算を行うが、文面はともかく中身は再帰ではないのでオッケーである。let rec f = prerr_endline "hello"; let cache = ref [] in fun () -> f () は再帰ではあるし束縛時計算は行われるが、その束縛時計算では再帰呼び出しを行わない(テキトーに言うと closure でストップされる)からこれも構わない。なぜこんな条件になっているかと言えば、この f みたいなのが定義できて、便利だから、だ。（これは確か私の師匠の Pierre Weis が caml-list かどこかで指摘していたと思う)

いや待て、コンパイラが計算のある再帰式を自動的にはねることが出来るのなら、let と let rec の区別はいらないのではないか？全てデフォルト let rec にして非再帰の式だけ let にすればよい。確かにそうだが…それが果たしてプログラマにとって嬉しいかどうか疑問だ。もしそんな事をするとプログラマはより多くの "Error: This kind of expression is not allowed as right-hand side of `let rec'" を見ることになるに違いない。そして今まで以上の量の「なんで俺のイケテル定義が OCaml に受け入れられないんだクソか！」という質問に、「束縛時に計算をする式」とか「βreduction」とか、 「check_recursive_lambda 読めやヴォケ」などという君が今まさに読んできたような血も涙もない答を我々はしなければいけなくなりヒューマニストとしてかなりメンドウクサイ。 いずれにせよ eager な世界では再帰定義の際に計算を避けるのをプログラマが意識しなければいけないのは避け様がない。ならば明確に再帰と非再帰を syntactic に分けておいたほうが意識できて良いのではないか。(あまり強い信念ではない)

さらに余談を重ねるならば、let rec ones = 1 :: ones という定義は「計算が行われない式」になる。なぜなら (::) は data constructor であって関数ではないので、「計算」は行われない、と OCaml は考えるからだ。そのためこの式は受け入れられ、ループのあるリスト(もはやリストではない!)を ones に束縛する。ones はいくらでも cdr (tail)を辿っていけるが、全体として有限の構造になっている。もちろん、 Haskell の [0..] の様な構造は eager evaluation では計算を伴う上、無限構造になるのでリストとしては定義できない。この様な構造を OCaml で定義する場合には list ではなく stream などの遅延構造を使う事になる。

同じ理由だと推測されるが SML でも val と fun という二種類の束縛がある。let/let rec と val/fun の意味は少し違う。let/let rec は再帰の有無をコントロールする。val/fun は syntactic に取れる定義の種類を制限する。let では非再帰な関数は定義できるけれども val では出来ない。関数は全て fun で定義しなくてはならない。そして fun は再帰である。(val x = fn x => という形なら val でも関数を定義できる。val rec というのもあるようだ。この SML の val と fun の区別の必要性は私には良く判らない。)

Haskell は lazy なのでこのような問題は無い。全ての定義は thunk を定義していると考えられる、そして thunk は implicit な lambda 抽象が入っていると考えてこの場合問題ないので、全ては即値になり、束縛時計算は起こらない。よって let/let rec の区別をする必要が無い。Let 束縛は全て OCaml の言うところの let rec で構わない。例えば OCaml では駄目だった x = x + 1 は Haskell では (OCaml 風にテキトーに書くと) let rec x () = x () + 1 の事になり、問題無い事がわかる。もちろん、こんな関数は無限ループするだけなので何の役にもたたないけれども。

時々、束縛時計算が行われるので束縛データのサイズが不明だから alloc 出来ないと答えている人がいるがこれもオカシイ話だ。型は付くんだし、C じゃねーんだから。

型推論の問題ではない

let rec x = x + 1 が型推論の時点ではなく、中間言語へのコンパイルの時点で蹴られる、と上に書いた。let/let rec の区別は本質的には型推論とは何の関係もない。事実 let/let rec の違いは自分自身に free type variable を持たせて定義式の型推論を行わせるか、どうかの違いしかない(typecore.ml type_let 参照)。

「SCC を計算すればいいのにサボっている」は間違い

これは、値の使用グラフを作ってその SCC (Strongly Connected Component) を計算すれば let/let rec の区別は付くはずなので、let/let rec の区別は必要ない。必要なのは型推論器の実装に手を抜いているから、という意見だ。

Haskell ユーザーはついこの批判をしてしまうように見受けられる。(実際私もこの主張を日本語であれ英語であれ何度か見ている。) なぜなら Haskell では実際に SCC を計算する事で let束縛の入れ子をフラットにしたまま多相的なプログラムを書くことが出来るからだ。例えば where の例を思い出そう:

hoge = ....
  where
    fuga = ...
    heke x = ...
    poko x y = ...
    ダラダラァッ

この様に Haskell では let を完全に順番を気にせずフラットに定義を書くことが出来るが、これは lazy evaluation だから出来ることだ。上でも言ったように全ては thunk であるから束縛時のコード実行は行われない。すなわちどんな順番に束縛を書こうとも問題は無いのだ。

ただし、これには落とし穴がある。全て thunk があるからといってこれを一つの let polymorphism に押し込んで型付を行うと多相性が低くなる場合があるからだ:

twin_map [] = []
twin_map (x:xs) = (twin x, twin "hello") : twin_map xs

twin x = (x,x)

この例自体の意味は全く無いのだが…まあ、 twin_map [1,2,3] は [( (1,1), ("hello", "hello") ), ((2,2), ("hello", "hello") ), ( (3,3), ("hello", "hello") )] を返す。問題ない。twin_map の型は [a] -> [(a,a), (String, String)]。この多相型を得るために、 Haskell は上のコードを OCaml で書かれた次に相当するものに変換する(記号の読み替えは面倒だがまあなんとかなるだろう):

let twin x = (x,x)
let rec twin_map = function
  | [] -> []
  | (x::xs) -> (twin x, twin "hello") :: twin_map xs

これは実際 OCaml でちゃんと定義でき型も Haskell の多相型と同じものが得られる。let 束縛が二段になっている事に注目して欲しい。これが一段ではいけない:

let rec twin x = (x, x)
and twin_map = function
  | [] -> []
  | (x::xs) -> (twin x, twin "hello") :: twin_map xs

この定義を用いると twin_map の型は(Haskell で書くと) [String] -> [( (String, String), (String, String) )] になってしまい、多相性が失われてしまう。この定義では twin_map [1,2,3] はもはや welltyped ではない!

何故か？これは話し出すと ML の型推論の授業を始めなければいけないし授業料をもらうと副業規定とかいろいろあるし確定申告も面倒だし「講演料払込願」とかいう方眼紙excelを招待されている本人が自らが書かなければならないのでうざいからしない。一言で言うと ML や Haskell が根ざしている Hindley Milner の型推論システムの特徴として、let 束縛中で定義されつつある値はその定義中では多相型を持てない。twin と twin_map を一段の let rec で定義した例では twin は一種類の型にしか対応できない。そして twin "hello" と文字列に使ってしまっている。それに引きずられて twin x のパラメータ x の型も string になってしまう。twin_map も同様である。

これを二段の let 多相に分けて、まず twin の型を求め(これは多相だ。a -> (a,a) になる)それからこの多相の twin を使って twin_map を型推論すれば、めでたく多相的な twin_map が得られる。

この出来るだけ高い多相性を得るために Haskell は束縛コード中の名前の使用グラフの SCC (Strongly Connected Component) を計算してフラットな let では無く階層状の let に分けた上で型推論を行っている。(ソースコードを見たわけじゃあないが、そうしないと出来るはずがない。) SCC はウィキペでも見て勉強して欲しい。

さて…長くなったが、「SCC を計算すれば let/let rec の区別は必要ないはずだ、なぜ OCaml では必要なのか？」の指摘は的外れである。指摘すべきは入れ子である。「SCC を計算すれば、let の入れ子をプログラマがわざわざ書く必要はなくなるはずだ、何でわざわざ ML では let let let と明示的に書かなきゃならないんだ面倒な」である。

さて、そうだろうか。残念ながら、SCC を計算して云々は eager evaluation の言語ではうまくいかない。Eager な言語では今までも見てきたように、束縛時に計算が行われる可能性があり、その計算は定義の順番に行われる(絶対に行われる必要も無いがプログラムが書かれた順番に行われるほうが自然だろう)。twin と twin_map の例でも判るとおり、SCC を計算して複数の let を自動的に配置する場合、定義の順番がプログラムテキストと入れ替わる可能性がある。定義の順番が入れ替われば、計算の順序も変わる。あまり意味論的によろしくない。特に、その束縛時計算に副作用があれば、この順序の勝手な入れ替えは致命的だ。プログラマはフラットな束縛列を書き、型推論が SCC で勝手に let を作ってやる、これは eager な言語では余計なお節介で益はない。(Eager でも pure な言語ならやってもいいかもしれないが、それでも semantics が勝手に変更される、と言う事だから、気味が悪い。この件に関しては Pure/Impure より Lazy/Eager の問題が主だと思う。)

もちろん let の入れ子を無くすために、SCC 入れて let 入れ子を自動的に構成し、eager である事を考慮して、その入れ子が元の文面の順番と矛盾したらエラー、という事をしても良いが…また「どうして俺のイケテルコードはコンパイラに弾かれるんだ気に食わん」という質問がやってくるのでヒューマニストの我々の心が折れる事になる。Eager な言語では let 束縛の順序はプログラマが意識して書かざるを得ないのだ。

一転、Haskell は lazy な言語であるので、束縛順を気にしなくてもプログラムの semantics にはさほど影響がない。そのため、where の様に定義を後置することも可能になっている。フラットな定義列を書いても型推論が宜しく多相性が最大になるように定義を解析してくれる。

ところで、これは私の嗜好なのだが、この Haskell のフラットな定義はあまり頂けない。インデントに意味があり、手動で行わなければいけない Haskell ではインデント修正を嫌ってどうしてもプログラムが横に長くなる。(ならない？ならばそれは君が本当に気をつけてよいコードを書いているか(皮肉ではなく本当に尊敬できる事だ)、ろくにコードを書いて無いかどちらかだ) 横に長くなるのを避けるには where のようなフラットな文法が好まれるようだ。書く分には構わないだろうが…他人の書いた where を読むほうは大変である。

まずどこから読むべきかわからない。読み手が SCC 解析を行わなければならないからだ。コードリーディングの為の SCC ツールがあるわけでもなし、できるだけ locality が判るように入れ子 let や where を書いてくれたほうが読みやすいのだが…どうもそういう文化は Haskell には余り無いようだ。"Write once, rewrite again from scratch if needed, you can always justify yourself using the category mumbo-jambo" な勘違いが少なからず蔓延している世界に思えてならない。

ちなみに OCaml 4.00.0 からは非再起定義にもかかわらず rec が使われている場合はコンパイラが警告を発することができる。つまり、SCC とまではいかないがコンパイラはちゃんと再帰定義かどうか確認しているのである。

歴史

let rec という字面は ML言語族のはじまりである Milner らの Edingburgh LCF ML に letrec というキーワードで既に見られる(1987年)。今までに見てきたように再帰非再起束縛の使い分けを行いたい場合、これらの束縛宣言を syntactic に区別する必要があるが、それは既に ML が生まれたときから持っていたことになる。コンピュータサイエンティストに限らず、研究者は先人の仕事には敬意を示し、よほど強い理由が無い限り変更は行わないものだ。rec キモイ！という方は是非 Milner 先生に喧嘩を売っていただきたい。あの世でな！(2010年三月没)

私見

もし伝統をガン無視してよいのならば…私にもアイデアがある。基本的には再帰非再起は区別しそのための束縛宣言構文を二つ用意するというのは同じ:

  • let は全て再帰定義とする (let と書けば普通の let rec になる)
  • shadowing を行いたい場合は let! を使う ! は override するよ！という意思表示
  • let! で shadowing が発生していない場合はエラーとする

つまり再帰非再起を直接区別するのではなく shadowing かどうかを区別するのである。結構良いと思うがどうだろうか。let は全て再帰となるが、上でも書いたように束縛時計算が行われる式では即時再帰呼び出しは行えないように制限を入れなければいけない。そうすると「どうしてこの俺のコードが動かんのだ」というクレームが来て心折れることになるが… Shadowing を起こす事を明快に宣言することで Haskell 的 let に慣れている人でも抵抗感は少ないというメリットがある。

まとめ

なぜ let/let rec の区別が OCaml にあるのか:

  • サボっているわけではない
  • 非再帰 let による shadowing は便利だと思っている
  • Eager な言語は 再帰let で取れる式に制限がある
  • Lazy な言語では let 入れ子を省略してフラットな定義列にしても型推論器がよろしくやってくれる
  • Eager な言語では、それはプログラムの意味を変えてしまうので不適当 (これは let/let rec の区別とは別の問題)

これだけ見ると Haskell は lazy で型推論器がよろしくやってくれるし最高だね! と読めないことも無いが… lazy には lazy の問題がある。

Eager では意味が無いと蹴られていた式に意味を持たせよう、これが lazy evaluation の一面だ。例えば、f x = x : f (x + 1) つまり [x .. ] に意味を持たせよう。確かに、こういう lazy を利用した簡潔な定義に魅力があるけれども、これもトレードオフがある。 例えば x = 1 + x は eager では意味のない定義だから弾かれる(上の let rec x = 1 + x) が、lazy だとこれは意味がある!ことになっている。どう見ても実用的な意味は無いのだが。(ここで bottom がなんたらとか言っている輩はこんなブログを読むのはやめて、さっさと大学か研究所に戻ったほうがいい。)

Haskell で x = 1 + x のような式を書いていて、はじめのうちは何も問題が無かったのに、プログラムの全然関係無い部分を(無いことは無いのだ、人間が気づけないだけだ)ちょっと変えたら人智を超える call-by-need で突然無限ループに陥った、どこだどこだどこでおかしくなったんだ？そういうことが無い人はいないはずだ。(それが無いならロクに Haskell を書いたことないか、Haskell 完璧超人に違いない :-P)

他にも計算量が読みきれない、メモリリークが起こりやすいなど lazy に起因する問題は目立たないが真面目に開発しているとジワジワとボディブローの様に効いて来る。ここんとこを過小評価したり、無視して lazy イイね!皆 Haskell 使わないなんてアホですよ!ではお話にならない。今や Haskell もカッコいいカッコいいとか言ってるだけじゃなくて、こういう落とし穴があってこう避けるべきだ、という段階に差し掛かっているのではないかと思う。それを怠っていると未来の君の同僚に苦しめられる事になるぞ!!

一年触って得心したのだが Haskell は laziness の部分で本当に人を選ぶ言語だと思う。ソビエトロシアでは君が Haskell を選ぶ！だったそうだがベルリンの壁が壊れてからは最早それは真ではない。プロトタイピングなら誰が触っても Haskell はとても良い言語とは思うが、 複雑で長期に渡るチームでのプロジェクトの場合、あくまでも真摯にコードに向き合える選ばれた人間にしか Haskell を触らせるべきではない。もしそういう人だけでチームを作ればそれはとても素敵な Haskell プロジェクトになるだろう。まあ、発想を変えて駄目な奴だけでチームを組む、お互いのコードは読まない、というのもアリだが、この場合、私は遠慮したいネ。

全てはトレードオフ。コインの表と裏。