実行と状態遷移

Aが引数値の空間、Bが戻り値の空間、Sが状態空間とすると、「副作用＝状態遷移」を伴う実行は、A×S→S×B という射で記述される。この実行が例外の可能性があり、例外値の空間をEとする。

このとき、実行は A×S→S×B + E かというと、そうではない。例外が起きても状態は消えてなくなるわけではないので、A×S→S×B + S×E だ。S×E は、例外発生後の状態と起きた例外（を表現する値）の組だ。

× と + が分配的ならば、A×S→S×B + S×E は A×S→S×(B + E) と書き直せる。B' = B + E と置けば、A×S→S×B' となり、戻り値の空間を直和スタンピングで拡張するに過ぎない。

ということは、例外があってもなくても事情が変わらないことになる。極論すれば、状態遷移の定式化は例外を考慮する必要がないし、もし必要でも値の空間を細工するだけで、状態空間は何も変わらない。

これは、かなり思考の節約になりそうだ。