指標の圏

具体的な指標＝コンピュータッドの圏は面白い。単純そうだが実際は色々と複雑で、ジャングルを探検する気分。

指標の射は基本射〈basic morphism〉と拡張射〈extended morphism〉に分けて考えたほうがいいようだ。基本射は、コンピュータッドとしての射。拡張射は項モナド（構文モナド）のクライスリ射。

で、射の方向が実に紛らわしい。どっちを順方向にするかを決めておいたほうがいいな。基準となるのは、部分指標の包含射 Δ⊆Γ をΔ→Γとみるか、Γ→Δとみるかだろう。仮に、Δ→Γを順方向とみると、包含に対応する制限子はΓ→Δだから反対になる。制限子は特殊な変換子〈トランスフォーマー〉とみなせるから、変換子も逆方向の射となる。

変換子はリダクト関手と同じ方向になるから、これはやはり指標射の反対射とみるのがよさそうだ。つまり、順方向の指標射は変換子の反対射。

改名子は同型射（可逆射）だから、方向はどうでもいいが、変換子の方向と揃えておいたほうがいいだろう。

 rename{ top to peek} signature {type S, V; top : S -> V; push : S*V -> S; pop : S -> S|eror}
=
 signature {type S, V; peek : S -> V; push : S*V -> S; pop : S -> S|eror}

次と同じ、

transformer (instance St of Stack) to (instance of ?)
{
  S := St.S;
  V := St.V;
  ppk := St.top
  push := St.push;
  pop := St.push;
}

方向は、リネーム前の指標 → リネーム後の指標、旧名 =: 新名 または、新名 := 旧名。

インスタンスは特殊な変換子になる。

instance of ToggleSwitch {
  S := bool;
  isOn := (s:S):bool => s == true;
  isOff := (s:S):bool => s == false;
  toggle := (s:S): S => s? false : true;
}

transformer (instance _ of Empty) to (instance of ToggleSwitch)
{
  S := bool;
  isOn := (s:S):bool => s == true;
  isOff := (s:S):bool => s == false;
  toggle := (s:S): S => s? false : true;
}

次に部分インスタンス：

partial instance of Counter {
  C := int;
}

transformer (instance X of singnature {init: -> int; up : int -> int})
          to  (instance of Counter)
{
 C := int;
 init := X.init;
 up := X.up;
}

インスタンス化（具体性が増す）の方向と変換子の方向は逆。

あとはパラメータ化。パラメータ化は指標に対する操作で、おそらく指数対象を作ることになる。もし、指数対象がパラメータ化指標なら、射＝変換子の逆に対して、射の指数は Sig×Sig^op→Sig という反変共変の二項関手になるので、取り扱い注意。

指標をワイヤー、変換子をノードにした絵を描くといいと思う。