Lean4のモナド系統図

1. Listはなぜかモナドから外されて単なる関手扱い。
2. 白が“クラス”で青が“インスタンス”ということだろう。
3. 矢印はクラス間の extends と、インスタンス-クラス間の member-of
4. モナドの末尾は M というネーミングルールだが、守られてはいない。
5. Pure と Bind は記法クラスで、以前の HasPure と HasBind だろう。
6. Monad, Applicative, Functor の系列を見ると、Applicateive は pure を持っている。
7. モナドの具体例は、オプションモナド、リーダーモナド、状態モナド、例外モナド

事前にListをモナドにしないで、Applicative List とかで持ち上げていくようだ。