練習問題 4.4.1

unzip [⊥]
はどうなるか． (⊥,⊥) ≠ ⊥であることを使って， 
zipp (unzip xys) ≠ xys
となるようなリスト 
xys
を構成せよ． 





unzip [⊥]

の値は，




    unzip [⊥]
=       { unzip の定義 }
    pair (map fst, map snd) [⊥]
=       { pair の定義 }
    (map fst [⊥], map snd [⊥])
=       { map の定義 } 
    (fst ⊥ : map fst [], snd ⊥ : map snd [])
=       { fst，snd，map の定義 }
    ([⊥],[⊥])

である．ここで

zipp (unzip [⊥])

は




    zipp (unzipp [⊥])
=       { 前述の運算 }
    zipp ([⊥],[⊥])
=       { zipp の定義 }
    uncurry zip ([⊥],[⊥])
=       { uncurry の定義 }
    zip (fst ([⊥],[⊥])) (snd ([⊥],[⊥]))
=       { fst，snd の定義 }
    zip [⊥] [⊥]
=       { zip の定義 }
    (⊥,⊥) : zip [] []
=       { zip の定義 }
    [(⊥,⊥)]

ここで，

(⊥,⊥) ≠ ⊥

であるから，

[(⊥,⊥)] ≠ [⊥]

である．すなわち，

xys = [⊥]

のとき，

zipp (unzip xys) ≠ xys
 
となる．