事情により二日ばかし遅延評価となってしまい申し訳ありませんm(_ _)m

次元付き計算がいかに重要か

皆さん、量の計算をするうえで、単位を間違えちゃいけないよ、って教わったと思います。

180cm + 55kg = 235年　　とかいう式は間違っていて、意味を成しませんよね。

間違えるとどんなことがおこるかって？テストに落ちるとかでしょうか。

1983年には、カナダ航空の飛行機が、燃料補給時に単位を間違えたために(間違いの本質は、22300 kgの燃料を補給すべきところ、22300 ポンド しか補給しなかったというもの)飛行中にまさかの燃料切れに陥り、お祭り会場になっていた廃空港に緊急着陸を強いられ、あわや大惨事、というギムリ・グライダー事件が起こっています。

1999年、NASAの火星探査衛星マーズ・クライメート・オービターは、制御プログラムの力の単位にポンド重とニュートンが混在していたために、計画よりはるかに低い軌道に投入されてしまい、火星大気との摩擦により墜落してして失われてしまいました。

以上は、単位の間違いがとんでもない規模の被害を引き起こした事例ですが、その背後には無数の科学・技術上の間違いが、物理量の単位を無視し、ただの値として扱ったために起こっています。物理量はただの数値ではなく、どのような計算が正しいものなのか、ルールが決まっているのです。

ん？生の値に対して施せる計算にルールを課し、安全な計算しか行えないようにするにはどうすればいいかって？Haskellerの皆様ならもう、答えはおわかりですね。

既存のライブラリの問題点

そう、型を使えばいいのです。単位計算のルールを型システムにエンコードできれば、コンパイル時にすべての単位エラーを検出できるはずです。

このアイデア自体は目新しいものではありません。hackageにはすでに単位付き計算のライブラリがいくつもありました。

私もまず、これらのライブラリを使って、自分の仕事に関わるライブラリの物理量に型を付けていってみました。ところが、しだいに何かがおかしいことに気が付きはじめたのです。

例えば以下のコードをご覧ください。

敢えて全部掲載することはしません。とても長いからです。というかわずか1行の計算に対して何十行もの型がついていて、明らかに異常です。

いったい何が起こっているのでしょうか？

問題の原因

[道のり] = [速度] * [時間]
[力] = [質量] * [加速度]

これらの物理法則に登場する項はすべて「単位」ではなく「次元」であることにお気づきでしょうか。次元は単位の上位概念です。[キログラム]とか[ポンド]は[質量]の次元に属する単位であり、[メートル]とか[尺]とかは[長さ]の次元に属する単位です。物理法則、という大げさな言い方をしなくても、量にまつわる計算をするとこの種の計算式は必ず登場します。ある一定量の航空燃料は、それをキログラムで測ろうが、ポンドで測ろうが、同一の量を表すのです。

[道のり] = [速度] * [時間]　という公式は、速度の単位が何であっても成立します。したがって、[速度]のところにあてはまる量の単位に型をつけるとしたら、その型は具体型にはなりません。その単位の型は、速度という次元に属するという拘束条件付きの__型変数__になるはずです。

そう、単位が型になるのなら、物理法則はポリモーフィズムになるのです。

単位計算は意外と複雑です。立方メートル毎秒のような合成単位を扱うためには、単位記号同士の乗算、べき乗、比較等の演算を型レベルで行う必要があります。unittypedライブラリでは、型拘束条件とfundepによりこれらの型レベル演算を実装しています。その結果、型レベル演算を積み重ねるにつれて、型拘束条件がみるみる膨張してしまったのでした。

Unitsライブラリにおける発想の転換

私とRichard A. Eisenbergはこの問題を解決すべく、あらたにunitsパッケージを開発しました。

unittypedライブラリの物理量型は、「次元」「単位」「値の型」の3つを型引数にとっていました。

これに対し、新開発のunitsライブラリでは、物理量型は、「次元」「単位系」「値の型」の3つを型引数にとります。

単位系とは何でしょうか？有名な単位系には、MKSA単位系、CGS単位系、尺貫法単位系などがあります。ある単位系では、どの次元の物理量をどの単位で表すか、一意に決まっています。したがって、単位系を変数にとれば、個々の単位を変数にとる必要がなくなるのです。

以下のHaskellプログラムは、unitsライブラリをもちいて [体積] = [質量] ÷ [密度] を表現したところです。

ℓという、単位系を表す__類__に属する変数と、値の型であるf という二つの型変数だけで、すっきり書けていることがおわかりいただけるかと思います。同じことをunittypedライブラリを用いて書くと以下のようになります。

年を越してお持ち帰りいただけるお菓子

さて、このままでは何だか自分の研究の宣伝になっちゃって嫌ですね。アドベントカレンダーには1日ごとにささやかなお菓子が入っているはずです。このお話から持ち帰れる、再利用可能なお菓子とは何でしょうか？

1つ目は、「物理法則は単位についてポリモーフィックだ」という発見です。最近では強力な型をもつ言語がいろいろ登場してきて実に楽しいことになっています。そこでもし、あなたが、あなたの好みの言語の型システムで量の計算を実装しようとすることがあったら、ぜひ「単位をポリモーフィックにできるか」にご配慮ください。さもないと、実際の物理を殴れないかも？

2つ目は、GHC7.8の型システムは、次元付き計算をエンコードできるほどに強力だということです。unitsライブラリには、単位計算を型レベルで実現するための型レベル道具がいろいろ含まれていて整数
や集合
などは、他にも使いまわしが効くのではないかと思われます。

詳細

この記事は、今年の夏にICFP付設のHaskell 2014イベントで発表した内容を日本語で紹介するものです。詳細については、以下の資料もあわせてごらんください。

今年はプログラミングを始めて約２０年、Haskellと出会って約１０年。情報学科を出たわけでもない私がついに国際学会でHaskellの発表をするところまでこれたのも、過去に文章を書いてくれた、私の質問に答えてくれたいろんな誰かのお蔭です。今回はLazyになってしまいましたが、今後とも勉強をつづけて、いろんな形でささやかながら文章の形での恩返しもしていければなあと思います。