Hちょびよみ勉強ノート(4 〜 7回目)
ブログ書くのむっちゃサボってる…。
多相の種類
polymorphism ┬ universal(静的) ┬ parametric(ジェネリクス)
│ └ inclusion(サブタイプ) ┬ nominal(継承)
│ └ structural(ダックタイピング)
└ ad-hoc(実行時) ┬ overloading(オーバーロード)
└ coercion(暗黙の型変換)
カリー化
他引数関数を1引数関数のチェーンにすること
(a, b, c) -> d ↓ a -> (b -> (c -> d))
カリー化すると何が嬉しい？
- 関数が取り回しやすくなる
- ラムダ計算界隈の話に載せられるようになる
カタモーフィズム
「Listはfoldrだ」
- List(データ構造)
- foldr(処理構造)
- f(a1, f(a2, f(a3, ..., f(an, zero) ... )
なんか構造が似ている気がする。
似ている？
Listの定義(Aは型変数)
List<A> : Nil | cons(A, List<A>) # Nilか任意の値とリストの組 nil : () -> Nil cons : A × List<A> -> List<A> # 任意の値とリストの組でリストにする head : A × List<A> -> A # 任意の値とリストの組から先頭の要素を取り出す tail : A × List<A> -> List<A> # 任意の値とリストの組から先頭以外のリストを取り出す isnil : List<A> -> Boolean # リストがnilかどうか
tailやheadが組になってるのは要素が最低1はあるってことを言いたいのかな？
folrの定義(AとBは型変数)
f : A × B -> B zero : Nil -> B foldr(f, zero) : List<A> -> B
似ている。
| List | cons : A × List -> List | nil : () -> Nil |
| foldr | f : A × B -> B | zero : Nil -> B |
List
cons
／＼
a1 cons
／＼
a2 cons
／＼
a3 nilfoldr
f
／＼
a1 f
／＼
a2 f
／＼
a3 zero似ている*2。
ListはF始代数*3
foldrの最も汎用的な形がList*4。
↓
foldrの始対象がList*5。
↓
ListはF代数の圏におけるF始代数*6
List foldr
cons f
／＼ ／＼
a1 cons a1 f
／＼ <------ 抽象的 ------ ／＼
a2 cons - 関数(射)が作れそう-> a2 f
／＼ ／＼
a3 nil a3 zero
可換図式*7
何を書いているのか分からねーと思うが僕も何を書いているのかわからない。
List<A> = Nil | A × List<A>
foldr↓ ↓ id | id × foldr(f, zero)
B ← Nil | A × B
(ex, sum)良くどころか完全に分からないんだけど、結局のところ何故foldrがListの様に見えるのかというと上の図の下向き矢印に当たる関数が存在するから、とのこと…。
とにかく、代数的データ型(F代数の構造を持つもの→右側が再帰している構造のもの)のうち最も汎用的なもの(始代数)がListであり、代数的データ型であればfoldrが出来る、という事？
Optionは要素数が0か1のList、Eitherは要素数が2固定のListという風にみなせるらしい。
要するに
ルノアールで2時間聞いただけで理解できるはずがなかった
