2006-09-07 [長年日記]
λ. Haskellに正格性注釈が無いのは何故か?
lethevert is a programmer - Haskell : モナドはややこしい のコメント欄での議論で、「何故HaskellにはCleanの正格性注釈にあたるものはないのだろうか?」と思い少し考えた。
GHC等の処理系では内部で正格性解析を行い、正格性の情報を利用して最適化などを行ってはいる。では、もし正格性の情報をユーザーから見えない内部情報ではなく、型として扱うことにしたらどうなるだろうか。とりあえず、一般の関数型の型構築子 (->) とは別に、正格な関数のための型構築子 (!->) を導入することにする。そして、(!->) a b のシンタックスシュガーとして !a -> b と書けることにもする。
関数 a -> b が必要とされる文脈では正格な関数 !a -> b も使えて欲しいから、!a -> b は a -> b のサブタイプになるのが望ましい。しかし、現在のHaskellにはサブタイプ関係は存在しないため、これを実現するには型システムにそれなりの変更を加える必要がある。障壁その1。
これが仮に解決したとして、次に「f x = 0」のような非正格な関数に対して、正格な関数の型を宣言したときにどうなるかを考えてみる。例えばこんな感じ。
f :: !Int -> Int f x = 0
このとき処理系はどのように振舞うべきか。
- 明らかな選択肢は「型エラー」とすることだろう。しかし、正格性解析は通常は型検査後に行われるので、型エラーにしようとするとややこしいことになる。また、正格性解析は型検査と違ってそもそも完全ではなく、正格な関数を解析機が正格と認識できない場合がある。そのような場合にエラーとなるのは(よほど分かり易い基準でも無い限り)どうかとも思う。
- それとは別の選択肢として、エラーにはせず正格な関数としてコンパイル/実行するという選択肢がある。ただ、これは同じ式が型によって違った意味を持つということを意味するので、一種のアドホック多相である。型クラス以外のアドホック多相をさらに導入するというのは、やはり躊躇われるものがある。
これらの問題に勝る正格性注釈のメリットがあるかと言えば……私には無いように思われる。*1
ただ、Haskellも正格なプログラムを書きやすくする方向へは進化していて、「f x = x `seq` 0」と書く代わりに「f !x = 0」と書くことの出来るBangパターンというものが GHC 6.5 には実装されている。*2
正格なプログラムが書きにくいという単純な問題はこのBangパターンでまず解決するだろう。それでもしも型レベルでしか解決できない問題が残ったとしたら、その時点で正格性注釈について議論すれば良いのではないかと思う。
2006-09-14 追記
lethervertさんが Clean の正格性注釈について、<URL:http://d.hatena.ne.jp/lethevert/20060911/p1> で解説してくれた。一見して型に見えるけど、実際は型ではないとのこと。これでCleanへの疑問が一つ解けた。
λ. 「デスノート」作者、小畑健容疑者逮捕
正直、車のコンソールボックス内に刃渡り8.6センチのアーミーナイフ(折りたたみ式)を持っていたくらいで……と思わなくもない。みせしめ感がひしひしと。ところで、産経の「ライトのせいで…「デスノート」作者、小畑健容疑者逮捕」という表題は狙っているのかな。
