モノイドの圏Monの直和に注目すべき

計算の副作用（主作用かも）の定式化はモノイドの圏となるが、モノイドの圏のなかの直和が重要だと気が付いた。つうか、前から細々とは使っていたが、これは大々的に使わないといかん、と思った。

例外（exception）があると、あるストレージ（加群の台）に作用するモノイドは、M + 1 の形になる。Mは正常処理から、1 は例外からやってくる。モノイドの圏の直和は、群と同様に自由積で与えられる。集合直和としての M + 1 はいったん自由積 M*1 に埋め込まれる。ところが、M*1 は M と同型なので、例外に起因する 1 の作用は消えることになる。

例外とは限らない、直和（場合分け）があると、それぞれの直和成分（ケース、選択肢、choice）ごとに作用モノイドが出てくる。これらの作用モノイドの直和＝自由積がストレージに作用する。

ん、モノイドの圏も半環圏になるのか？ と思ったがまったくダメだ。それに、モノイドの圏の直積と割とショーモナイ感じがする -- ほんとに実行が分離しているプログラムのモデルにしかならない。