- 総称型も「型」と言ってる。Type u → Type v は宇宙非エンド〈universe non-endo〉な型関数だが、これが単項〈1パラメータ〉の総称型。関手やモナドの台構造はこの種の「型」。広義の“型”上に構造が載るので型クラスになる。
- 「総称型＝型関数」という“型”上の型クラス（ベース圏上のファイブレーション）に、Functor, Applicative, Monad がある。圏論では別に型クラスを使うわけではないが（型クラス使用はメカニズムだけの問題）。
- 用語の運用： 「Option型はモナドである。」 Option型自体は総称型＝型関数。型クラスMonadが定義するファイブレーションに対して、ベースであるOption型からの増強が定義されている。という意味。
- オプション総称型＝オプション型関数がモナドになるかどうかはインスタンス環境（データベース）次第。Leanの標準環境が増強を持っている、という記述・主張。
- PureとBindは、いわゆる記法クラス。Seq, SeqLeft, SeqRightも記法クラスだが、セマンティクスも持っている模様。
- Option型は再帰的型。someとnoneは再帰的型の値コンストラクタ。値コンストラクタは、定義される再帰的型への関数とみなされる。値コンストラクタ名＝関数名。
- Option型は、再帰的型の型構成パラメータをもつので、型関数となるが、値コンストラクタが代数構造を与える。したがって、最初から代数構造を持ったパラメータ付き型〈総称型〉となる。代数構造の演算は多相関数とみなせる。
- モナド種別のクラス階層は、型クラス階層だが、これは指標の階層。指標の階層で、代数階層、位相階層、順序階層などを作る。コレクション型の階層とかも作れる。
- 自己関手を台としてその上の代数構造が、一般的代数的構造だろう。関手圏における自然変換を演算とする代数構造。あるいは、代数構造を対象とする圏への関手。関手をモノ＝対象と考えることが大事。
- 「ListがFunctorのインスタンスです」もミスリーディングだが、総称型＝型関数としてのListが、標準の定義環境において、Monad型クラスのファイブレーションに対する増強〈セクション〉を持つと言っている。
- Functor.map の中置演算子記号が <$> だった、やっぱり。Functor.map f y ≡ f <$> y
- y はとある総称型 F の値である F α の要素だとわかる。これで、台関手が特定できる。関手Fが増強可能かどうかはデータベース検索で分かる。F の増強のなかで Functor.map の具体化が定義されているからそれを使う。
- F = List のとき： y は List α の要素。List.map を探して、f <$> y ≡ List.map f y に置き換える。
- f <$> y は、名前空間が適切にセットしてあれば、y.f と同じ。<$> はドットの逆順の中置演算子になる。記号の対称性がないが、so-called メソッド呼び出し記法になる。
- y が関手で作られた型の要素で、名前空間が適切なら“オブジェクト”として扱える。メソッドはモノイドの構成素の演算（実体は自然変換）で与えられる。
- Leanは、記法クラスの利用と、マクロによる記法、それと名前空間を利用したメソッド定義が多用される。
- Functor, Applicative, Monad の階層も代数階層の一種。台が集合か型関数かの違いがあるが、指標で定義すれば同じ構造なのが分かる。
- アプリカティブは、ラックスモノイド関手のハズだが、型クラスとプログラミング的にはどう定義するのかな？
- seq : F (α → β) → F α → F β がプロファイル。F (α → β) → (F α → F β) だから、(m: F (α → β)) |→ seq f : F α → F β
- class Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f
- 型関数を"type transformer"とも呼んでいるな。"type constructor"が多い。僕は「型{値}?関数」を使っている。
- 型変換子または関手の値となる型を monadic type と呼んでいる。これはどうかな？
- 純な値とは、型変換子に作用される前の単なる型の値のこと。型変換子をコンテナに例えていることから、変換子の像の要素はラップされた値ということになるのだろう。
- within a monad とは、モナドのクライスリ圏のなかで云々の意味だろう。
- IO monadic function とは、IOモナドのクライスリ圏の射のことだろう。 IO code は、IOモナドのクライスリ圏に対して書かれたプログラムコード。pure code 〈the pure Lean code〉は元の圏に対して書かれたプログラムコード。
関手 F を適用した型 F α が構文的にずっとFを残している。つまり、関手の行き先の像集合が非常にハッキリしている。これはむしろ、像集合を取り出してファイブレーションだと考えたほうがいい。関手記号'F'のパラメータがファイブレーションの値。関手記号が再帰的型定義の値コンストラクタ記号〈タグ〉の役割を演じている。
型クラス〈ファイブレーション〉を語るときは、必ずそのインスタンス環境を述べるべき。インスタンス環境はファイブレーションの射だから、型クラス状態とは、ファイブレーションのあいだの射。射は両端を指定しないと分からない。
