https://twitter.com/kinaba のログ (twilog の方が便利です。)
| Semantic subtypingの論文 http://www.pps.univ-paris-diderot.fr/~gc/papers/semantic_subtyping.pdf (と、この次のpolymorphism入れる奴)ちゃんと読んだことがなかったので読んでた＆大変面白かった。しかし具体的な構成法が最初にあった方が読みやすいと思うんだけどこれはこだわりなのかな | |
| https://t.co/g3RRLOp4r2 「型とは値の集合のこと、subtypeとは部分集合」という素朴な解釈は、特に多態とかで自分を引数に取れる関数とか現れると難しい（値集合Vより関数達V→Vが濃度が大きく宇宙がやばい）と思われていたが小粋な小技でこの素朴な解釈を救う話 | |
| 続) 型tからsへの関数の型を「tを取ってsを返す関数全体の集合」と解釈すると破綻なのでこれを「tを取ってsを返す、しかし有限通りの引数でしか定義されてない部分関数全体」と解釈する。これは取り得る値全部の集合ではないが、""型検査に関しては元の素朴な解釈と完全に同じにふるまう"" | |
| 型検査という文脈において十分に値の集合っぽくふるまうならばそれはもうそれでありであるというダックタイピングみたいなノリで面白い | |
| RT @ranha: なーにが多相型じゃ．どうせ計算は有限，全部はいらんのでいるところを共通型で埋め込むゾイ！に通じる精神力を感じる． | |
| @ksknac @ranha あそうか、これMIXですね。 http://www.sciencedirect.com/science/article/pii/S0022000015000264 によるとindexのもう一個上なら確実に入る感じですかふむう | |
| はあーやらかしたー | |
| これはひどい | |
| たびにでたい | |
| 面倒な手続きは悪であるが、まあこういう極端な場合は面倒な手続きがあるのも仕方ないよねと認めざるをえない状況もあってそういうのは避けて生きていけばいいはずなのだが問題はそんなものが必要な状況に自らを追いやる自分は死ねばいいのにという感じである | |
| 部屋を漁った結果めんどくささレベルが2εぐらいは減った。はー |