Kleisli construction and its properties

読者の中には、数学の内容がpdfで投稿される事に気づいた人がいるかも知れません。

正にメンテナンス性の為に今ではこうしているのですが^[1]WordPressで数式を取り扱う時に私は QuickLatex … Continue reading、ドキュメントを修正・追記したり記事を移植・配布する場合にも有用と気づきました。

さて今回は、Kleisli圏 (構成) という面白い圏とその性質について、敢えて計算込みで詳細に紹介します。

コンピュータ科学者であるE. Moggiは「”コンピュータ・プログラム” の形式的モデリング」の為にこの構成を参照し、非決定論的処理、例外、ポリモーフィズムを含む「副作用」を定式化することに成功しました^[2]Eugenio Moggi, Notions of computation and monads。これらは数学的な関数では説明できない “プログラム関数” の振る舞いに含まれるものです。

しかもKleisli圏は対応する然るべき2-圏の対象として普遍性を持ち、この普遍性によって、(形式化された) プログラムの実行結果 (随伴Fによる作用) は副作用 (Monad Tによる作用) と分離されます。