型理論を細々と勉強する
名古屋大学の木原貴行准教授の講義動画。
ハキハキと抑揚のある話し方が少し気になるかもしれないがすぐ慣れる。淀みなくはっきりと話すので聴きやすい。
講義の内容はテンポ良く非常にわかりやすく、ラムダ計算の説明でさえもなるほどそういうことかとすっと納得感を得られる。資料も読みやすい。
この動画で型無しラムダ計算/型付きラムダ計算/カリーハワード対応あたりを一通り理解できると型システム入門のⅠ・Ⅱ部は飛ばして読めるようになりそうだった(操作的意味論の定義の読み方の部分はキャッチアップしておいた方が良さそう)
とはいえ1章は歴史的背景とか良いこと書いてるので読んでおいた方が良さそう
ラムダ項に型がつくと何が嬉しい? -> 型の付くラムダ項の計算は停止するので
ベーシック圏論を解説してるYoutube
TAPL読んだ人の感想。TAPL読む前に目を通しておくと雰囲気わかって良い。
TaPL感想
11章から14章までは基本型~例外。TSとかRustとか書いてるときに出くわす明確にイメージできなかったワードやよく使う機能の形式的な定義なんかが書かれていたりしてほぉ〜〜となった。参照への型付けやエラーや例外どう扱うのかみたいな話もここに書いてあった。
15章は部分型について。言語機能として使うだけならOOP的なプログラミングやTSなどの構造的部分型の言語(TSやGo)がわかれば理解はできる。
18章はこれまでの型に関する話を具体的なプログラミング言語で解説している。正確な理解ではないが"ゆるふわな理解"は一気に進む。
再帰型読んでて初めて眠気に襲われた...
多相についての話はある程度使ったことのある機構なのでイメージは湧きやすい(操作的意味論が読み下せるとは言ってない)
22章のlet多相はそもそもlet多相について知らないことので何もわからん..となった
TaPL読む -> 知らない概念に出会う -> 本文を読み込む -> 意味わからん -> ググる -> 「OOOはXXXみたいなイメージやで」みたいな解説を読む -> 自分なりに噛み砕く -> TaPL読む -> 知らない概念に出会う -> ...の繰り返しである
多相わかってきた...
カインド型、カインド = 種類 じゃん!となりあ〜となりつつある
高階多相、カインドに多相を加えたものという理解であってる??