Notes from Bananas, Lenses, Envelopes, and Barbed Wire. Will clean these notes up at some point. The Haskell Implementation is a old. Refer to this version: https://gist.github.com/ssbothwell/5464663d1c111de0e49342ae6ea12309

bananas-notes.hs

{-# Language
        FlexibleContexts,
        UndecidableInstances,
        TypeSynonymInstances,
        DeriveGeneric,
        DeriveDataTypeable,
        DeriveFunctor,
        StandaloneDeriving,
        ScopedTypeVariables,
        TypeFamilies #-}
module RecursionSchemesNotes where

import Data.List
import Data.Data
import GHC.Generics
import Test.QuickCheck


--------------------
-- List Morphisms --
--------------------

cataL :: (a -> b -> b) -> b -> [a] -> b
cataL _ b [] = b
cataL f b (a:as) = a `f` (cataL f b as)

lengthL :: [a] -> Int
lengthL = cataL (\a b -> 1 + b) 0

filterL :: (a -> Bool) -> [a] -> [a]
filterL p = cataL (\a b -> if p a then (a:b) else b) []

-- Fusion Law for Catamorphism
a :: Foldable t => (b -> c) -> (a -> b -> b) -> b -> t a -> c
a z f b = z . foldr f b


--a' :: Foldable t => (b -> c) -> (a -> b -> b) -> b -> t a -> c
--a' z f b = foldr f' b'
--    where f' x y = f x (z y)
--          b' = z b

anaL :: (b -> Bool) -> (b -> (a, b)) -> b -> [a]
anaL p g b =
    case p b of
        True -> []
        False -> a:(anaL p g b')
    where (a, b') = g b

zipL :: (Eq a, Eq b) => ([a], [b]) -> [(a,b)]
zipL = anaL p g
    where p (as, bs) = (as == []) || (bs == [])
          g ((x:xs), (y:ys)) = ((x,y), (xs, ys))

iterateL :: (a -> a) -> a -> [a]
iterateL f a = anaL p g a
    where p _ = False
          g a' = (a', f a')

mapL :: (a -> b) -> [a] -> [b]
mapL f as = anaL p g as
    where p xs = length xs == 0
          g (x:xs) = (f x, xs)

hyloL :: c -> (b -> c -> c) -> (a -> (b, a)) -> (a -> Bool) -> a -> c
hyloL c f g p a = 
    case p a of
        True -> c
        False -> b `f` (hyloL c f g p a')
    where (b, a') = g a

facL = hyloL 1 (*) g p
    where g n = (n, n-1)
          p n = n == 0

data Nat = Z | S Nat deriving (Show, Eq)

addNat :: Nat -> Nat -> Nat
addNat Z b = b
addNat (S a) b = S (addNat a b)

multNat :: Nat -> Nat -> Nat
multNat a b = go a b
    where go (S Z) y = y
          go (S x) y = go x (addNat b y)
          go Z y = Z

paraL :: (Nat -> b -> b) -> b -> Nat -> b
paraL f b Z = b
paraL f b (S n) = n `f` (paraL f b n)

paraLFac :: Nat -> Nat
paraLFac = paraL f b
    where f n acc =  (S n) `multNat` acc
          b = S Z

--------------
-- Functors --
--------------

-- a Bifunctor Ϯ is a binary operation taking types into types and
-- functions into functions such that if f ∈ A -> B and g ∈ C -> D
-- fϮg ∈ AϮC -> BϮD, and which preserves identities and composition:
-- 
-- idϮid = id
-- fϮg ∘ hϮj = (f ∘ h)Ϯ(g ∘ j)
--
-- a functor is unary type operation F, which also is an operation on
-- functions, F ∈ (A -> B) -> (Af -> Bf) that preserves identity and
-- composition
class (Bifunctor f) where
    bimap :: (a -> b) -> (c -> d) -> f a c -> f b d

-- D||D' = {(d, d')|d ∈ D,d' ∈ D'}
data Product a b = Product a b deriving (Eq, Show)

instance Bifunctor Product where
    --bimap f g (Product a b) = Product (f a) (g b)
    bimap f g = (f . fst') `tupling` (g . snd')
--  (f||g) (x, x') = (f x, g x')

instance Functor (Product a) where
    fmap f pab = bimap id f pab

--- Related Combinators ---

-- Projection 
-- `π (x, y) = x
fst' :: Product a b -> a
fst' (Product a b) = a
-- π` (x, y) = y
snd' :: Product a b -> b
snd' (Product a b) = b
-- Tupling
-- (f ∆ g) = (f x, g x)    
tupling :: (a -> b) -> (a -> c) -> a -> Product b c
tupling f g = \x -> Product (f x) (g x)


-- D|D' = ({0}||D)U({1}||D')U{⊥}
data Sum a b = A a | B b | Bottom deriving (Eq, Show)

instance Bifunctor Sum where
    --bimap f g = (leftInjection . f) `selection` (rightInjection . g)
    bimap f _ (A a) = A $ f a
    bimap _ g (B b) = B $ g b
    bimap _ _ Bottom = Bottom
--  (f|g) ⊥ = ⊥
--  (f|g) (0, x) = (0, f x)
--  (f|g) (1, x') = (1, f x')

instance Functor (Sum a) where
    fmap f sum = bimap id f sum

--- Related Combinators ---
leftInjection :: a -> Sum a b
leftInjection = A

rightInjection :: b -> Sum a b
rightInjection = B

selection :: (a -> c) -> (b -> c) -> Sum a b -> c
selection f g = \x -> case x of
            A a -> f a
            B b -> g b

newtype Reader r a = Reader { runReader :: r -> a }

instance Bifunctor Reader where
    bimap f g (Reader ra) = Reader $ \r -> undefined

instance Functor (Reader r) where
    fmap f (Reader ra) = Reader $ \r -> f (ra r)

-- Arrow Function
(.->) f g = \h -> g . h . f

--- Related Combinators ---
curry' :: ((a, b) -> c) -> (a -> b -> c)
curry' f a b = f (a, b)

uncurry' :: (a -> b -> c) -> ((a, b) -> c)
uncurry' f (a, b) = f a b

eval' :: ((a -> b), a) -> b
eval' (f, x) = f x

newtype Identity a = Identity a deriving (Eq, Show)

instance Functor Identity where
    fmap f (Identity a) = Identity $ f a

newtype Const a b = Const a deriving (Eq, Show)

instance Functor (Const a) where
    fmap f ca = bimap id f ca

instance Bifunctor Const where
    bimap f g (Const a) = Const $ f a


-- Lifting
-- For functors F, G and bifunctor Ϯ we define the functors FG and FϮG by:
-- 
-- X(FG) = X(F)G
-- X(FϮG) = (XF)Ϯ(XG)
--
-- For both types and functions X

-- Sectioning
-- ???

---------------------
-- Combinator laws --
---------------------

instance (Arbitrary a, Arbitrary b) => Arbitrary (Product a b) where
    arbitrary = Product <$> arbitrary <*> arbitrary

instance (Arbitrary a, Arbitrary b) => Arbitrary (Sum a b) where
    arbitrary = frequency [(1, A <$> arbitrary)
                          ,(1, B <$> arbitrary)]

instance Arbitrary a => Arbitrary (Identity a) where
    arbitrary = Identity <$> arbitrary

instance (Arbitrary a) => Arbitrary (Const a b) where
    arbitrary = Const <$> arbitrary

instance (CoArbitrary a, CoArbitrary b) => CoArbitrary (Sum a b) where
    coarbitrary (A x)  = variant 0 . coarbitrary x
    coarbitrary (B y) = variant 1 . coarbitrary y

type F = Int -> Int
type H = Sum Int Int -> Int

--  `π ∘ f||g == f ∘ π
prop (Fn (f :: F)) (Fn (g :: F)) x y =
    (fst' . bimap f g) (Product x y) == (f . fst') (Product x y)

prop1 :: (Int -> Int) -> (Int -> Int) -> Int -> Int -> Bool
prop1 f g x y = (fst' . bimap f g) (Product x y) == (f . fst') (Product x y)

-- `π ∘ f ∆ g = f
-- \x.(`π ∘ f ∆ g) x = f x
prop2 x (Fn (f :: Int -> Int)) (Fn (g :: Int -> Int)) =
    (fst' . (f `tupling` g)) x == f x

--  π` ∘ f||g == g ∘ π
prop3 (Fn (f :: F)) (Fn (g :: F)) x y =
    (snd' . bimap f g) (Product x y) == (g . snd') (Product x y)


-- π` ∘ f ∆ g = g x
-- \x.(π` ∘ f ∆ g) x = g x
prop4 x (Fn (f :: F)) (Fn (g :: F)) =
    (snd' . (f `tupling` g)) x == g x

-- TODO: What is the signature of h? It seems like it 
-- would have to return a Product.
-- (`π ∘ h) ∆ (π` ∘ h) = h
-- \x.((`π ∘ h) ∆ (π` ∘ h)) x = h x
--prop5 x (Fn (h :: Int -> Int)) =
--    ((fst' . h) `tupling` (snd' . h)) x == h x

-- `π ∆ π` = id
-- \x.(`π ∆ π`) x = id x
prop6 x = (fst' `tupling` snd') x == id x

-- f||g ∘ (h ∆ j) = (f ∘ h) ∆ (g ∘ j)
-- \x.(f||g ∘ (h ∆ j)) x = \x.((f ∘ h) ∆ (g ∘ j)) x
prop7 x (Fn (f :: F)) (Fn (g :: F)) (Fn (h :: F)) (Fn (j :: F)) = 
    (bimap f g) ((h `tupling` j) x) == ((f . h) `tupling` (g . j)) x


-- f ∆ g ∘ h = (f ∘ h) ∆ (g ∘ h)
-- \x.(f ∆ g ∘ h) x = \x.(f ∘ h) ∆ (g ∘ h)) x
prop8 x (Fn (f :: F)) (Fn (g :: F)) (Fn (h :: F)) = 
    ((f `tupling` g) . h) x == ((f . h) `tupling` (g . h)) x

-- NOTE: This implication cannot be proven with random testing
-- f||g === h||j = f = h ∧ g = j	
-- \x. y.((f||g) x y ==  (h||j) x y) === \x y.(f x == h x) ^ (g y == j y)
prop9 x y (Fn (f :: F)) (Fn (g :: F)) (Fn (h :: F)) (Fn (j :: F)) = 
    (bimap f g (Product x y)) == (bimap h j (Product x y)) ==>
        f x == h x && g y == j y

-- NOTE: This implication cannot be proven with random testing
-- f ∆ g = h ∆ j === f = h ∧ g = j
-- \x.(f ∆ g = h ∆ j) x === \x.(f x == h x) ^ (g x == j x)
prop10 x (Fn (f :: F)) (Fn (g :: F)) (Fn (h :: F)) (Fn (j :: F)) = 
    (f `tupling` g $ x ) == (h `tupling` j $ x ) ==>
        (f x == h x) && (g x == j x)

-- f|g ∘ `i = `i ∘ f 
-- \X.(f|g (X|Y) . (`i X)) = \X.`i ∘ (f X)
prop11 x (Fn (f :: F)) (Fn (g :: F)) =
    ((bimap f g) . leftInjection) x == (leftInjection . f) x

-- f ∇ g ∘ `i = f
-- \x. (f ∇ g ∘ `i) x = f x
prop12 x (Fn (f :: F)) (Fn (g :: F)) =
   ((f `selection` g) . leftInjection) x == f x

-- f|g ∘ i` = i` ∘ g 
-- \X.(f|g (X|Y) . (`i X)) = \X.`i ∘ (f X)
prop13 x (Fn (f :: F)) (Fn (g :: F)) =
    ((bimap f g) . rightInjection) x == (rightInjection . g) x

-- f ∇ g ∘ `i = f
-- \x. (f ∇ g ∘ i`) x = g x
prop14 x (Fn (f :: F)) (Fn (g :: F)) =
   ((f `selection` g) . rightInjection) x == g x

-- TODO: What does strict mean?
-- TODO: How to use the Sum CoArbitrary Instance
-- (h ∘ `i) ∇ (h ∘ i`) = h <== h strict
prop15 xy (Fn (h :: H)) =
    ((h . leftInjection) `selection` (h . rightInjection)) xy

-- `i ∇ i` = id
-- \x.(`i ∇ i`) x = id x
prop16 x = (leftInjection `selection` rightInjection) x == id x

-- f ∇ g ∘ h|j = (f ∘ h) ∇ (g ∘ j)
-- \x.(f ∇ g ∘ h|j) x = ((f ∘ h) ∇ (g ∘ j)) x
prop17 x (Fn (f :: F)) (Fn (g :: F)) (Fn (h :: F)) (Fn (j :: F)) = 
    ((f `selection` g) . (bimap h j)) x == ((f . h) `selection` (g . j)) x

-- TODO: What does strict mean?
-- f ∘ g ∇ h = (f ∘ g) ∇ (f ∘ h) <== h strict 
-- \X|Y.((f ∘ g ∇ h) X|Y) = \X|Y.((f ∘ g) ∇ (f ∘ h)) X|X
prop18 xy (Fn (f :: F)) (Fn (g :: F)) (Fn (h :: F)) =
    (f . (g `selection` h)) xy == ((f . g) `selection` (f . h)) xy

-- NOTE: This implication cannot be proven with random testing
-- f|g = h|j === f = h ∧ g = j
-- \X|Y.f|g X|Y = h|j X|Y === f x = h x ∧  g y = j y
prop19 xy (Fn (f :: F)) (Fn (g :: F)) (Fn (h :: F)) (Fn (j :: F)) =
    undefined

-- NOTE: This implication cannot be proven with random testing
-- f ∇ g = h ∇ j === f = h ∧ g = j
-- \X|Y.f ∇ g X|Y = h ∇ j X|Y === f x = h x ∧  g y = j y
prop20 xy (Fn (f :: F)) (Fn (g :: F)) (Fn (h :: F)) (Fn (j :: F)) =
    undefined

-----------
-- Varia --
-----------

-- p ∈ A -> Bool

-- p? ∈ A -> A|A
-- p? a = ⊥,    p a = ⊥ 
--      = `i a, p a = true
--      = i` a, p a = false


pq :: (a -> Bool) -> a -> Sum a a
pq p a = 
    case p a of
        True -> leftInjection a
        False -> rightInjection a

propVaria1 x (Fn (f :: F)) (Fn (g :: F)) (Fn (p :: Int -> Bool)) =
    ((f `selection` g) . (pq p)) x == if p x then f x else g x

void _ = ()

propVaria2 x (Fn (f :: F)) = (void . f) x == void x

-- p? ∘ x = x|x ∘ (p ∘ x)?
propVaria3 x (Fn (f :: Int -> Int)) (Fn (p :: Int -> Bool)) =
     (((pq p) . f) x) == ((bimap f f) . ((pq (p . f)))) x

-- In order to make recursion explicit, we use:
-- µ ∈ (A -> A) -> A 
-- µ f = x where x = f x
u :: (a -> a) -> a
u f = x where x = f x

-- Least Fixed Point Recursion Example:
len xs = if xs == [] then 0 else 1 + len (tail xs)

len' :: Eq a => [a] -> Int
len' = u (\rec xs -> if xs == [] then 0 else 1 + rec (tail xs))


-----------------------------
-- Natural Transformations --
-----------------------------

-- let F and G be functors and φA ∈ AF -> AG for any type A.
-- φA is a polymorphic function.  A Natural Transformation 
-- is a family of functions φA such that:
-- ∀f: f ∈ A -> B: φB ∘ fF = fG ∘ φA 

f :: x -> y
f = undefined

fF :: Functor f => f x -> f y
fF = fmap f

fG :: Functor g => g x -> g y
fG = fmap f

nat :: (Functor f, Functor g) => f a -> g a
nat = undefined

data Id a = Id a deriving (Show, Functor)
data Yd a = Yd a deriving (Show, Functor)

natId :: Id a -> Yd a
natId (Id a) = Yd a

natYd :: Yd a -> Id a
natYd (Yd a) = Id a

-- Let F be a monofunctor
-- Let L be a type
-- inF ∈ LF -> L 
-- outF ∈ L -> LF


--in' :: List' a (List a) -> List a
--in' Nil' = Nil
--in' (Cons' a x) = Cons a x

--out' :: List a -> Fixable (List a) (List a)
--out' Nil = Nil'
--out' (Cons a as) = Cons' a as

-- NOTE: What is the left arrow here?
-- id = µ (in <- out)
-- µF denotes the pair (L, in)
-- µF is the least fixed point of F

-- Using the fixed point to define a recursive list:
-- XL = 1|(A||X)
-- (A*, in) = µL

--------------------------------
---- Haskell Implementation ----
--------------------------------

newtype Fix f = Fix { unFix :: f (Fix f) } deriving (Generic, Typeable)

fix :: (a -> a) -> a
fix f = let x = f x in x

genCata :: Functor f => (f a -> a) -> (Fix f -> a)
genCata alg = alg . fmap (genCata alg) . unFix

genAna :: Functor f => (a -> f a) -> a -> Fix f
genAna coAlg = Fix . fmap (genAna coAlg) . coAlg

genHylo :: Functor f => (f b -> b) -> (a -> f a) -> a -> b
genHylo phi psi = genCata phi . genAna psi


----------------------
---- List Example ----
----------------------

-- type List a = Fix (ListF a)
data List a = Nil | Cons a (List a)
data ListF a x = NilF | ConsF a x deriving Functor


fromL :: [a] -> Fix (ListF a)
fromL = foldr (\a b -> Fix (ConsF a b)) (Fix NilF)

toList :: Fix (ListF a) -> [a]
toList = 
    genCata (\xs -> case xs of
        NilF -> [] 
        ConsF a as -> a : as)

listLengthAlg :: Num p => ListF a p -> p
listLengthAlg x = 
    case x of
        NilF -> 0
        (ConsF _ n) -> n + 1
  
listLengthCata :: Num a => [a] -> a
listLengthCata = genCata listLengthAlg . fromL

listSumAlg :: Num p => ListF p p -> p
listSumAlg x = 
    case x of
        NilF -> 0
        (ConsF a r) -> a + r

listSumCata :: Num a => [a] -> a
listSumCata = genCata listSumAlg . fromL

listFilterAlg :: (a -> Bool) -> ListF a [a] -> [a]
listFilterAlg p x =
        case x of
            NilF -> []
            (ConsF a r) -> if p a then (a:r) else r

listFilterCata :: (a -> Bool) -> [a] -> [a]
listFilterCata p = genCata (listFilterAlg p) . fromL

listFoldAlg :: Monoid a => ListF a a -> a
listFoldAlg x = 
    case x of
        NilF -> mempty
        (ConsF a r) -> a `mappend` r

listFoldCata :: Monoid a => [a] -> a
listFoldCata = genCata listFoldAlg . fromL

listFoldrAlg :: (a -> b -> b) -> b -> ListF a b -> b
listFoldrAlg f b x =
    case x of
        NilF -> b
        (ConsF a r) -> f a r

listFoldrCata :: (a -> b -> b) -> b -> [a] -> b
listFoldrCata f b = genCata (listFoldrAlg f b) . fromL

listMapAlg :: (a -> b) -> ListF a [b] -> [b]
listMapAlg f x =
    case x of
        NilF -> []
        (ConsF a r) -> (f a):r

listMapCata :: (a -> b) -> [a] -> [b]
listMapCata f = genCata (listMapAlg f) . fromL
        

-----------------------------
---- Binary Tree Example ----
-----------------------------

--type BinTree a = Fix (BinTreeF a)
data BinTree a = Leaf | Branch (BinTree a) a (BinTree a) deriving Show
data BinTreeF a x = LeafF | BranchF x a x deriving Functor 


fromT :: BinTree a -> Fix (BinTreeF a)
fromT Leaf = Fix LeafF
fromT (Branch l a r) = Fix (BranchF (fromT l) a (fromT r))

toT :: Fix (BinTreeF a) -> BinTree a
toT =
    genCata (\tree -> case tree of
        LeafF -> Leaf
        BranchF l a r -> Branch l a r)

treeSumAlg :: Num a => BinTreeF a a -> a
treeSumAlg x =
    case x of
        LeafF -> 0
        BranchF l a r -> l + a + r

treeSumCata :: Num a => BinTree a -> a
treeSumCata = genCata treeSumAlg . fromT

-- TODO: Implement Factor Tree anamorphism
factorTreeCoAlg :: [Integer] -> Integer -> BinTreeF Integer Integer
factorTreeCoAlg primes 0 = LeafF
factorTreeCoAlg primes 1 = LeafF
factorTreeCoAlg primes n 
    | n `elem` primes = LeafF
    | otherwise = BranchF left n right
    where left = case find (\a -> n `mod` a == 0 && n /= a) primes of
                    Just x' -> x'
                    Nothing -> 1
          right = n `div` right

factorTreeAna n = toT . genAna (factorTreeCoAlg primes) $ n
    where primes = takeWhileS (\x -> x <= (n `div` 2)) $ sieveAna [2..]

factorTree :: Integer -> BinTree Integer
factorTree 0 = Leaf
factorTree 1 = Leaf
factorTree n = Branch left n right
    where primes = takeWhileS (\x -> x <= n) $ sieveAna [2..]
          p = case find (\a -> n `mod` a == 0 && n /= a) primes of
                    Just x' -> x'
                    Nothing -> 1
          left = if p == 1 then Leaf else Branch Leaf p Leaf
          right = if n `elem` primes then Leaf else (factorTree $ n `div` p)

data FactorTree = 
      Prime Integer 
    | Composite FactorTree Integer FactorTree
    deriving Show

factorTree' :: Integer -> FactorTree
factorTree' n
    | n `elem` primes = Prime n
    | otherwise = Composite (Prime left) n right
    where primes = takeWhileS (\x -> x <= n) $ sieveAna [2..]
          left = case find (\a -> n `mod` a == 0 && n /= a) primes of
                    Just x' -> x'
                    Nothing -> 1
          right = factorTree' $ n `div` left



------------------------------
---- General Tree Example ----
------------------------------

-- type GenTree a = Fix (GenTreeF a)
data GenTree a = GenLeaf | GenBranch a [GenTree a] deriving Show
data GenTreeF a x = GenLeafF | GenBranchF a [x] deriving Functor

toGT :: Fix (GenTreeF a) -> GenTree a
toGT = 
    genCata (\tree -> case tree of
        GenLeafF -> GenLeaf
        GenBranchF x xs -> GenBranch x xs)

fromGT :: GenTree a -> Fix (GenTreeF a)
fromGT GenLeaf = Fix GenLeafF
fromGT (GenBranch x xs) = Fix (GenBranchF x (fmap fromGT xs))

genTreeSumAlg :: Num a => GenTreeF a a -> a
genTreeSumAlg x =
    case x of
        GenLeafF -> 0
        GenBranchF x xs -> x + sum xs

genTreeSumCata :: Num a => GenTree a -> a
genTreeSumCata = genCata genTreeSumAlg . fromGT


------------------------
---- Stream Example ----
------------------------

data Stream a = Stream a (Stream a) deriving Show

--type Stream a = Fix (SteamF a)
data StreamF a x = StreamF a x deriving Functor


-- TODO: Rewrite take and takeWhile using recursion schemes:
takeS :: Int -> Stream a -> [a]
takeS 0 s = []
takeS n (Stream a as) = a : (takeS (n-1) as)

takeWhileS :: (a -> Bool) -> Stream a -> [a]
takeWhileS p (Stream a as) =
    case p a of
        True -> a:(takeWhileS p as)
        False -> []

fromS :: Stream a -> Fix (StreamF a)
fromS (Stream a as) = Fix (StreamF a (fromS as))

toS :: Fix (StreamF a) -> Stream a
toS = genCata (\(StreamF a x) -> Stream a x)

countCoAlg :: Integer -> StreamF Integer Integer
countCoAlg n = StreamF n (n+1)

fibCoAlg :: (Integer, Integer) -> StreamF (Integer, Integer) (Integer, Integer)
fibCoAlg (n, m) = StreamF (n, m) ((m, m + n))

sieveCoAlg :: [Integer] -> StreamF Integer [Integer]
sieveCoAlg (p:ps) = StreamF p (filter (\x -> x `mod` p /= 0) ps)

countAna :: Integer -> Stream Integer
countAna = toS . genAna countCoAlg

fibAna :: (Integer, Integer) -> Stream (Integer, Integer)
fibAna = toS . genAna fibCoAlg

-- TODO: Test performance of sievaAna
sieveAna :: [Integer] -> Stream Integer
sieveAna = toS . genAna sieveCoAlg