https://twitter.com/kinaba のログ (twilog の方が便利です。)
@ytomino ところで突然ですが、型レベル会で何かScala/Haskell/C++/D/Agda以外の言語のネタでお話してみたりしませんか | |
@ytomino G'Camlで型レベル計算するとどういう風になるかYTさんがざっとまとめて話しつつ、思わず横から @camlspotter さんが突っ込みを入れるという展開は面白いのではないか…と僕が勝手に妄想しているだけなのですが、よろしければご検討下さいませませ | |
…と、いうことを考えつつ @camlspotter さんに何も振ってなかった。@camlspotter さんなにか発表されますか?>型レベルの会 | |
そうだustreamの流し方調べないといかん | |
ねよう | |
@ytomino 原始再帰はそれでいいと思います。型サイズは a->b より a->b->c の方が大きい的な意味で。型の式のノード数。recursiveなgenericを書くときの制約。 | |
制限取っ払ったら普通にチューリング完全になりそうな。サイズ増えないというのはどことなく文脈依存言語っぽい。 | |
いけがみさんのコメントの本意は僕も実はわかっていなくて、というのは僕の中ではどの言語においても概念としての「型」は同じものなので(もちろん言語の能力の内で定義できる型は違う)。ただ、そうであるということはそのまま、僕の「型の定義」といけがみさんのが違うことを意味していて当に違いが | |
@ikegami__ http://atnd.org/events/451 の「初歩的な講義」というのはもう少し具体的にどんな感じのことを想定されてますか? | |
handbook of satisfiability 届いたこれは萌える | |
でかけr | |
http://twitter.com/hogelog/status/1398469270 素晴らしいなー。 | |
@camlspotter おお!やっぱりそうなのですね。証明眺めてみます。 | |
@chunjp <censored> | |
きたく。Twitterはじめるまでテレビの視聴率20%とか30%とか絶対嘘だろーとひそかに思ってたのけどTL見てると普通にそんなこともありそうだと思えるように最近なってきた…。 | |
@filil あとこの前のWBCも結構すごかったw | |
@nodchip さっきやる気満々でpracticeのAを素で間違えたのでどうしたものか状態 | |
てきとうに2,3時間くらいやるかも |