Created
December 3, 2015 08:09
-
-
Save kosmikus/bc7d29cdbdcdae699eab to your computer and use it in GitHub Desktop.
Regensburg Haskell Meetup December 2015
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE GADTs, InstanceSigs, TypeFamilies #-} | |
{-# LANGUAGE FlexibleContexts, RankNTypes, PatternSynonyms #-} | |
module Fold where | |
import Prelude hiding (foldr, take, all) | |
--------------------------------------------------------------------------- | |
-- "foldr" on lists, Maybe, Bool, and binary trees | |
--------------------------------------------------------------------------- | |
{- | |
data [] :: * -> * where | |
[] :: [a] | |
(:) :: a -> [a] -> [a] | |
-} | |
foldr :: (a -> b -> b) -> b -> [a] -> b | |
foldr cons nil = go | |
where | |
go [] = nil | |
go (x : xs) = cons x (go xs) | |
{- | |
data Maybe :: * -> * where | |
Nothing :: Maybe a | |
Just :: a -> Maybe a | |
-} | |
foldMaybe :: b -> (a -> b) -> Maybe a -> b | |
foldMaybe nothing just = go | |
where | |
go Nothing = nothing | |
go (Just x) = just x | |
{- | |
data Bool = True | False | |
data Bool :: * where | |
True :: Bool | |
False :: Bool | |
-} | |
foldBool :: b -> b -> Bool -> b | |
foldBool true false = go | |
where | |
go True = true | |
go False = false | |
-- if c then t else e == foldBool t e c | |
data Tree :: * -> * where | |
Leaf :: a -> Tree a | |
Node :: Tree a -> Tree a -> Tree a | |
foldTree :: (a -> b) -> (b -> b -> b) -> Tree a -> b | |
foldTree leaf node = go | |
where | |
go (Leaf x) = leaf x | |
go (Node l r) = node (go l) (go r) | |
example :: Tree Integer | |
example = Node (Node (Leaf 1) (Leaf 2)) (Node (Leaf 3) (Leaf 4)) | |
productTree :: Integer | |
productTree = foldTree id (*) example | |
--------------------------------------------------------------------------- | |
-- Pattern functors and fixed points and "generic" catamorphisms / folds | |
--------------------------------------------------------------------------- | |
data TreeF :: * -> * -> * where | |
LeafF :: a -> TreeF a r | |
NodeF :: r -> r -> TreeF a r | |
-- NOTE: We make TreeF a functor in r, not in a. | |
instance Functor (TreeF a) where | |
fmap :: (r -> s) -> TreeF a r -> TreeF a s | |
fmap _ (LeafF x) = LeafF x | |
fmap f (NodeF l r) = NodeF (f l) (f r) | |
-- Tree a ~ TreeF a (Tree a) | |
-- ~ TreeF a (TreeF a (Tree a)) | |
-- ~ TreeF a (TreeF a (TreeF a (Tree a))) | |
-- ~ ... | |
outTree :: Tree a -> TreeF a (Tree a) | |
outTree (Leaf x) = LeafF x | |
outTree (Node l r) = NodeF l r | |
inTree :: TreeF a (Tree a) -> Tree a | |
inTree (LeafF x) = Leaf x | |
inTree (NodeF l r) = Node l r | |
cataTree :: (TreeF a b -> b) -> (Tree a -> b) | |
cataTree f = f . fmap (cata f) . outTree | |
-- cataTree is isomorphic to foldTree, because: | |
-- | |
-- TreeF a b -> b ~ (a -> b, b -> b -> b) | |
right :: (TreeF a b -> b) -> (a -> b, b -> b -> b) | |
right f = (\ a -> f (LeafF a), \ bl br -> f (NodeF bl br)) | |
left :: (a -> b, b -> b -> b) -> (TreeF a b -> b) | |
left ( leaf, _node) (LeafF x) = leaf x | |
left (_leaf, node) (NodeF l r) = node l r | |
-- Or: | |
-- | |
-- TreeF a b ~ a + b * b | |
-- | |
-- Therefore: | |
-- | |
-- TreeF a b -> b | |
-- ~ (a + b * b) -> b | |
-- ~ (a -> b) * (b * b -> b) | |
-- ~ (a -> b) * (b -> b -> b) | |
class (Functor (FunctorOf t)) => HasFunctor t where | |
type FunctorOf t :: * -> * | |
out_ :: t -> (FunctorOf t) t | |
in_ :: (FunctorOf t) t -> t | |
instance HasFunctor (Tree a) where | |
type FunctorOf (Tree a) = TreeF a | |
out_ :: Tree a -> TreeF a (Tree a) | |
out_ (Leaf x) = LeafF x | |
out_ (Node l r) = NodeF l r | |
in_ :: TreeF a (Tree a) -> Tree a | |
in_ (LeafF x) = Leaf x | |
in_ (NodeF l r) = Node l r | |
cata :: HasFunctor t => (FunctorOf t b -> b) -> (t -> b) | |
cata f = f . fmap (cata f) . out_ | |
-- We can also work with an explicit fixed point: | |
data Fix :: (* -> *) -> * where | |
In :: { out :: f (Fix f) } -> Fix f | |
-- Fix f ~ f (Fix f) | |
-- Fix (TreeF a) | |
-- ~ TreeF a (Fix (TreeF a)) | |
-- ~ TreeF a (TreeF a (Fix (TreeF a))) | |
-- ... | |
-- ~ Tree a | |
outT :: Tree a -> Fix (TreeF a) | |
outT (Leaf x) = In (LeafF x) | |
outT (Node l r) = In (NodeF (outT l) (outT r)) | |
inT :: Fix (TreeF a) -> Tree a | |
inT (In (LeafF x)) = Leaf x | |
inT (In (NodeF l r)) = Node (inT l) (inT r) | |
-- Cata just using Fix, without the HasFunctor | |
-- class and the relation to the "original" | |
-- Haskell type. | |
cata' :: Functor f => (f b -> b) -> (Fix f -> b) | |
cata' f = f . fmap (cata' f) . out | |
-- It's possible to just start from the functor | |
-- and work with the fixed point, just | |
-- inconvenient because we have to wrap and un-wrap | |
-- the 'In' constructor all the time. | |
-- | |
-- Pattern synonyms help somewhat | |
type Tree' a = Fix (TreeF a) | |
pattern Leaf' :: a -> Tree' a | |
pattern Leaf' x = In (LeafF x) | |
pattern Node' :: Tree' a -> Tree' a -> Tree' a | |
pattern Node' l r = In (NodeF l r) | |
--------------------------------------------------------------------------- | |
-- Excursion: take as a foldr | |
--------------------------------------------------------------------------- | |
-- First (not entirely correct) attempt | |
take :: Int -> [a] -> [a] | |
take n xs = snd (foldr go (n, []) xs) | |
where | |
go :: a -> (Int, [a]) -> (Int, [a]) | |
go x (n, xs) | n == 0 = (0, xs) | |
| otherwise = (n - 1, x : xs) | |
-- Second (better) attempt: | |
take' :: Int -> [a] -> [a] | |
take' n xs = (foldr go (const []) xs) n | |
where | |
go :: a -> (Int -> [a]) -> Int -> [a] | |
go x r n | n == 0 = [] | |
| otherwise = x : r (n - 1) | |
--------------------------------------------------------------------------- | |
-- Fold/build fusion | |
--------------------------------------------------------------------------- | |
build :: (forall b . (a -> b -> b) -> b -> b) -> [a] | |
build f = f (:) [] | |
-- An example "builder": | |
downFrom :: (Num a, Ord a) => a -> [a] | |
downFrom n' = | |
build $ \ cons nil -> | |
let go n = if n < 1 then nil else n `cons` go (n - 1) | |
in go n' | |
-- map as a build / foldr: | |
bmap :: (a -> b) -> [a] -> [b] | |
bmap f xs = | |
build $ \ cons nil -> | |
foldr (\ x r -> f x `cons` r) nil xs | |
-- Fold/build fusion rule: | |
-- | |
-- foldr cons nil (build f) == f cons nil | |
-- all as a foldr: | |
all :: (a -> Bool) -> [a] -> Bool | |
all p = foldr (\ x r -> p x && r) True | |
-- Example fusion: | |
ex1 :: Integer -> Bool | |
ex1 u = all (>1) (bmap (+1) (downFrom u)) | |
-- all (>1) (bmap (+1) (downFrom 1000) | |
-- | |
-- = { expansion of all and bmap } | |
-- | |
-- foldr (\ x r -> x > 1 && r) True | |
-- (build $ \ cons nil -> foldr (\ x r -> cons (x + 1) r) nil (downFrom 1000)) | |
-- | |
-- = { applying fold/build fusion } | |
-- | |
-- foldr (\ x r -> (\ x r -> x > 1 && r) (x + 1) r) True (downFrom 1000) | |
-- | |
-- = { beta reduction } | |
-- | |
-- foldr (\ x r -> x + 1 > 1 && r) True (downFrom 1000) | |
-- | |
-- = { expanding downFrom } | |
-- | |
-- foldr (\ x r -> x + 1 > 1 && r) True | |
-- (build $ \ cons nil -> | |
-- let go n = if n < 1 then nil else cons n (go (n - 1)) | |
-- in go 1000) | |
-- | |
-- = { applying fold/build fusion } | |
-- | |
-- let go n = if n < 1 then True else (\ x r -> x + 1 > 1 && r) n (go (n - 1)) | |
-- in go 1000 | |
-- | |
-- = { beta reduction } | |
-- | |
-- let go n = if n < 1 then True else n + 1 > 1 && go (n - 1) | |
-- in go 1000 | |
ex2 :: Integer -> Bool | |
ex2 u = let go n = if n < 1 then True else n + 1 > 1 && go (n - 1) | |
in go u | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment