iso-再帰型(???)のfoldとunfold?

TAPLのiso-recursive type の説明でfoldとunfoldというのが出てきたけど、それっぽいことをする。
単に再帰型っぽく展開したりたたんだりできるだけで、実際に再帰型を作っているわけではない。

-- 再帰させたい型
data A x = A x deriving Show
data B x = B x deriving Show
data C x y = C x y deriving Show
unA (A x) = x
unB (B x) = x
unC1 (C x _) = x
unC2 (C _ y) = y

実際に、再帰っぽいデータを作る。

*Main> let x = rec (A y) ; y = rec (B (C x y)); _ = num x

(_ = num x は再帰変数にpeano数を割り当てるおまじない)

型をみたり展開したり

*Main> :t x
x :: Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))
*Main> x
Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))

*Main> unfold x
A (Rec (S Z) (B (C (Rec Z (A (Var (S Z)))) (Var (S Z)))))
*Main> :t unfold x
unfold x
  :: A (Rec (S Z) (B (C (Rec Z (A (Var (S Z)))) (Var (S Z)))))

*Main> unC1 $ unB $ unfold $ unA $ unfold x
Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))
*Main> :t unC1 $ unB $ unfold $ unA $ unfold x
unC1 $ unB $ unfold $ unA $ unfold x
  :: Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))

ソース
誰得。