構文的モナドと手続き

モナド (T, μ, η, s)/C が構文的だとは:

  1. 基礎圏 C は挿入的余デカルト・モノイド圏
  2. モナドは強度 s とその余強度〈右強度〉に対して可換モナド
  3. モナド単位は、Cの挿入。

挿入的モノイド圏〈insertive monoidal category〉とは:

  1. 挿入〈insertion〉の圏と呼ばれる広大部分モノイド圏がある。
  2. 挿入はすべてモノ射である。
  3. モノイド圏の構造射〈法則射 | 一貫性射〉は挿入である。

デカルト圏のときは:

  1. 始対象=モノイド単位からの射は挿入である。
  2. 直和の入射は挿入である。

構文的モナドのクライスリ圏の反対圏の射を手続きと呼ぶ。手続きに関して次の演算ができる。

クライスリ圏の対称モノイド性定理により、構文的モノイドのクライスリ圏は対称モノイド圏。もし、余デカルト構造が持ち上がれば、手続きの圏はデカルト圏になる。

手続きは、色々なものを包摂する。

sign/proc定式化 ML オブジェクト指向言語
指標 シグネチャ インターフェイス
手続き ファンクター アダプター
リテラル手続き ストラクチャ クラス
部分手続き (特に名前無し) 抽象クラス

MLのストラクチャはモジュールだから、モジュールシステムも包摂される。