指標と型クラス 1

型理論 本編ネタ セオリー論

Twitterでつぶやいていた内容の一部をメモにしておこう。

無名指標と入れ子指標

無名指標または指標リテラルは、sig {...} の形で書く。

sig {
 sort U
 operation e:ε → U
 operation m:(U, U) → U
}

これはモノイド指標（monoidal signature、「モノイドの指標」ではない！）で、宣言の区切り記号をカンマにしてもいいように構文を決めておく。プロファイルの左右は原則括弧で囲み、空リストはεでもよい。(U) は U と書いてもよい。略式記法は、

sig {U, e:ε → U, m:(U, U) → U}

カンマ区切りで1行でも書ける。

入れ子の指標〈nested signature〉の例を出す。

sig {
 sig 1 {
   sort U
 }
 operation e:ε → U
 operation m:(U, U) → U
}

sig {
 sig 1 {
   sort U
   operation e:ε → U
 }
 operation m:(U, U) → U
}

sig {
 sig 1 {
   sig 2 {
     sort U
   }
   operation e:ε → U
 }
 operation m:(U, U) → U
}

規則と注意は：

  1. 部分指標には、1始まりの番号を付ける。欠番はダメ。
  2. 一番外の全体は番号0とする。番号0は書いても書かなくてもよい。
  3. 当面、部分指標の重なりは許さないが、そのうち重なりも考える。
  4. Σが番号で識別された部分指標を持つ指標のとき、Σi で番号が i である部分指標を意味する。
  5. 等式〈equation〉も書けるが、簡単な例では使わない。

無名指標への名前付けは次の形：

PtMagma := sig {
 sort U
 operation e:ε → U
 operation m:(U, U) → U
}

同じことを次にようにも書く。

signature PtMagma {
 sort U
 operation e:ε → U
 operation m:(U, U) → U
}

入れ子の指標にも名前付けができる。

signature PtMagma {
 sig 1 {
   sort U
 }
 operation e:ε → U
 operation m:(U, U) → U
}

まったく同じだが、気分だけの問題で、部分指標を param で指定する。

signature PtMagma {
 param 1 {
    sort U
 }
 operation e:ε → U
 operation m:(U, U) → U
}

部分指標を指定された指標をパラメータ付き指標〈parameterized signature〉とも呼ぶ。

パラメータ付き指標には極端な例もある。

signature PtMagma0 {
 param 1 {}
 sort U
 operation e:ε → U
 operation m:(U, U) → U
}

signature PtMagma1 {
 param 1 {
  sort U
  operation e:ε → U
  operation m:(U, U) → U
 }
}

次は同じ概念。

  1. パラメータ付き指標
  2. 相対指標〈relative signature〉
  3. 部分指標をただ1つだけ持つ入れ子指標

語「パラメータ」が意味的にふさわしくないときがある。そのときは「相対指標」を使う。例えば、レコードの余域となる相対指標をパラメータ付き指標と呼ぶのは奇妙。

指標Σと、その部分指標 Γ⊆Σ で定義される相対指標を Γ.Σ とも書く。空指標を 0 と書くと、0.Σ や Σ.Σ もある。

相対指標 Γ.Σ は、指標の圏の包含射 Γ→Σ in Sig と同一視できるので、アンビエント圏（モデルのターゲット圏の圏）内の射 Mdl(Σ, C) → Mdl(Γ, C) in AMB を定義する。これは忘却射影関手〈forgetful projection functor〉。ここで、Cは任意のターゲット圏（アンビエント圏の対象）。忘却射影関手は次のように略称する。

  • {忘却}?射影{関手}?

レコードとそのプロファイル

レコードは構文的対象物だが、意味的には関手になる。レコードのプロファイルは、2つの相対指標を矢印で区切った形。構文的に r:Γ.Σ ← Φ.Δ だと、意味的には次のようになる。

$`\newcommand{\cat}[1]{ \mathcal{#1}}
\xymatrix {
{Mdl(\Sigma, \cat{C})} \ar[d]^{Proj}
&{}
\\
{Mdl(\Gamma, \cat{C})}
& {Mdl(\Delta, \cat{C})} \ar[l]_{F} \ar[d]^{Proj}
\\
{}
& {Mdl(\Phi, \cat{C})}
}\\
\mbox{in }{AMB}
`$

Fがレコードrで定義される関手。レコードが、パラメータを持たない完全定義レコードなら：

$`
\xymatrix {
{Mdl(\Sigma, \cat{C})} \ar[d]^{=}
&{}
\\
{Mdl(\Sigma, \cat{C})}
& {Mdl(\Delta, \cat{C})} \ar[l]_{F} \ar[d]^{!}
\\
{}
& {Mdl(0, \cat{C}) = {\bf I}}
}\\
\mbox{in }{AMB}
`$

さらに域側指標が空指標なら、

$`
\xymatrix {
{Mdl(\Sigma, \cat{C})} \ar[d]^{=}
&{}
\\
{Mdl(\Sigma, \cat{C})}
& {Mdl(0, \cat{C}) = {\bf I}} \ar[l]_{F} \ar[d]^{=}
\\
{}
& {Mdl(0, \cat{C}) = {\bf I}}
}\\
\mbox{in }{AMB}
`$

これは事実上、単一のインスタンス。

$`
\xymatrix {
{Mdl(\Sigma, \cat{C})}
& {\bf I} \ar[l]_-{F}
}\\
\mbox{in }{AMB}
`$

相対指標を射影関手と解釈する事と、それに伴うレコードの解釈はけっこうミソかも知れない。レコードという言葉はCoqやAgdaに合わせた。特にAgdaだと、この意味論が直接的に使えそう。いや、そうでもないか。

後で書く予定：

レコードのメンバー関数コードの定式化には、構文モナドとクライスリ射、システムのコア指標が必要。コア指標のモデル（エンジンと呼ぶことにする）があれば、クライスリ射はモデルを定義する。

射影関手のセクションと、セクションの一般化であるアドホック・セクション。アドホック・セクションが型クラスのインスタンス（の集まり）に相当する。アドホック・セクションとの対比で、通常のセクションをパラメトリック・セクションと呼ぶ。パラメトリック・セクションは、アドホック・セクションの極めて特殊なもの。

多相型と多相関数は、関手と自然変換で解釈して、関手圏の対象と射と考える。すると、多相型と多相関数で作られる多相モデルは関手圏をターゲット圏とするモデル。アドホック・セクションは、多相モデルを決定する。したがって、アドホックセクションの全体は多相モデルのなかに埋め込める。特に、パラメトリック・セクションの像となっている多相モデルはパラメトリック多相モデルで、パラメトリック多相モデルのメンバー関数はパラメトリック多相関数。ここで、メンバー関数は、指標の演算記号に割り当てられる射のこと。