タイピングからプロファイリングへ

「型」と「型つけ」の概念が曖昧。型の代わりにプロファイルを導入して、型つけ〈タイピング〉の代わりにプロファイリングを使う。型は対象のことだとして、型付けは、基礎射のプロファイリングの意味に限定して使う。つまり、f:->A in C の形のプロファイリングをタイピングと呼ぶ。

1. 圏のプロファイリング C : D 右辺はドクトリン
2. 対象のプロファイリング A : C 右辺は圏
3. 射のプロファイリング f: A -> B 右辺はホムセット
4. アノテーション付きの、射のプロファイリング f:A->B in C 右辺はホムセット
5. タイピング＝基礎射のプロファイリング a: -> A 右辺は基礎ホムセット
6. コンストラクタのプロファイリング F:C -> D 右辺はコンストラクタセット
7. コンビネータのプロファイリング F -> G, F'->G' => K -> L 右辺はコンビネータセット

最初のプロファイル項（左辺のこと）はドクトリンとなる。したがって、ドクトリンはシステムに組み込む必要がある。ドクトリンの必須条件（＝メタドクトリン）は、基礎付き対称モノイド閉圏(〈grounded symmetric monoidal closed category〉に対して忘却関手を持つような圏のドクトリンの部分ドクトリンであること。基礎となるGSMCC〈grounded symmetric monoidal closed category〉を固定してもいいかも知れない。