CatyScriptと総称ラムダ計算

CatyScriptの総称機能がだいぶちゃんとしてきたので、それに絡めて総称ラムダ計算の説明をしておこうかな、と。

ここで言う「総称」は「型変数を含む」という意味です。そして、総称をサポートするとは次のことです。

1. 型変数を含む型表現を扱う。
2. 型変数を含むスクリプトコードを扱う。

総称をサポートする動機は、型定義／型宣言を容易にするためです。型定義／型宣言を（徹底的に）利用する動機は、実行時の安全性をできる限り保証したいからです。人間の間違いを早く発見したいのです。

内容：

1. 総称型の概要
2. プロファイルの扱い方
3. 総称の式（項）の扱い方
4. ほんとに大丈夫？

総称型の概要

α、βなどは型変数を含むかもしれない型表現（type expression）とします*1。こういう表現（式、expression）を型スキームと呼ぶこともあります。Tを型変数として、ΛT.α を、型表現（型スキーム）αの型抽象だとします。総称型とは、型抽象された型表現のことです*2。

CatyScriptでは、総称型を次のように定義します。

/* 長さ2の配列で、2つの項目の型が同じもの */
type PairOf<T> = [T, T];

PairOfが定義された総称型の名前です。定義とは、名前と無名の実体を結び付けることなので、左辺に名前だけ、右辺に無名の型を書くことにすると*3：

PairOf = type<T>[T, T];

type<T>[T, T] がラムダ抽象された型表現です。キーワードtypeが大文字ラムダに対応します。型抽象をもとの大文字ラムダを使って書くなら、ΛT.[T, T] となります。

型適用は、α<β>、α<β, γ> の形で書きます。もしそうしたいなら、任意のα, βに対して α<β> を定義できますが、CatyScriptでは次の制限を設けています。

• α<β> が定義できるのは、αが ΛT.α' の形をしているときだけ。
• α<β, γ> が定義できるのは、αが ΛS,T.α' の形をしているときだけ。
• 以下同様に、n個の型引数の適用の条件がある。

例えば、(type<T>[T, T])<string> は正しい型適用ですが、(type<T>[T, T])<string, integer> とか、integer<string> とかは禁止しています。こういう制限を付けたほうが、むしろ混乱が起きにくいと考えました。

αが型表現のとき、αに自由に出現する型変数Tをβで置き換えたものを α《β/T》 と書きましょう。普通は、α[β/T] とか α{β/T} とか書くのですが、'[', ']'、'{', '}' だとメタな記号であることが分かりにくいので、実際の型表現には登場しない 《, 》 にしました。（「型推論に関わる論理の概念と用語 その6：substitutionの記法」も参照。）

型適用 (ΛT.α)<β> は、型置換 α《β/T》 により計算します。例えば、(ΛT.[T, T])<string> = ([T, T])《string/T》 = [string, string] です。型抽象、型適用、型置換は、通常の抽象、適用、置換とまったく同じように計算できます。「高階関数を持たないが型の順序を持つラムダ計算」で述べた計算方法がそのまま総称型の計算にも使えます。

プロファイルの扱い方

圏論で、射fが「dom(f) = A, cod(f) = B」のとき、f:A→B と書きます。このときの A→B をfのプロファイルと呼びます。型付きラムダ計算では、プロファイルを次のように扱えます； Eが式、α、β は型表現だとして、Eに指数型 α->β で型注釈を付けます。すると、E:(α->β) となります。これは、式Eがα型の入力を受け取ってβ型の値を返すことを意味するので、プロファイルになっています。

ところが、CatyScriptでは次の問題があります。

1. 自由変数には型がない。（なにしろ、自由だからな :-)）
2. 型システムに指数型がない。（ガーン、なんてこったい）

そこで、次のようにします。

1. 自由変数をラムダ束縛（普通のラムダ抽象）するとき、同時に型付けする。
2. プロファイルを型とは別なものとして扱う。

Eが、自由変数x, yを含むかもしれない式（項、スクリプトコード）とします。x, yに前もって型はありません。α、βを型表現として、λx:α,y:β.E の形でラムダ抽象を行います。これにより、変数x, yはラムダ束縛されると同時に型を持つことになります。さらに、λx:α,y:β->γ.E という書き方で、E全体の型がγであることを示します。矢印 '->' は指数型の構成子ではなく、単なる区切り記号です。

今出てきた λx:α,y:β->γ は、「(1)ラムダ抽象、(2)変数の型付け、(3)式全体の型の宣言」を同時に行う操作となります。CatyScriptではこの3つの操作を切り離して行えないのです。ラムダ抽象をするときは、もれなく「変数の型付けと式全体の形宣言」も付いてきます。したがって、ラムダ抽象された式は自動的・必然的にプロファイルを持つことになります。

CatyScripでは、標準入力は無名な変数として与えられます。ホントの無名だと書きようがないので、仮に「-（ハイフン）」で表現すると、λ-:α->β.E のようなラムダ抽象は、標準入力の型がαで、式Eの型がβであることを示します。ダミーの名前「-」は省略していいとすると、λα->β.E となります。この記法、プロファイルっぽいでしょ。

