Type

Type, Type System, Type Inference などの話題

型推論

Programming_WayToHaskeller より、

nobsun(2004/09/23 00:54:22 JST): 括弧なしで、

> main = putStr “Hello,” ++ " ほげさん!\n"

と書くと何故、叱られるかというと。関数適用の結合力は、二項演算子 ++ の結合力より強いので、上は

> main = (putStr “Hello,”) ++ " ほげさん!\n"

と解釈されてしまいます。(putStr “Hello,”) の型は IO () で、" ほげ さん!\n" の型は String です。これは、++ の型 [a] -> [a] -> [a] と いうのに矛盾します。で、エラー。

Haskellの型推論のシステムが、上のように型を推論してくれて、プログラマ の意図と実際に書かれたプログラムとの齟齬を教えてくれます。こんなのが実 行時エラーだったらやだよねぇ。型推論マンセー！

WiLiKi:Shiro (2004/09/23 11:24:53 JST): でもでも、最初の関数の型が [Char] -> [Char] だったら、エラーは出ないよね。プログラマの意図を完全 に表現しきるのは無理なんだから、結局程度問題ってことにならない? (いや、 型推論があるのはうらやましいんだけどさ。)

nobsun(2004/09/24 15:42:36 JST): Haskell では、実行可能なプログラムは、 「プログラム全体」を通して、型の整合性がとれていることが保証されていま す。もちろん、2 + 3 という意図と 2 * 3 というプログラム(算譜)の表現の 齟齬を型で発見するのは無理ですが、2 + length “Hello” という意図と、算 譜に表れた 2 + “Hello” のタイポによるバグは、型推論で発見可能です。まぁ。 程度の問題といってしまうと確かにそうなんだけど。これが、相当にでかい差 だと思いますよ。

上の例だと putStr の型が [Char] -> [Char] だったら、++ とは矛盾しない けど、今度は、main と矛盾しますよね。main は特別な名前の変数で、main はプログラムの外側とやりとりをするアクションなので型は必ず IO a です。

一般にHaskellでは、型の整合さえとれていれば、実行可能なので、実は、プ ログラマの意図とは違うプログラムができる可能性はあります。しかし、バグ は、プログラマが自分の意図が正しいという前提のもとでは、算譜に転写する ときに入り込むものです。それゆえ、その間違いを犯したあとでも、プログラ ム全体で、型の整合がとれていることは稀だといっていいでしょう。

制約の強さの度合

Shiro(2004/09/24 18:31:04 JST): 一般的に動的型付けに対する静的型付けの そういうメリットを否定するつもりではなく、むしろ静的型付けの枠組のスペ クトルの中で、Haskellが選んでいる現在の形に対して、Haskellerがどういう 評価をしているかに興味があっての発言です。Haskellの現在の標準の選択は、 広い意味での静的型付けの唯一の解では無いはずで、「プログラマの意図」の 表現の度合で測ればより緩いものもよりきついものもあるはずですよね。それ を指して「程度問題」と言いました。

例えば、absの型は Num a => a -> a となっていますね。logの型は Floating a => a -> a です。従って、 log(-abs(-3)) という式の評価が出来ないこと は、実行時までわかりません。でも、absの値域やlogの定義閾が型で表現され ていたとすれば、上記の式が不正であることはコンパイル時に検出できるでしょ う。

別の例として、文字列処理ライブラリを作っているとします。非常に多くの関 数が [Char] -> [Char] という型を持つことでしょう。そのようなドメインで は、「バグがあったら型の整合がとれることは稀」とは言えないと思います。 実は、動的型付けもこのスペクトルの一番端にあるでしょう。可変長引数の話 を置いておけば、全ての関数は Anything -> Anything ってことでOK。

