Functor と natural transformation に関する課題

    data Nodes a = Node a (Nodes a) (Nodes a)
           |       Leaf a
       deriving (Show)
    instance Functor Nodes where
        fmap f (Leaf a ) =  Leaf (f a)
        fmap f (Node  a b ) =  Node (fmap f a) (fmap f b)

Agda のNodes

    data Node {a} ( A : Set a ) : Set a where
       leaf  : A → Node A
       node  : Node A → Node A → Node A
    nmap : ∀ {a b} {A : Set a} {B : Set b} -> ( A -> B) -> Node A -> Node B
    nmap f (leaf v) = leaf ( f v )
    nmap f ( node v left right)  = node (f v) (nmap f left) (nmap f right)

どちらかを使って、以下の性質を確認せよ。(Haskell の場合は Test.QuickCheck を使う。Agda の場合は証明する)

Nodes が Functor であることを確認する

(1) id が id に写ることを示す(2) 分配法則 Nodes (f ○ g) = (Nodes f) ○ (Nodes g) を示す

flatten が自然変換であることを確認する

    flatten n = case n of
        Node v s t ->  (flatten s)++[v]++(flatten t)
        Leaf v ->  [v]

自然変換の可換則を記述して、正しいことを確認する。(以下の問題でも、同様)

1->T

1->T となる自然変換の例ηを挙げて、それが自然変換であることを確認せよ。

Nodes のconstructor そのもので良い。

    eta x = Leaf x

TT

Nodes (Nodes) a の fmap を定義せよ。Agda では名前を変える必要がある (nnmap とか )

ネストしたNodes がFunctorであることを確認する。

(1) id が id に写ることを示す(2) 分配法則 Nodes (Nodes (f ○ g)) = (Nodes (Nodes f)) ○ (Nodes (Nodes g)) を示す

ηT

η(T(a)) : T -> TT のこと。

    etaNodes v = eta v

etaNodes の型は何か?

作成したηとNodes の組み合わせが自然変換になることを確認せよ。

Tη

T(η(a)) のこと。η(a) は射なので、これは fmap

    nodesEta n = fmap eta n

nodesEta の型は何か?

作成したηとNodes の組み合わせが自然変換になることを確認せよ。

μ

自然変換、

   μ : TT -> T

となる例を作りたい。List の List を、平らな List にする関数を作り、それが自然変換であることを確認せよ。

   μ○Tμ と μ○μT

が何かを考えよう。これらの型は何か。

作成したμとList の組み合わせが自然変換になることを確認せよ。