mod_poppoが型付きラムダ計算の処理系を実装する日記

mod_poppo @mod_poppo

let多相の実装がようやく形になってきた（まだ型検査器のコンパイルが通る程度で、正しく動作するとは到底言えない）

mod_poppo @mod_poppo

本当は、部分型のある体系で型再構築がどの程度できるのか、論文を参考にしつつ色々試したいんですよ

mod_poppo @mod_poppo

単純型を拡張する方向性でいくのか、System Fを制限する方向性でいくのか

mod_poppo @mod_poppo

let多相の実装がうまくいかない

mod_poppo @mod_poppo

どういうバグがあったら let f = \x. x in let a = f 1 in a の型が Int にならないんだ

mod_poppo @mod_poppo

let f = \x. x in f 1 の型は Int になるし、 let f = \x. x in f の型は forall a. a -> a 相当になるのに

mod_poppo @mod_poppo

わからん、全然わからん

mod_poppo @mod_poppo

プログラミング言語処理系実装者を殺す服

mod_poppo @mod_poppo

型推論で型注釈を省略とか言ってる軟弱者を型っ端から殴り殺す人

mod_poppo @mod_poppo

型スキームの具体化がバグってるんだろうけど

mod_poppo @mod_poppo

そもそも (\x. x) 0 の型が forall a. a になるんだが

mod_poppo @mod_poppo

これはunificationの結果が反映されていないとかそういうやつか

mod_poppo @mod_poppo

unificationの結果が反映されてないとかそういうやつだった

mod_poppo @mod_poppo

let多相を実装した（つもり） github.com/minoki/LambdaQ… pic.twitter.com/dpeu5vI7yO

拡大

mod_poppo @mod_poppo

まとめを更新しました。「mod_poppoが型付きラムダ計算の処理系を実装する日記」 togetter.com/li/1133178

mod_poppo @mod_poppo

ブログ更新した / 型システムの勉強 近況報告 blog.miz-ar.info/2017/09/type-s…

mod_poppo @mod_poppo

let多相が実装できたと言っても先はまだまだ長い

mod_poppo @mod_poppo

型システムの研究と実装って、それ専門でもない人間が片手間にできることじゃなくない？

mod_poppo @mod_poppo

片手間にやっていることが多すぎる

mod_poppo @mod_poppo

趣味で型付きラムダ計算を実装している者だ

mod_poppo @mod_poppo

本業であるべきの数学がまるで進んでないんだよなあ

mod_poppo @mod_poppo

Scalaは部分型があると思うけど型再構築ってどうなってるんだ

mod_poppo @mod_poppo

Scalaの型推論について - Togetterまとめ togetter.com/li/219702 見てる

mod_poppo @mod_poppo

自作言語の設計の参考にしたいから、各種言語の型システムと実装方式の比較が欲しい

mod_poppo @mod_poppo

素人「型付きラムダ計算ってどれがおすすめ？」 刺激の少ないものから与えてじっくり育てたいオタク「単純型付きラムダ計算かな」 珍しく同士が増えそうでテンパるオタク「let多相いいよ！」 崖から突き落として生き残った奴を選別するオタク「部分型のある体系での型再構築についてサーベ