http://msakai.jp/d/?date=20100628 を参考にした 前に挫折した覚えがあるがよくよく考えてみればfoldnとnatを対応させたのだからunfoldnとconatを対応させるだけだった

conat.hs

{-# LANGUAGE RankNTypes, ExistentialQuantification #-}

-- forall X, N -> (X + 1 -> X) -> X
-- N -> (forall X, (X + 1 -> X) -> X)
-- => forall X, (X + 1 -> X) -> X
--
-- forall X, (X -> X + 1) -> X -> N
-- (exists X, (X -> X + 1) * X) -> N
-- => exists X, (X -> X + 1) * X

data N = Zero | Succ N
newtype Nat = Nat (forall x. (Maybe x -> x) -> x)
data CoNat = forall x. CoNat (x -> Maybe x) x

inn :: Maybe N -> N
inn Nothing = Zero
inn (Just n) = Succ n
outn :: N -> Maybe N
outn Zero = Nothing
outn (Succ n) = Just n

casen :: (Maybe N -> a) -> N -> a
casen f = f . outn
foldn :: (Maybe a -> a) -> N -> a
foldn f = let go = f . fmap go . outn in go

uncasen :: (a -> Maybe N) -> a -> N
uncasen f = inn . f
unfoldn :: (a -> Maybe a) -> a -> N
unfoldn f = let go = inn . fmap go . f in go

-- curry
foldnC :: (a -> a) -> a -> N -> a
foldnC f z = go
  where
    go Zero = z
    go (Succ n) = f (go n)

toInt :: N -> Int
toInt = foldnC (+ 1) 0

instance Show N where
  show = show . toInt

nat2n :: Nat -> N
nat2n (Nat fo) = fo inn
n2nat :: N -> Nat
n2nat n = Nat (\g -> foldn g n)
con2n :: CoNat -> N
con2n (CoNat g x) = unfoldn g x
n2con :: N -> CoNat
n2con n = CoNat outn n

infn :: N
infn = Succ infn