https://twitter.com/kinaba のログ (twilog の方が便利です。)
"公式RT直後の発言が分かる「RtRT」が面白い" http://nlab.itmedia.co.jp/nl/articles/1210/30/news118.html おおこれは https://t.co/TMCwNjLN これじゃないですか素晴らしい | |
そして誰も関係ある発言なんて特にしないことがわかる http://gyazo.com/e7e8e973620862211ec28ccbe476d3ab | |
RT @_tanzaku_: 今年もAdvent Calendarのページ作りました。参加してくださると嬉しいです。http://partake.in/events/3fcea6d7-0bab-4597-82db-86439aadb1b9 | |
もうそんな季節かー(アドベントカレンダー参加登録しました) | |
ぼんやりとネタ考えてたけど、去年の思い返してみると割とみんなもっと狭義競技プログラミングな感じだったな。来月までにもっといいネタ思いついたら切り替えよう | |
RT @lyrical_logical: ADT と Nested type 許す ADT と GADT の表現力の違いをきちんと理解したいんですが type theory をある程度まともに勉強しないとダメそうだしどの辺当たればいいんだろう。TAPL とかそういうのある ... | |
だいたい ADT:正規 NestedType:文脈自由 GADT:なんでもあり だろ、という把握の仕方をしているオートマトン脳です | |
ICPCのJavaチャレンジは本気でX10チャレンジ https://t.co/MOtq7wq7 とかにする気はないんだろうか。今時Java限定で何かやる意味って本気で何。 | |
@lyrical_logical TAPLを投げ捨ててTATA http://tata.gforge.inria.fr/ 読みましょう | |
マジメな話ただのADTは再帰部分が常に"T a"で不変なので相互再帰してもせいぜい有限状態しか持てないので作れるデータ構造が概ね正規木言語で、Nestedはパラメタ積めるけど構築子の型T aなので積んだパラメタaを壊せなくてその場に降ろすしかない文脈自由木言語で、GADTはヤバい | |
「作れるデータ構造」の中にどの生成規則を適用したかが(データ構築子として)必ず全ステップ含まれてしまうので、厳密に考えるとその分のギャップがあると思うけど、逆にその分のギャップしかないはず。たぶん。もしかしたら。 | |
@lyrical_logical チューリングマシン脳の恐怖( http://www.kmonos.net/pub/Presen/HiC.pdf )じゃないですけど実際一気に飛んでて文脈自由とそれ以外の違い、になってると思うので、TATAでdestructをいかに制限して無限の彼方に飛ばさないかを学びましょう | |
まあしかし他にタダの文献知らないのでTATAだけどTATA個人的にはそこまで面白くなかった… |