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 則が成立していることを確認せよ。