イイカゲンな型推論を求めて

「イイカゲンな型システムを求めて」：

僕のようなずぼらでだらしない性格の人に向いていて、それにもかかわらずある種の適切さ、バランスの良さを備えていて、さらに破綻しない程度には首尾一貫している型システムはないものかと探したり考えたりしてきました。

ずぼらでも破綻しないためには、どこかシッカリした面もないとね。

というわけけで、イイカゲン型システムの型推論を考えてみました。古典論理のシーケント計算をまねて作ったので自動的検証のアルゴリズムとかには向きません。とりあえず、人間が（って、僕だけど）紙と鉛筆で使う用途つうことで。とはいえ、人間用のシーケント計算としても、いまひとつシックリこない点が残っています。まーなんだ、現時点でもスナップショットということで書いておきますわ。後でゴッソリ修正するはめになるかも。

内容：

1. モデル
2. シーケントの構文
3. 推論規則：公理
4. 推論規則：ガードとマーク
5. 推論規則：構造規則
6. 推論規則：論理規則
7. それで

モデル

モデルとしては、「集合と部分写像の圏」の部分圏を使います。基本データ型{integer, number, string, boolean, null, any, never}に対応する領域を含んでいて、直積と直和で閉じた圏です。anyの意味は、すべてのデータ領域を埋め込めるような領域、neverの意味は空集合です。こういう圏を1つ確定しても、それだけでモデルが作れるわけでもないので、今これ以上正確な定義はしません*1。

キーと呼ばれる記号の集合を固定します。キーの役割は2つあって、直積成分のラベルとなること、直和成分の弁別子となることです。aがキー、Tが型（意味はデータ領域）であるとき、実は a:T の意味は曖昧で、aというラベルで特定される成分を持つ直積型なのか、aという弁別子で特定される成分を持つ直和型なのかハッキリしません。でも、この曖昧さがイイカゲンさに寄与する気がするので、ホントに具合が悪いことが起きないかぎり目くじら立てずほっておきます。

キーの列 a₁, ..., a_n に対する直積型は Π(a_i:T_i)、直和型は Σ(a_i:T_i) と書くことにします。これは、キーで修飾しているので、純粋な圏論的直積／直和ではありません。

a_kを、a₁, ..., a_n のうちどれか1つのキーだとして、π_{a_k}:Π(a_i:T_i)→T_k は射影です。一方で、jが{1, 2, ..., n}の部分集合を走る添字だとすると、Π(a_i:T_i) から Π(a_j:T_j) への射影もあります。このタイプの射影を選択射影（選択子）と呼ぶことにします。特に、Π(a_i:T_i)→a_k:T_k という選択射影がありますが、これは π_{a_k} とは区別されます。

直和に関しても同様に、入射 ι_{a_k}:T_k→Σ(a_i:T_i) と、選択入射（余選択子） Σ(a_j:T_j) →Σ(a_i:T_i) を考えます。

シーケントの構文

a, bなどはキー、S, Tなどは型（を表す変数）です。a:T はキー付きの型ですが、このままでは解釈が曖昧です。そこで、a:T の解釈はシーケントの左右で変えることにします。キー付き型の列、a₁:T₁, ..., a_n:T がシーケントの左に出てきたら直積、右に出てきたら直和にします。

シーケントの左右を区切る記号は「⇒」、論理記号としては「∧」と「∨」を使います。その他の論理記号はありません。「∧」と「∨」は、2項演算子ではありません。丸括弧と一緒に使って、n = 0, 1, 2, 3, ... に関してn項演算子を定義するとします。例えば、(∧), (∧a:T), (a:S∧b:T), (a:S∧b:T∧c:U) など。(∧)には単元集合を割り当てればいいので、null型と解釈していいかもしれません。(∨)の意味はneverです。

ここでは、普通のシーケントは違って、f :: α ⇒ β のようにラベルfを付けます。このfは関数として解釈されます。αとβは型をカンマで区切って並べた列です。fの解釈は、おおよそ Π(α) から Σ(β) への部分関数です。

解釈や推論がうまくいくためには、構文的な制約が必要ですが、細々してめんどくさいので全て割愛。

推論規則：公理

■公理
     (なし)

  -------------

   f :: S ⇒ T

型の間の包含関係、例えば integer ⊆ number などは公理の形で入れておきます。包含写像をiで表すなら、i :: integer ⇒ number というシーケントが公理です。この場合、ラベルiを省略してもかまいませんが、それはあくまで略式の書き方で、本来すべてのシーケントにラベルが付いているとします。

推論規則：ガードとマーク

■ガード
   f :: S ⇒ γ

  ------------------

  f@a :: a:S ⇒ γ 
■アンガード
   f :: a:S ⇒ γ 

  -----------------

  f@^a :: S ⇒ γ
■マーク
   f :: α ⇒ T

  -----------------

  b:f :: α ⇒ b:T
■アンマーク
   f :: α ⇒ b:T

  ----------------

  b^:f :: α ⇒ T

解釈は次のようになります。

• ガード： 射影のプレ結合
• アンガード： 射影に対するセクションのプレ結合
• マーク： 入射のポスト結合
• アンマーク： 入射に対するレトラクトのポスト結合

推論規則：構造規則

■増-左
  f :: α ⇒ γ

  ---------------

  f :: a:S, α ⇒ γ
■増-右
  f :: α ⇒ γ

  ---------------

  f :: α ⇒ γ, b:S
■換-右
  f :: α, a:S, b:T, β ⇒ γ

  ---------------------------

  f :: α, b:T, a:S, β ⇒ γ
■換-左
  f :: α ⇒ γ, a:S, b:T, δ

  ----------------------------

  f :: α ⇒ γ, b:T, a:S, δ
■カット
  f :: α ⇒ T   g :: T ⇒ γ

 ---------------------------

  f;g :: α ⇒ γ

増-左が、選択射影のプレ結合、増-右が、選択入射のポスト結合です。換は特に言うことはありません。カットは射の結合ですが、一見当たり前そうで実は問題を含んでいます。カット規則は修正が必要かもしれません。

推論規則：論理規則

■∧-左2
  f :: a:S, b:T, α⇒γ

 -----------------------

 f' :: (a:S∧b:T), α⇒γ
■∧-右1
    f :: α ⇒ a:S

  ----------------------

  {a:f} :: α ⇒ (∧a:S)
■∧-右2
  f :: α ⇒ a:S   g:: α ⇒ b:T

  -------------------------------

  {a:f, b:g} :: α ⇒ (a:S∧b:T)
■∨-左1
  f :: a:S ⇒ γ   g :: b:T ⇒ γ

 --------------------------------

  [f@a] :: (∨a:S) ⇒ γ
■∨-左2
  f :: a:S ⇒ γ   g :: b:T ⇒ γ

 --------------------------------

   [f@a, g@b] :: (a:S∨b:T) ⇒ γ
■∨-右2
   f :: α⇒γ, a:S, b:T, δ

 -----------------------------

  f' :: α⇒γ, (a:S∨b:T), δ

規則の一部だけを挙げています。1とか2と番号が付いている規則は n = 0, 1, 2, 3, ... に対して番号nの規則があります。∧-右 と ∨-左 が一番大事な規則でしょう。fとf'の関係とかは適当に想像してください。

それで

ものすごく大雑把な話でしたが、ある程度は推論できそう。キー付き型の解釈の曖昧性（よく言えば多義性）、カット規則の変な感じとかがあるので、もう少し考えてみます。

*1:圏をモデルにするんじゃなくて、適当な圏のなかで再帰的領域を作って、それをモデルにするほうがいいのかも知れません。ハッキリとはわからんけど。