2natlist.hs

import Numeric.Natural (Natural)

type Nat = Natural

data NatListF a = Nil | Cons (Nat, a) deriving Show
newtype NatList = In (NatListF NatList) deriving Show

out :: NatList -> NatListF NatList
out (In x) = x

natlistF :: (a -> b) -> NatListF a -> NatListF b
natlistF _ Nil          = Nil
natlistF f (Cons (n,x)) = Cons (n,f x)

fold :: (NatListF b -> b) -> NatList -> b
fold f = f . natlistF (fold f) . out

sumF :: NatListF Nat -> Nat
sumF Nil          = 0
sumF (Cons (m,n)) = m + n

sumNL :: NatList -> Nat
sumNL = fold sumF

fromListNL :: [Nat] -> NatList
fromListNL = foldr cons (In Nil)
  where
    cons n ns = In (Cons (n, ns))

ex2 :: Nat
ex2 = sumNL $ fromListNL [1..5]

31list.hs

data Base a b = Nil | Cons (a, b) deriving Show
data List a = In (Base a (List a)) deriving Show


out :: List a -> Base a (List a)
out (In x) = x

fold :: (Base a b -> b) -> List a -> b
fold f = f . base id (fold f) . out

base :: (a -> c) -> (b -> d) -> Base a b -> Base c d
base _ _  Nil         = Nil
base f g (Cons (x,y)) = Cons (f x, g y)

-- T f == fold (αY . B f id)
list :: (a -> b) -> List a -> List b
list f = fold (In . base f id)

sumF :: Base Int Int -> Int
sumF  Nil          = 0
sumF (Cons (m, n)) = m + n

sumL :: List Int -> Int
sumL = fold sumF

fromHaskList :: [a] -> List a
fromHaskList = foldr cons (In Nil)
  where
    cons x xs = In (Cons (x, xs))

sumEX :: Int
sumEX = sumL $ fromHaskList [1..5]

32list.hs

{-# LANGUAGE Rank2Types #-}

data Base a b = Nil | Cons (a, b) deriving Show
type ListF x a = Base a (x a)
newtype List a = In (ListF List a)

base :: (a -> c) -> (b -> d) -> Base a b -> Base c d
base _ _  Nil         = Nil
base f g (Cons (x,y)) = Cons (f x, g y)

out :: List a -> ListF List a
out (In x) = x

hfold :: (forall a . ListF n a -> n a) -> List b -> n b
hfold f = f . listF (hfold f) . out

listF :: (forall a . x a -> y a) -> ListF x b -> ListF y b
listF f = base id f

list :: (a -> b) -> List a -> List b
list f = In . base f (list f) . out

32nest.hs

{-# LANGUAGE Rank2Types #-}

data Base a b = Nil | Cons (a, b) deriving Show
type NestF x a = Base a (x (Pair a))
type Pair a = (a, a)
newtype Nest a = In (NestF Nest a)

-- data Nest a = Nil | Cons (a, Nest (a, a))

base :: (a -> c) -> (b -> d) -> Base a b -> Base c d
base _ _  Nil         = Nil
base f g (Cons (x,y)) = Cons (f x, g y)

out :: Nest a -> NestF Nest a
out (In x) = x

hfold :: (forall a . Base a (n (Pair a)) -> n a) -> Nest b -> n b
hfold f = f . base id (hfold f) . out

nest :: (a -> b) -> Nest a -> Nest b
nest f = In . base f (nest (pair f)) . out

pair :: (a -> b) -> Pair a -> Pair b
pair f (x, y) = (f x, f y)