2023 03 18 - qnighy/umo GitHub Wiki

近況

昨日は特に進捗はない。

副作用・作用について

関数が外界とどのようにやり取りするかは関数のインターフェースで厳格に表現されるのが望ましい。少なくともUmoではそうしていきたい。

このような作用の表現方法として最初に挙げられるのはMonadのように戻り値側に作用を書く方法である。たとえば a -> State s b や a -> Either e b によって状態や大域脱出をとらえることができる。

一方で、引数側に作用を書くアプローチもある。

• Reader Monadの左随伴を取るとReader Comonadが得られる。たとえば、Go言語の ctx context.Context はReader Comonad的な書き方にも読める。
• RustではState effectを戻り値として宣言するのではなく、個別のメモリ領域に対する変更許可を &mut T 引数として得るようになっている。
• 依存関係逆転を行うと外部依存へのハンドルを戻り値として受け取る形になる。これはある種、外部環境へのアクセスをinjected dependency経由に限定するという規約であるとも読め、引数による権限管理が行われるとみることもできる。

Rustの例をもう少し考えてみる。Rustの &mut T は分離論理におけるフルパーミッションを表しているものだとみなせる。その分離論理の典型的なセマンティックスといえば、メモリ全体を1つのStateとみなしてしまうのがわかりやすい。そう考えると、Rustでは全ての関数がMemory stateに対する書き込み副作用を許可されているが、かといって任意の書き込み処理が許されているのではなく、参照に基づくパーミッションで制限されているとも考えることができる。 (こういう副作用の局所性みたいなのってindexed monadかgraded monadで扱えるんだろうか？) これにより、参照を受け取らない関数は (static変数やFFIなどの抜け道を使わない限りは) pureであるという推論が成り立つことになる。

とにかく、引数側に書く作用と戻り値側に書く作用にはそれぞれの利点があると考えられる。

• そもそも局所的に管理しようがないもの (大域脱出など) は戻り値側で宣言するしかない。
• 一方、局所的に管理できるものは引数側の作用で書いたほうがより詳細な制御を行いやすい。

そのため、この2つをうまく統合して両立するのが、関数の作用を制御するもっともよい方法なのではないか…… というところまでを考えている。