(() => 1)() + (() => 1)() も 1 + 1 も beta-eta で同じなので同じってわけ (なお副作用
(() => 1)() + (() => 1)() も 1 + 1 も beta-eta で同じなので同じってわけ (なお副作用
let x = { print "1"; 1 } : Num a => a in x + x : Int
で、1 が出るべきか 11 が出るべきか問題な
理論屋泥臭さ避けすぎてる感はまあ分かるが、System-F レベルになってくると、たまに value restriction / sub typing translation 入ってなくて soundness が意図せずぶっ壊れてる実装はあって、やっぱ理論も大事ですねとなる時はある
弱弱なので、既存理論の言葉を categorical に言い換えるぐらいしか category theory を使えてない。やっぱ SGL ぐらいちゃんと読んどくべきなのか
category theory 学んだ後、何かの理論を categorical characterize して categorical に証明書いていくのは楽しい
このアカウントは、notestockで公開設定になっていません。
魔王ヴェスパーも好きだけど、こっちもやっぱ好き
#NowPlaying この瞬間に全てを賭けて / ZWEI2 オリジナル・サウンドトラック / ファルコム・サウンド・チーム・JDK
#AppleMusic
ChatGPT 永遠になぜ何が聞けるけど、永遠にちゃんとした回答が返ってこなくて、ちゃんと人間を反映できてる感がある
HM 推論で扱える範囲は、そもそも推論モデル作らなくていいわけだから絶対 HM 推論の方が楽そうだな、そもそも directional typing は完成形を与えてくれるわけではなく、モデル化から考えるので難易度が高そう。ただ、確かに higher-rank poly とかに HM 推論を頑張って無理やり拡張するより、一度 directional typing の手法でモデル化して、algorithm 組み上げた方が筋は良さそう
後 directional typing と HM 推論、題材が System-F だからこそ比べられることが多そうだが、directional typing 自体は別に多相型専用というわけではなく、色々応用が効く型推論のモデル化手法だが、HM type system は多相型題材の場合に基礎とできる完成されたシステムなので、そもそも比較するものでもないという
大体 bidirectional typing、bidirectional じゃなかったりするしな、type check と synthesize をいい感じに連動させてやっていこうぜってだけで、direction 自体は bi じゃなくてもいいわけだしな
HM 推論はもう古いこれからは双方向型検査に乗せられて、Dunfield 先生の論文さらった結果
* そんなことは特にない
* HM type system に bidirectional typing 導入できるが、そこから algorithmic typing 構築しても Algorithm W と似たようなことすることにはなる
みたいな感想しか持てんかった
の投稿
gredia@vrc-ins.net
このアカウントは、notestockで公開設定になっていません。
suenaga 先生アカウント見つけたが、あまりにも適当な toot した後途絶えてた
