haskell-jp / random #28

@Cassin has joined the channel

english 、 code-review 、 kinds チャンネルはアーカイブしてしまってもいいと思ったのですがどうでしょう？情報を集中させ、より多くの人が発言にアクセスできるようにするというのが動機です

kinds に関しては賛成です．他のチャンネルに関しては棄権で

現状、追えないほど random が活発というわけでもないので random に集約させるのは自分は賛成です
新規参入者にとってもチャネルが多いのはどこに入るべきか迷うように思います
random の流速が速すぎるようになったら再分離の検討をすればよいと思います

ようやく理解できたような気がします．
メモを公開してあります．(不備の指摘などいただけると嬉しいです) ありがとうございました．
https://scrapbox.io/ny-sketch-book/%E5%A4%89%E6%95%B0%E3%82%92%E6%9D%9F%E7%B8%9B%E3%81%99%E3%82%8B%E3%81%AE%E3%81%AF%E5%80%A4%E3%81%A7%E3%81%AF%E3%81%AA%E3%81%84%E3%81%AE%E3%81%8B

CI した https://travis-ci.org/kakkun61/pixela-client-haskell

実際，[Lazyな(おもちゃ)言語 https://gist.github.com/nobsun/5b310dd4a397af624690b6ca4b0af2c8]も`interp`は意味関数(semantic function あるいは meaning function)という表示意味論で登場する意味を決める関数なわけで，操作意味論における簡約過程を書いたものではない．計算済みかどうかを意識して区別していない(できないし，必要もない)のはその所為である．

意味論については議論の途中で出てきたURLを踏んだりして勉強している所で、これは私見なのですが。denotativeに評価器を定義したいなら、ステップを陽に見えるように書かない限り、ちゃんとした定義にならないのではないかと思います。

現状だと⊥をdenoteする式に対してinterpを動かすと「プログラムが停止しない」という結果が得られる訳ですが、これはHaskellの持つ操作的意味論によって意味づけられているだけで、数学的にはinterpは部分関数で、⊥に相当する部分がill-definedなのではないかと思います。

Haskellにおいてステップを陽に書くなら、Iterモナドを用いると綺麗になりそう。 http://hackage.haskell.org/package/free-5.1/docs/Control-Monad-Trans-Iter.html#t:Iter

はい，ご指摘のとおりです．Div e1 e2 の意味がHaskellのdivに依存しているからです．

divというか、 let inf = inf + 1 in inf みたいなのの事を想定していました。こういうものの意味論をきちんと定義するために、Wikipediaの記事で言うところのprogressionを使った手法を導入したはずなので、表示的意味論でinterpを定義するなら考慮しないと駄目では、と思った次第 https://ja.wikipedia.org/wiki/%E8%A1%A8%E7%A4%BA%E7%9A%84%E6%84%8F%E5%91%B3%E8%AB%96

⊥を表示する式で停止するのは，Lazyおもちゃ言語では div ？ 0 だけですが．

申し訳ない、「停止しない」でした（訂正済）

そうですねぇ．⊥から始まる近似列を実装しなければなりませんが，たとえば，inf = inf + 1 の場合，infの値はその近似列の極限になるわけで， +1 が値構成子 Succ :: Nat -> Nat で構成されていればなんとかなるかもしれませんが，その場合は，inf ≠ ⊥ですねぇ．実装上は単に停止しないということで表現する以外は思いつかなかったです．

単にsuccでいいのかな．

+ がプリミティブだとむずかしそう．

すいません，あれから少し不動点意味論の勉強をして，言いたかったことやHaskellの仕様が混乱していないという主張の意味がわかりました．

ところで，僕も @as_capabl さんと同じ疑問は持ったのですが，個人的にはHaskellの意味関数を[]，Toy言語の意味関数を[| |]とした時，[|e|] = [interp e]でHaskellの意味領域に接地させることで，意味関数と主張しているのだと思っていました．

primitiveの場合単に [e1 + e2] = { ⊥ if [e1] = ⊥ || [e2] = ⊥; [e1] + [e2] else }で定義すればいいのではないでしょうか？

あ，それで1つ前で言いたかったのは，例えばparallel ifなどを実装する際多分そのままの定義ではできなくて，それは何故できないかというと

⊥に相当する部分がill-defined

が効いてきてるのではないかなと思ったという感じです(あんまり説明になっていないかも)

停止が判定できないので，[e]=⊥が判定できないです．

@ has joined the channel

例えばparallel ifなどを実装する際多分そのままの定義ではできなくて

parallel-orのことでしょうか？多分，⊥のように計算が停止しない値ではなく，値にバインドされていない変数が表示する値(emptyMVarの中身)みたいな計算をブロックするような値を考えないといけないですね．(たぶん)

asyncパッケージにあるControl.Concurrent.Async.raceみたいなもの実装のことですよね．

はい，C[pif L then M else N](env) = { [M](env) if [L](env) = true; [N](env) if [L](env) = false; [N](env) if [L](env) = ⊥ and [M](env) = [N](env); ⊥ else } みたいなやつですね．parallel orでも同じ議論ができますし，そっちの方が単純なのでそっちで考えてもらっても大丈夫です．

停止が判定できないので，[e] = ⊥が判定できないです．

これがよく分からないのですが，別に意味論上は停止するかどうかは判定しなくてよくて，その表示を満たせば良いと思うのですが，何か勘違いしてるでしょうか？実装上は， seq e1 . seq e2 $ e1 + e2 で問題ないはずです(Haskellの場合はそもそもe1 + e2でもいいですね)

「MonadPlusは高階なモノイドである」っていう主張、妥当か否か？
（e.g. MonadPlus Maybe は Nothing mplus Just = Just かつ右についてもそう）

また，自分の言っていることが混乱しているような気がしてきました．すみません．

⊥に相当する部分がill-defined

がよく判っていない気がします(私が)．どうなっていれば，well-definedですか？

ああ．プリミティブの場合はおっしゃるとおりですね．

要は，⊥となるtermへの扱いが明確に定められていなくて，Haskellの式が結果的に計算が停止しないので評価器も停止しないようになっているだけで，por のような⊥の扱いが重要になる場合にそれが問題になりそうというのが言いたいことでした．個人的には，

Haskellの意味関数を[]，Toy言語の意味関数を[| |]とした時，[|e|] = [interp e]でHaskellの意味領域に接地させることで，意味関数と主張している

ということでも問題ないとは思うのですが，denotativeと主張するならHaskellに接地させるのでなくtermに対する定義が明確になっていて，

let inf = inf + 1 in inf みたいなの

に対する定義が明示されているべきだという主張も分かる気がするという感じです(これが明示されていれば，おそらくporの導入もそれほど難しくないのかなという．例えば， @as_capabl さんがいうように評価器がちゃんとステップを陽に見えるよう書かれていれば，porはステップを同時進行させることで実装できるはずです)

プログラムのコードでいうと，ValueにBotが含まれているべきということになりますか？

それもありますが，主に

progressionを使った手法を導入したはずなので、表示的意味論でinterpを定義するなら考慮しないと駄目では

ですね．多分ValueにBotを導入しただけではporは実装できないはずです(片方が停止しなくてももう片方が停止してtrueになれば結果が返せるので)

x por y = if isBot x then y else x は無理ですよね．

はい，その定義は二重にだめで，isBotがおそらく停止するように実装するのが無理なのと，⊥ por falseは通常⊥になるはずっていうのですね(なので，結構実装は難しいはずです)

let inf = inf + 1 in infに対する定義がなされているべき

これがそもそもできそうもない(私の能力的に)

(まあ，本題からかなり外れる気がするのでどうなんですかね？個人的には，

実際，[Lazyな(おもちゃ)言語 https://gist.github.com/nobsun/5b310dd4a397af624690b6ca4b0af2c8]も`interp`は意味関数(semantic function あるいは meaning function)という表示意味論で登場する意味を決める関数なわけで，操作意味論における簡約過程を書いたものではない

という文が気になったというだけなので．後この議論で不動点意味論の気持ちが分かったので，感謝の気持ちしかないです)

よく分からないんですけど、Alt によって任意の MonadPlus は Monoid になるのと関係ありそうな気が
https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Monoid.html#t:Alt

意味が定められない = ⊥ ?

Iterモナドを使えば行ける...と思ったんですけど、意外に難しくてまだ組み途中です

Alternative は (Hask, (), (,)) -> (Hask, Void, Either)の monoidal functorだから、monoidっぽいのは間違いなし

f Void <-> f a — trivial
f a -> f b -> f (Either a b) <-> f a -> f a -> f a — trivial

interpをinterpFの不動点として定義してできたことにする．じゃだめかな？ <- 適当にいってます．

Monoidal functor であるという条件からこの二つの関数が得られて、

() -> f Void
forall a b. (f a, f b) -> f (Either a b)

これが Alternative である条件の二つの関数と対応するということですよね？

forall a. f a
forall a. f a -> f a -> f a

（一瞬、forall a. f Void <-> f a に見えてびっくりした）

ww
そうです、その <-> はisomorphicの記号みたいなものww

https://gist.github.com/as-capabl/9dfb4cff6c08f6b5027741e2fc4bf40b por実装したやつできました

これは，call-by-name だけど，call-by-needじゃないようですが，そこは意図的ですか？

なるほど、そこは意識できてなかったです。おそらく改良すればcall-by-needも実装可能ですが、考える事が増えそうですね

単純にnormalizeがcall-by-need用になっていないだけです．

たまたま正格版のコードを元にして作り始めて、そうすると非正格評価に戻したときlet内でbotが呼び出しエラーになる事が分かって、結果的にほとんどnormalizeしていない形に修正しました。上の非正格版のnormを埋め込めば動くかどうか。

それはそれとして、このスレッドの本題としては「変数に束縛されるのはIter Valueだが、これを『値』とみなして良いのかどうか」かと

そうですね．Iter Value は値ではなく計算なので，「変数に束縛されるのは値ではなく，値を求める計算」ということになります．ただし，解釈器interp の最終結果すなわち，式が表示するものが，Iter Valueであるとするなら，Iter Valueを改めて値と読んでもよいと思います．

ちょっと強引かな．

Lazy版を修正してみました．Porの意味は勝手に替えてしまいましたが，動くようです．
https://gist.github.com/nobsun/5b310dd4a397af624690b6ca4b0af2c8

ありがとうございます！
とても参考になりました

MonadPlusは高階なモノイドである
（任意のMonadPlusはAltを介して任意のaに対してMonoidである）
って感じに主張しようかな:face_with_rolling_eyes:

monoidal functor、また何なのか忘れたのでみてみよw

そういえば， <@U570660KX> さんのだと
```
>>> eval $ Div (Con 1) (Con 0) `Por` Div (Con 1) (Con 1)
*** Exception: divide by zero
```
になるんですね( <@U4KU9ABL0> の修正見るまで気づかなかった)．本来のdenotational semanticsに立ち戻るならIter ValueはあくまでValueの近似であって，Iter Value ~ Valueとみなしても良いのではないでしょうか？まあただdenotationalにも近似を束縛する，計算を束縛するとも言えるかもしれないですね．