CatyScriptでは、ラムダ抽象された式（スクリプトコードが式）をコマンドと呼びます。キーワードcommandを使って、λx:α,y:β->γ.E を command x:α,y:β->γ {E} と書きます*4。λα->β.E なら command α->β {E} ですね。

適用は、コマンドラインパラメータ適用と標準入力適用で書き方が変わります。command α->β {E} に式Fを標準入力適用するときは、 F | (command α->β {E}) と書きます（コマンドライン適用の説明は省略）。普通の書き方だと、(λ-:α->β.E)・F なので左右が逆になります。左右を逆にすることによって、（それだけで）人間にとっての読み書きは格段に楽になります。

総称の式（項）の扱い方

λx:α,y:β->γ.E のようにラムダ抽象された式をコマンドと呼ぶと言いましたが、さらにこれを型抽象すると総称コマンドになります。型抽象は大文字Λで表現すると、ΛT.(λx:α,y:β->γ.E) のようになります。CatyScript風の書き方だと command<T> x:α,y:β->γ {E} です。キーワード command は、小文字λと大文字Λの抽象を同時にしてしまうダブルラムダ作用素なのです*5。

型パラメータを持たないコマンドも、たまたま型パラメータ個数が0個なのだとみなせば、あらゆるコマンドは総称コマンドです。総称コマンドの実行には、型パラメータ（Λで束縛された型変数）の具体化と値パラメータ（λで束縛された変数）の具体化の二段階が必要です。

値パラメータの扱いはまーいいとして、型パラメータの具体化の手順を考えてみます。型の具体化は、型置換の特別な場合に過ぎません。つまり、総称の式（項、スクリプトコード）に対する型置換が定義できればよいことになります。型置換操作で置換の対象にすべき場所は二種類しかありません。

1. Eが式、αが型表現だとして、型適用 E<α> のαが型置換の対象となる。
2. Eが式、x₁, ..., x_n が変数、α₁, ..., α_n, β が型表現だとして、ラムダ抽象 λx₁:α₁, ..., x_n:α_n->β.E の α₁, ..., α_n, β が型置換の対象となる。

一番目は型引数、二番目はプロファイルなので「型置換は、型引数かプロファイルに対して行う」となります。

式（項、スクリプトコード）に対する型置換をちゃんと定義するには、式の構文的構成に沿った帰納的な定義になりますが、その本質は次のようになります。型表現に対する型置換を一般の式にも拡張するのです。

1. (E<α>)《γ₁/T₁, ..., γ_k/T_k》 ⇒ (E《γ₁/T₁, ..., γ_k/T_k》)<α《γ₁/T₁, ..., γ_k/T_k》>
2. (λx₁:α₁, ..., x_n:α_n->β.E)《γ₁/T₁, ..., γ_k/T_k》 ⇒ λx₁:(α₁《γ₁/T₁, ..., γ_k/T_k》), ..., x_n:(α_n《γ₁/T₁, ..., γ_k/T_k》)->(β《γ₁/T₁, ..., γ_k/T_k》).(E《γ₁/T₁, ..., γ_k/T_k》)

帰納的な定義にしたがって、どんどん型置換を進めていくと、最後に残るのはコマンド定数（基本コマンド）に対する型置換ですが、それは自明なルールです。

• c《γ₁/T₁, ..., γ_k/T_k》 ⇒ c

CatyScriptでは、これ以外に型ケース構文 case {型1 => 式1, 型2 => 式2} を入れているのでそこにも総称型表現が登場し、型置換の対象となります。しかし、扱い方に大きな変更はありません。

ほんとに大丈夫？

型置換の実行系は、一種の項書き換えシステムとなるので、合流性と停止性がないと困ったことになります。また、通常のラムダ計算（Λではなくてλを使うほう）の計算も項書き換え（アルファ変換、ベータ変換）なので、2つの項書き換え系が整合的に動いてくれるかも問題となります。

完全にフォーマルな定式化と証明はできてませんが、実装は動いているので大丈夫だろうと（楽観的に）思っています。型変数と再帰的型／再帰的コマンドが一緒になると、事情が複雑になり、実は完全には実装できてません。うまくいく範囲に制限している*6のですが、この制限で実用上困ることはないような気がしています。つまり、総称のサポートは「もうこれでいいかな」という気分。

*1:ギリシャ小文字を使うのが型理論の習慣のようなので、それに従いました。

*2:型を渡すと型を返す関数とみなすこともできます。なので、型関数と呼ぶこともあります。

*3:この書き方は、実際のCatyScriptでは構文エラーです。

*4:正確なCatyScript構文ではありませんが、まー、だいたいこんな感じです。

*5:キーワードcommandは、「(1)ラムダ抽象、(2)変数の型付け、(3)式全体の型の宣言、(4)型に関するラムダ抽象」を同時に行うことになります。

*6:再帰構造をサイクリックグラフで表現するのですが、このサイクリックグラフ構築が有限ステップで終わることが容易に判定できるときだけサイクリックグラフを作っています。