指標＝インターフェイスの理論
[追記]いいこと気付いたと思ったが、ずっと昔に同じこと書いてたわ。アジャー。「だんだん思い出した：指標＝インターフェイスの理論 - 檜山正幸のキマイラ飼育記 メモ編」参照。[/追記]
パラメータ付きのインターフェイスが難しいのは、それがプリミティブではなくて、構成物だからだ。「パラメータ付きインターフェイスは、指標か？」という問われれば、指標＝インターフェイス＝対象ではない。パラメータ付きインターフェイスは、実は射なのである。
通常の指標の圏をSigとする。圏SigをモナドLで拡張したクライスリ圏を Kl(Sig, L) =: SubstL と書く（Substは代入から）。したがって、
- Kl(Sig, L)(Σ, Γ) = SubstL(Σ, Γ) = Sig(Σ, L(Γ))
となる。Σ'⊆Σ のときは、JΣ'⊆Σ∈SubstL(Σ', Σ) とみなす。
パラメトライズの定式化には、有極指標〈polarized signature〉を使う必要がある。有極指標とそのあいだの射の圏をAdaptとする。対象は有極指標で、射はSubstの射から作る。この部分は、Int構成／GoI構成を使う。
Adaptには、双対スター作用素（対合作用素）が入り、直和に関してコンパクト閉圏になる。コンパクト構造とスター構造は整合する。コンパクト閉圏はモノイド閉圏なので、モノイド閉圏のラムダ計算ができる。そのラムダ計算によって、パラメトライズは定式化される。
事態が複雑なのは、SubstとAdaptの2つの圏があり、相互に関係しているから。それと、次を満たす非対称テンソル積▷があると思う（まだよく分からんのだが）。
- Model(Σ, Model(Γ, C))
Model(Γ▷Σ, C)
この積を融合積（fusion product）と呼んでおくと、融合積をモノイド積に持つモノイド圏の構成がキモになるような気がする。融合積の構成は、普通にやっていたは出来そうにない。なんかトリックが必要だろう。
Model(Γ, C) をMΓ(C)と書くと：
- Model(Σ, MΓ(C))
なので、Γ▷(-) という二項演算ではなくて、FΓ(-) であって、FΓ -| MΓ である関手 FΓ:Sig→Sig が決まればいい。FΓは普通のテンソル積ではないのかも知れない。
