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

mod_poppo @mod_poppo

自作言語の型システムを設計したいのでTaPLを読んでいる

mod_poppo @mod_poppo

算術演算子のオーバーロードをするのに、intersection typeを入れるか、型クラス的なものを入れるか

mod_poppo @mod_poppo

フルのintersection typeを入れるのはtype reconstructionが不可能になるらしいから避けたいが、じゃあどの程度まで制限すればいいのか

mod_poppo @mod_poppo

型クラス的なやつだと、 abs : Int → Int と abs : Complex → Real みたいなアドホックなオーバーロードができないんじゃないかという気がする

mod_poppo @mod_poppo

intersection typeの実装は面倒くさいな〜〜〜

mod_poppo @mod_poppo

新しく型検査器を作るならCoqとかで正しさの証明をつけておきたい気がするが

mod_poppo @mod_poppo

複数引数の関数をカリー化することにすると、arityが違う関数のオーバーロードをしようとしたときに 関数型 vs それ以外 の交差が空でないという状況が発生しうる

mod_poppo @mod_poppo

TaPLにはintersection typeについてはあまり詳しく書いてないので、挙げられている文献を読んだ方がいいのだろうが、しかし入手性が

mod_poppo @mod_poppo

東大の図書館にあるか、ネットに落ちているか、東大の学内ネットからアクセスできるのであればいいんだけど

mod_poppo @mod_poppo

不労所得で30代くらいから悠々自適に過ごしたい

mod_poppo @mod_poppo

人生短いんだから好きな時に好きなことをするしかない

mod_poppo @mod_poppo

まともで使いやすい型システムを設計して実装するのは大変だし、もしプログラミング言語を何か作れと言われたら動的型にすると思う

mod_poppo @mod_poppo

有償の論文を学内のネットワークからタダで落とせることが判明した時が「大学にいて良かった〜〜〜〜」と思う瞬間である

mod_poppo @mod_poppo

有界量化

mod_poppo @mod_poppo

趣味で型システムの論文を読んでいる者だ

mod_poppo @mod_poppo

Coqで証明されたプログラムを作るには、プログラム全体を一旦Coqで書かないといけない？

mod_poppo @mod_poppo

TaPLでは項に関する抽象と型に関する抽象を両方とも小文字のラムダで書いている

mod_poppo @mod_poppo

部分型と交差型と多相性（有界量化）を持ったシステムをでっち上げたい

mod_poppo @mod_poppo

その際に、型チェックだか部分型関係だかのアルゴリズムが停止するようにしたい

mod_poppo @mod_poppo

intersection typesってunion typesよりも歴史的に古い概念なのか？

mod_poppo @mod_poppo

お金が無限に欲しい

mod_poppo @mod_poppo

まずSystem Fを実装します

mod_poppo @mod_poppo

ご飯を食べる間も惜しんでSystem F

mod_poppo @mod_poppo

俺、このSystem F実装が終わったらご飯食べるんだ