Skip to content

Instantly share code, notes, and snippets.

@kory33
Created February 3, 2026 21:45
Show Gist options
  • Select an option

  • Save kory33/2fc6cac3546baa397d95102f3d2a01e5 to your computer and use it in GitHub Desktop.

Select an option

Save kory33/2fc6cac3546baa397d95102f3d2a01e5 to your computer and use it in GitHub Desktop.
20260204 rizkubo さんへの返信

https://x.com/rizkubo/status/2013122492244611503

↑ のポストへの返信を、読みやすいようにマークアップしたものです。

本文

こちらも妥当な質問だと思います。まず主張をもう少し明確にさせてください。

まず、「for/doは[...]脱糖してるだけ」はその通りです。しかし、「プログラムの実行をある程度許して」というのは、for/doプログラムの実行をする、と言いたかったのではなく、「自由でない >>= 演算が、一般に、なんらかの意味で部分的にプログラムを実行しており」「そういう、プログラムを部分的に実行するような >>= 演算についても合成を書きやすくするのが for/do という構文だ」「だから、for/do はそういう意味で .replaceExits の一般化になっている」という立場があり得るというのが僕の主張でした。

さて、この中で、「プログラムを部分的に実行する」とはどういうことなのか、というところが最も意味不明であると思われます。言いたいこととしては、「自由でない」というのと「部分的な実行をしている」というのが同じであると主張しているつもりなのですが、これがいったいどうして同じだと言えるのかというところこそ明らかでないと思うので、この点の正当化を試みてみます。かなり長くなります。

「自由」というのは、テクニカルには「(何らかの、その文脈の中で固定された)忘却関手の左随伴の像と同型(Wikipedia (en) - Free Object) 」という特徴づけがあるのですが、「自由モナド」の文脈においては、m: Monad[M] が自由であるというのは、m が何らかの命令型 I[_] についての Monad[Executable[I, _]] と同型である(つまり、変換 c: [A] => M[A] => Executable[I, A] があって、各 A について c[A] が同型で、c[A](m.pure[A](a)) = Exit(a) といった等式を満たす )ことだと考えられます。つまり informal には、まさに Executable のように、「演算が形式的な合成になっている」ようなものであると考えてよいです(この点については、まず記事の 2.5.4 節を読んでいただくことをおすすめします)。

「自由でない」モナドの例として、e ≇ () のときの Reader e があります(実際、Reader[A, _] が仮に Executable[I, _] と同型だと仮定すると e → X ≅ X + Coyoneda[I, A → X] という同型が得られますが、一般に e → X ≅ X + G(X) という X についての自然同型があれば G(()) ≅ Void であることから G = Const Void が示せて、つまり e → X ≅ X + Void ≅ X ≅ () → X が言えて、すると米田の補題の系(e.g. E. Riehl - Category Theory in Context 2.3.1)により e ≅ () です)。ここで僕が主張していることは、例えば、「Reader Bool の標準的なモナドインスタンスの >>= は(ある意味で)プログラムを部分的に実行する」です。

いま、enum AskBool[A] { case Ask[E]() extends AskBool[Bool] } という命令セットを考えます。すると、Executable[AskBool, _] のモナドは、機能的には Reader[Bool] と極めて似通ったものになります。実際、 ask : Reader Bool Bool = idReaderdo/for の中で書くのと、 AskInstr.Ask().asSingleInstrExeExecutabledo/for の中で書くのとでは、書き心地は(戻り値型が同じなので)全く変わらないことでしょう。

でも、Executable[AskBool, _]Reader[Bool] は、(先ほどの一般論からもわかりますが、もっと直感的に)同型ではありません。まず、Reader[Bool, A]Bool → A であり、(記事の 2.3.4 節の議論から)(A, A) と同型であることがわかります。一方、Executable[AskBool, A] は、「プログラムの中でいつでも Ask() することができるが、終了時には A を返すようなプログラム」になっており、この型の値は Reader[Bool, A] に比べて圧倒的に多様で、豊かな構造を持っています。例えば、「true が最初に AskBool.Ask() から返ってくるまでに何度 false が返ってきたか」というプログラムを、

def countFalses: Executable[AskBool, Int] =
  Ask().asSingleInstrExe.replaceExits { b =>
    if (b) Exit(0) else countFalses.map(_ + 1)
  }

と書けます。

何がこの多様性をもたらしているか?というと、「ask はいつ ask しても同じ値が環境から降ってくるものだが、AskBool.Ask() にはそのような保証は一切ない」という点だと思われます。countFalses と同じ実装を Reader モナドで書いて countFalsesR : Bool → Int とすれば、countFalsesR true0 ですし countFalsesR false は無限再帰して帰ってきません。しかし、countFalses の方は、Ask() 命令が書かれたただの構文木です。このプログラムは、「Ask 命令がどのような順番で Bool 値を返していくのか」というデータ(Bool の無限リストや、本当に「外部世界」に Bool 値を取りに行く IO[Bool])を用意して初めて実行することができます。そう考えれば、countFalsesR は、countFalsesrepeat truerepeat false を与えたときの挙動しか記述できていないということがはっきりすると思います。

逆に言えば(そして、この「逆に言う」ことこそが僕の主張の根幹となっているわけなのですが)、Reader[Bool] のことを、Executable[AskBool, _] を「ask で返ってくる結果というのがプログラム全体を通じて必ず同じである」という追加の制約に基づいて(ゲスト言語のプログラムの実行に対して)ahead-of-time に最適化したプログラムであると思うことができます。これは、Bool → A 自体が(何らかの Haskell や Scala の関数ボディがそこにあるはずだという意味で)プログラムであるといった話をしているわけではなくて、Executable[AskBool, A] に対してこのような最適化処理を 仮に 掛けたら、そこには Bool → A 程度の情報しか残らなくなっている はずだ 、ということを言っています。

そのような最適化というのは事前計算に他ならず、この事前計算こそが「自由性」を壊しているものであり、かつ、「部分的な実行」と最初に言っていたものだ、というのが元々の主張の裏側にあるアイデアでした。…どうでしょう、大変長くなってはしまいましたが、伝わりますでしょうか!この気持ちを持ったうえで 2.5.4 と 2.5.5(最後のコラム部分を含む)を読むとさらに気持ちがわかるかもしれません。

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment