Monoid

なんか唐突に授業で出てきて。自分で忘れているところがな。Monoid は、

＊　単位元があって結合法則が成り立つ

というぐらいなので特に難しくはなく。

なぜ出てきたかは、ちょっと先を見たら思い出した。

＊　Monad の例に使う

というわけですね。Monad 則を満たすのにはMonoid との直積を使うのが楽らしい。もっと、一直線な授業の構成にするべきだな。

例としてはリストとか、関数の結合とかを挙げているのだけど、リストだけで十分かな?

Monoid を Haskell で定義するとかは入っていたけど、それだと単位元と結合演算だけで、結合法則が入れられない。

Monoid の定義を Agda で書いて、リストがそれを満たすことを示すとかが良いはずだが、それをいれなかった理由はなんかあるのかな? (単にさぼているだけか?!)