Skip to content

Instantly share code, notes, and snippets.

@chengluyu
Created June 24, 2022 14:54
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save chengluyu/b241d6abf5a2aeb60f8972c121206e03 to your computer and use it in GitHub Desktop.
Save chengluyu/b241d6abf5a2aeb60f8972c121206e03 to your computer and use it in GitHub Desktop.
-- Lecture 4
-- Hylomophism
-- Definitions from previous lectures.
data Tree a = Empty | Fork (Tree a) a (Tree a)
-- We can construct a tree form a list.
build :: Ord a => [a] -> Tree a
build [] = Empty
build (x : xs) = Fork (build ys) x (build zs)
where
(ys, zs) = (filter (< x) xs, filter (>= x) xs)
-- Then we can convert the tree back to a list.
flatten :: Tree a -> [a]
flatten Empty = []
flatten (Fork t x u) = flatten t ++ [x] ++ flatten u
-- You want to describe your program.
-- Build is an anamorphism.
-- Flatten unfolds. This is a cata.
-- The `Tree a` is a `Cotree a (Nu)`.
-- It is so attempting to compose...
-- So this is a terminating program.
-- Another approach is...
-- Move away from the category set.
newtype Fix f a = In {out :: f a (Fix f a)}
class Bifunctor f where
bimap :: (a -> c) -> (b -> d) -> f a b -> f c d
cata :: Bifunctor f => (f a b -> b) -> (Fix f a -> b)
cata phi (In x) = phi (bimap id (cata phi) x)
ana :: Bifunctor f => (b -> f a b) -> (b -> Fix f a)
ana phi z = In (bimap id (ana phi) (phi z))
hylo :: Bifunctor f => (f b c -> c) -> (a -> f b a) -> a -> c
-- hylo phi psi = cata phi . ana psi
-- = phi . bimap id (cata phi) . out .
-- In . bimap id (ana psi) . psi
-- Note that `bimap f g . bimap h k = bimap (f . h) (g . k)`.
-- = phi . bimap id (cata phi . ana psi) . psi
-- = phi . bimap id (hylo phi psi) . psi
-- Therefore, we have:
hylo phi psi = phi . bimap id (hylo phi psi) . psi
-- This is the shape of divide conquer algorithms.
-- It isn't doing anything memoization. There are a lot of examples.
-- The price we pay for this is we don't get unique solutions anymore.
-- Program Calculation Properties of Continuous Algebras, Fokkinga & Meijer 1991
-- https://research.utwente.nl/en/publications/program-calculation-properties-of-continuous-algebras
{-
┌────┐ F (cata phi) ┌────┐ F (ana psi) ┌────┐
│F C │◀────────────────│F T │◀─────────────────│F A │
└────┘ └────┘ └────┘
│ │ ▲ ▲
│ │ │ │
phi │ in │ │ out │ psi
│ │ │ │
▼ ▼ │ │
┌────┐ ┌────┐ ┌────┐
│ C │◀────────────────│ T │◀─────────────────│ A │
└────┘ cata phi └────┘ ana psi └────┘
-}
-- ╔═════════════════════╗
-- ║ Recursive Coalgebra ║
-- ╚═════════════════════╝
-- Uustalu, Vene, Capretta
-- h = phi . bimap id h . psi -- "hylo equalia"
-- psi is a recursive coalgebra
-- if (*) has a unique solution for each phi
-- h = hylo phi psi (=) (*)
{-
┌─────┐ K ┌─────┐ h ┌─────┐
│ D │◀────────────│ C │◀─────────────│ A │
└─────┘ └─────┘ └─────┘
▲ ▲ │
phi │ │ phi │ psi
│ │ ▼
┌───────┐ ┌───────┐ ┌───────┐
│ F B D │◀──────────│ F B C │◀───────────│ F B A │
└───────┘ F id K └───────┘ F id h └───────┘
-}
-- Metamorphisms (J, G)
-- Structured stuff. Extract the content into something.
-- It does not fit into my categorical story well.
foldr' :: (a -> b -> b) -> b -> [a] -> b
foldr' f e [] = e
foldr' f e (x : xs) = f x (foldr' f e xs)
foldl' :: (b -> a -> b) -> b -> [a] -> b
foldl' f e [] = e
foldl' f e (x : xs) = foldl' f (f e x) xs
-- This is how things like `sum` defined in Haskell.
-- To sum a list, you keep a accumulation and...
unfoldr :: (b -> Maybe (a, b)) -> b -> [a]
unfoldr g z = case g z of
Nothing -> []
Just (x, z') -> x : unfoldr g z'
zeroToTen = unfoldr g 0
where
g x = if x <= 10 then Just (x, x + 1) else Nothing
-- Main> zeroToTen
-- [0,1,2,3,4,5,6,7,8,9,10]
-- The magic is:
stream :: (b -> a -> b) -> b -> (b -> Maybe (c, b)) -> [a] -> [c]
-- stream f e g = unfoldr f . foldl f e -- Nope!
-- e is the state, g e produces something from the initial state.
stream f y g xs = case g y of
Just (z, y') -> z : stream f y' g xs
Nothing -> case xs of
(x : xs') -> stream f (f y x) g xs'
[] -> [] -- Flush the buffers?
testStream = stream (*) 0 g [0, 1, -1]
where
g a = if a <= 4 then Just (a, a + 1) else Nothing
{-
testStream = [
0,1,2,3,4,5,6,7,8,9,10,
0,1,2,3,4,5,6,7,8,9,10,
-11,-10,-9,-8,-7,-6,-5,-4,-3,-2,-1,
0,1,2,3,4,5,6,7,8,9,10]
-}
{-
┌───┐ produce z ┌────┐
│ y │─────────────────▶│ y' │
└───┘ └────┘
│ │
consume x │ "streaming condition" │ consume x
│ │
▼ ▼
┌───────┐ ┌────────┐
│ f y x │─────────────▶│ f y' x │
└───────┘ produce z └────────┘
-}
-- If streaming condition holds, `stream = stream` on finite inputs.
fstream :: (b -> a -> b) -> b -> (b -> Maybe (c, b)) -> (b -> [c]) -> [a] -> [c]
fstream f y g h xs =
case g y of
Just (z, y') -> z : fstream f y' g h xs
Nothing -> case xs of
x : xs' -> fstream f (f y x) g h xs'
[] -> h y
-- fstream condition holds, then
-- fstream f y g h = apo ... g ... h ... . fold l f y
-- on finite input
-- converting from base 3 to base 7
type Rat = Double
fromBase3 :: [Int] -> Rat -- [0,1,2] |-> 5
fromBase3 = foldr stepr 0 where stepr d x = (fromIntegral d + x) / 3
toBase7 :: Rat -> [Int]
toBase7 = unfoldr split
where
split x = let y = 7 * x in Just (ceiling y, y - ceiling y)
fromBase3' = extract . foldl stepl (0, 1)
where
stepl (u, v) d = (d + u * 3, v / 3)
-- (u, v) represents (v *) . (u +)
extract (u, v) = v * u
-- Exercise
-- Fusion rule?
-- Can we stream it?
-- Does the streaming condition hold?
-- toBase7 . extract = unfoldr split . extract
-- = unfoldr split' where
-- split' (u, v) = let y = (floor 7 * u * v) in
-- Just (y, (u - y / (v * 7), v * 7))
-- 0.1_3 \approx 0.222_7
-- 0.11_3 \approx 0.305_7
-- It does't quite work.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment