線形型DSL on Haskell (前回参照) の基本的アイデアと難しい点

前回は、線形型をもつ DSL の例として線形λ計算を挙げ、実装を示した。これをもっと押し進めれば、ファイルやネットワーク接続などのリソースの「使い方」をより詳しく指定できる DSL をエンコードできるはずだ (きれいに書けるか、使う人が居るかは別問題;p)。
実装の簡単な説明はコメントにもあるけど、今回はより詳しい説明を試みたい。

前回の記事では、線形型を Haskell でシミュレートするために、

newtype LLC ii jj a = LLC (ii -> (jj, a))

という型を作った(上の定義は IO や t を省いてある)。
ii -> (jj, a) という型を見てもらえばわかるように、これは Stateモナドの一種になっている。

線形性と「スロット」

型 ii, jj は、線形性をもつ変数の「スロット」になっており、各スロットの使用回数を制限することで、「ただ一度だけ使われる」という線形性を実現している。
たとえば Stateモナド実行前に

(F Int, (F String, ()))

の型を持っていた状態で、ひとつめのスロットを使うと、

(U, (F String, ())

という型に「変化」し、それ以上そのスロットを使うことはできない。このような計算は

(F Int, (F String, ())) -> ((U, (F String, ()), a)

という Stateモナドの型になる。
(前回のエントリの記法を使うと逆順になり

(Nil :> F String :> F Int) -> (Nil :> F String :> U, a)

となるけれど、それはどっちでもいい)

変数とλ抽象のエンコード

この「変化」は var の型にエンコードされている。変数のエンコーディングは (var x) となっており、ここで x には、スロットのある特定の位置を指す (型レベル) 自然数が来ることになっている。

var :: (Update ii n U jj, Pickup ii n (F a)) => n -> LLC ii jj a

だいたいこういう型を持っていたと思う。名前からわかるとおり、 Update ii n U jj はスロット ii の n番目の要素を U に置き換えたものを jj とする、という意味だ。
これにより、「変数を一度使ったらスロットの内容が F a から U に置き換わり、二度とその変数を使えない」という制約を実現している。

一方、λ抽象はこんな型になっていた

lam :: Length ii n => (n -> LLC (F a,ii) (U, jj) b) -> LLC ii jj (a -> b)

ここでのポイントは Length ii n (前回のエントリでは List ii n) だ。これはスロット ii の長さが n であることを示している。そして λ抽象の中では (F a,ii) などとスロットの長さが1増えている。つまり、n はλ抽象によって導入された新しいスロットの番号を指している。
ここでスロットの番号は後ろから数えていることに注意してほしい。新しいスロットを前から数えると常にゼロ番目になってしまい、スロットを指すインデックスの役目を果たさないのだ。
（実はこの「より内側のλ抽象で導入した変数により大きな番号を付番する方法」が de Bruijn level であり、その逆が de Bruijn index になっている。）

残る関数適用は簡単で、関数部分で消費されるスロットと引数部分で消費されるスロットを分離しているだけだ。前回の実装ではたまたま関数部分で使った残りを引数部分で使い切る、というような型になっているが、順番は重要でなく、単に分離することを目的としている。

型推論

理屈では上の通りだが、これをうまく型推論させるにはコツがいる。なぜか？例えば

lam (\x -> var x)

のような項を考えてみるとよい。このλ式は「他のコードの一部分」であるかもしれず、x の de Bruijn ~~index~~level が静的には完全に決まらない。
たとえば上の式では x の de Bruijn level は 0 だが、 lam (\y -> lam (\x -> app (var x) (var y))) では外側にもうひとつλがあるため 1 となる。
このようにgroundな(型変数を含まない)型にはできない x の型は S n のような型になる。
この結果、普通に型推論させると var x の型の Update と Pickup の計算が途中で止まってしまう。

この結果どうなるかというと、型エラーが、全体の型が決まるまで見過ごされてしまうといったことが起こる。

これを防ぐため、 Update と Pickup の定義を、「後ろから数える」ようにして、さらに引き算の定義にうまくパターンマッチを使うことで、「長さnのリストの、後ろから数えて(n+1)番目の要素は、最初の要素である」などと推論させて、うまく型推論を進めている。
具体的には、 n-n=0, (n+1)-n=1, (n+2)-n=2 などと引き算の性質をうまく使って、変数を含む式(型)から変数を除去している。

Coq等で実現するには？

上記のように、型推論でパターンマッチの仕組みを利用しているので、Coqでストレートに実装するのはむずかしい。
何かもっと単純な仕組み - たとえば元のの実装のように de Bruijn index を使うとか - にしないとだめだ。