このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

型の次元解析

さらに「ラムダ計算、論理、圏」セミナーへの補足・応答: rst76さんから絵を拝借:

この絵で、E3, E2, E1が同じなの違うの? ということを何人もの人が気にしていたようですから補足しておきます。

このようなことを確認したかったら、型の“次元解析”をすればすぐに分かります。g:A, B, X → Y とします。ここで、A, B, X, Yは変数じゃなくて型(の名前)です。gをフルカリー化したg^^^は、I → ((YX)B)A です。Iはユニット型で、“引数なし関数の引数の型”はIだとします。I = {*}, f() = f(*) と考えればいいでしょう。

括弧が煩雑になるので、((YX)B)A をYX B Aと書いてもよいとします。指数による表記は圏論では標準的です; Haskellなら A -> B -> X -> Y と書きますね。

図のE3は、「YX B AとA」をもらってYX Bを出力するので、

  • E3: YX B A, A → YX B

同様に考えて:

  • E2: YX B, B → YX
  • E1: YX, X → Y

… という次第で、E3, E2, E1は、それぞれ異なった入出力の型を持ちます。

ちょっと先走って、型推論と命題論理の対応を使えば、オダンゴ図と同じことを次のような証明図でも書けます。


A⊃(B⊃(X⊃Y)) A
-------------------[E3のモダスポネンス]
B⊃(X⊃Y) B
-------------------[E2のモダスポネンス]
X⊃Y X
-------------------[E1のモダスポネンス]
Y

この証明図の存在から、A⊃(B⊃(X⊃Y)), A, B, X |- Y が言えます。これはまー要するに、「h∈YX B A, a∈A, b∈B, x∈X が与えられたなら、適用を繰り返して、値 y∈Y が得られますよ」ってこと。

ちなみに、物理量の次元解析は「次元+次元・解析 -- 現象と量の型チェック機構」参照。計算と物理は関係なさそうだけど、根は同じです。