Monad の組み合わせ

Menu Menu

---

List Monad

List をメタデータとして持つ Monad を例に使ってきた。

この Monad を

    Haskell で記述 (既に記述されている)
    Java で記述
    Agda で記述

せよ。( C++ を使っても良い。C では記述することはできない。Ruby, Python では可能か? )

Agda は以下を参考せよ。

list-level.agda list-monad.agda

---

T が Functor であることの確認

それぞれの実装について、

Monad のTに相当するものがFunctor であることを確認する論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

ηが自然変換であることの確認

それぞれの実装について、

Monad のηに相当するものが自然変換 であることを確認する可換図を書き、その論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

μが自然変換であることの確認

それぞれの実装について、

Monad のηに相当するものが自然変換 であることを確認する可換図を書き、その論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

TT が Functor であることの確認

それぞれの実装について、

Monad のTTに相当するものが自然変換 であることを確認する論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

ηT が 自然変換 であることの確認

それぞれの実装について、

Monad のTTに相当するものが自然変換 であることを確認する論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

Tη が 自然変換 であることの確認

それぞれの実装について、

Monad のTTに相当するものが自然変換 であることを確認する論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

μT が 自然変換 であることの確認

それぞれの実装について、

Monad のTTに相当するものが自然変換 であることを確認する論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

Tμ が 自然変換 であることの確認

それぞれの実装について、

Monad のTTに相当するものが自然変換 であることを確認する論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

Monad 則1

それぞれの実装について、

   μ○Tη = 1_T = μ○ηT

であることを確認する論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

Monad 則2

それぞれの実装について、

   μ○μT  = μ○Tμ

であることを確認する論理式を、それぞれのプログラミング言語で記述せよ。

Agda では可能ならば証明を示せ。

---

組み合わせ

List Monad を他のMonad と組み合わせ可能にし ( Haskell では既に定義されている )

Maybe Monad あるいは、その他のMonadの組み合わせについて、Monad 則が成立していることを確認せよ。