強モナド (T, μ, η, s)/C が構文的だとは:
挿入的モノイド圏〈insertive monoidal category〉とは:
- 挿入〈insertion〉の圏と呼ばれる広大部分モノイド圏がある。
- 挿入はすべてモノ射である。
- モノイド圏の構造射〈法則射 | 一貫性射〉は挿入である。
余デカルト圏のときは:
- 始対象=モノイド単位からの射は挿入である。
- 直和の入射は挿入である。
構文的モナドのクライスリ圏の反対圏の射を手続きと呼ぶ。手続きに関して次の演算ができる。
クライスリ圏の対称モノイド性定理により、構文的モノイドのクライスリ圏は対称モノイド圏。もし、余デカルト構造が持ち上がれば、手続きの圏はデカルト圏になる。
手続きは、色々なものを包摂する。
sign/proc定式化 | ML | オブジェクト指向言語 |
---|---|---|
指標 | シグネチャー | インターフェイス |
手続き | ファンクター | アダプター |
リテラル手続き | ストラクチャ | クラス |
部分手続き | (特に名前無し) | 抽象クラス |
MLのストラクチャはモジュールだから、モジュールシステムも包摂される。