現実には、普通に使い易い落としどころを探っていって今の形に落ち着いてい るんだと思うんですね。緩くしてゆけば、プログラマの意図とは違うプログラ ムが実行できてしまう可能性が増える。きつくして行くと、プログラムがます ます書き難くなってゆく(表現が冗長になり、型システムを納得させるのも難 しくなる)。 Haskellの現在の形は、もともとはその最適化のカーブの極大点 にすぎないでしょう。

しかし、そこに「本質的」な差異があるとすれば、それは何なのでしょうか。

(例えば、全てはチューリングマシンだと言ってしまえば全ては程度問題になっ てしまいますが、再帰が出来るかできないかというポイントは、そのスペクト ルにおいてひとつのギャップになってると思うんですよ。現在のHaskellの型 システムが落ち着いた背景に、どちらにシフトするにせよギャップがあるんで、 かなり必然的にここに落ちるんだ、みたいな背景があるのかなあ、とか。)

nobsun(2004/09/27 11:08:33 JST): うまく、まとめられませんが。とりあえ ず、つらつらと。

私の場合は、Haskellの型システムは、「なかなか、いいんじゃない」という 感じです。Haskellの型推論は単純で、そのアルゴリズムはプログラマが自分 でやってもできる程度のものでしょう。ならば、そのくらいのチェック作業は、 処理系がやってくれてもいいかなと思います。

では、型推論の前提となる静的な強い型付けが、プログラミングのしやすさに どれほど制約を与えているかというと、これはプログラミングスタイルによる と思います。関数的に書くときには、型を意識しますので、静的な強い型付け はむしろあたりまえ、型推論機構があるのも当然(ないと不便)と思います。

型推論機構があることで、型が抽象化の強力な道具となり、プログラマの意図 の一部を型に載せることができます。もちろん、なにもかもが型に載るわけで はありませんし、値に依存するような型は使えると便利でしょうけど、今のと ころ決定版というべき実装法はありません。

「バグがあるとすれば、それは型のバグである」ということがいいたいのでは なく、タイポでは型のバグになることが多く、そのくらいはコンパイル時に弾 けるほうが良いでしょう、ということを言おうとしました。もちろん、2 + 3 とすべきところを 2 * 3 としたという類いのバグまではカバーしきれません ね。

文字列処理ライブラリを作っているとすると、API としては多くの関数が [Char] -> [Char] になるでしょうが、その関数の多くは、高階関数をつかっ て合成されるでしょう。高階関数は型としては、ずっと複雑で、合成の際に引 数順などの誤りを型でチェックできると楽ができると思いませんか？

私自身には、静的型付けを「きつくして行くと、プログラムがますます書き難 くなってゆく」という感覚があまりありません。表現が冗長になる度合にもよ りますが、型システムを納得させられないようなものは、私の場合、自明なバ グである可能性が高いので、そのようなものはさっさと弾いてもらうほうがい いのです。

Haskell の型システムのおとしどころは、機械的な静的型付けが実用的な範囲 で実装可能であるというところでしょうか。 (実際、Haskellの型システムの 基本は変ることはないでしょうけど、すこしずつ進化はしています。Haskell 98 の仕様にはない機能が Hugs や GHC に追加されていて、一部は事実上の標 準になっています。)

再帰の可不可と同様のギャップが静的型付け、動的型付けの間にあるといえる かどうかちょっとわからないです。スペクトルの端にあるか中間にあるかは決 定的にちがうような気もするしそうではないような気もします。ただ、関数の 型による抽象化を(意識的に)行うプログラミングスタイルかどうかの違いはあ るとおもいます。

Shiro: ふむ。納得です。静的型という制約を、抽象化のための思考の道具と して使うわけですね。動的型では、やはり思考がランタイムでの値中心になり がちなように思います。

高階関数の合成に関しては、静的型が圧倒的に有利だと思います。動的型だと 人間の頭で追わないとだめだし。引数順の誤りは、同じ議論になるので(引数 が同じ型だったら? という)アレですが、引数の数だけでもチェックできたら ずいぶん違うと思います

Last modified : 2009/06/08 05:53:43 JST