「Gordon Plotkin先生に学ぶAlgebraic Effect」のまとめ

lotz @lotz84_

Extensible Denotational Language Specification 25年前の仙台で初めて発表された #effect_study

κeen @blackenedgold

昔聞いた時全然わからなかったけどいまならなんとなく分かる #effect_study

Je mange, donc je suis @ryotakameoka

クライアント=サーバ・モデルって感じかな #effect_study

κeen @blackenedgold

幕府じゃなくなってる #effect_study

lotz @lotz84_

Milner先生のインタビューこれか・・・？ users.sussex.ac.uk/~mfb21/intervi… #effect_study

κeen @blackenedgold

†(ダガー) #effect_study

lotz @lotz84_

exp を作って eval で評価して observe で…何するんだ？ #effect_study

κeen @blackenedgold

expがナイーブなAST、evalするとeffect計算になってobserveするとeffect計算を簡約して本当の値が出てくるという理解でOK? #effect_study

lotz @lotz84_

exp と eval と observe の全部の実装を並べて見たいな… #effect_study

lotz @lotz84_

observe の実装を変えれば Call-by-name, Call-by-need も切り替えることが出来る #effect_study

Masahiro Sakai @masahiro_sakai

λ を Effect として解釈する話、簡単な例だけど、面白い。 #effect_study

lotz @lotz84_

コンテキストにメッセージを送る時、計算はエフェクトフルになる #effect_study

びしょ〜じょ @Nymphium

ラムダ抽象のbodyはimpure､(自由変数のない)ラムダ抽象全体はpure #effect_study

κeen @blackenedgold

nameはcontextから決まる #effect_study

Je mange, donc je suis @ryotakameoka

x という変数が出現するとき，その値は文脈に依存するので，x の値を環境から読みたいという旨のメッセージを投げる effectful な計算になる．Frege も Wittgenstein も言ってる． #effect_study

Taro Sekiyama @skymountain_

Lambda のケースは lift を使っていないのがポイントで、その意味で Lambda は特殊な扱いをしてやらないといけない(先に body を eval するなら)ということか。 #effect_study

lotz @lotz84_

type e += Get | Put of v += ってどういう意味なんだろう… #effect_study

びしょ〜じょ @Nymphium

moduleとextensible variantsによるアレですね #effect_study

Masahiro Sakai @masahiro_sakai

OCaml って type v += VInt of int みたいな書き方ができるのか。 #effect_study

lotz @lotz84_

こっからLT大会！ #effect_study

lotz @lotz84_

Geometry Of Interaction semantics for linear logic 面白そう #effect_study

κeen @blackenedgold

GoIってProof netのこと？ #effect_study

吉村 優 / YOSHIMURA Yuu @_yyu_

Effectで実装されたラムダ計算の上にEffectを乗せられるか？という質問に対してそれはできないというのはおもしろかった。 #effect_study

κeen @blackenedgold

なるほどー。 #effect_study