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


Shinji KONO / Tue Jul 1 13:08:48 2014