Skip to content

Instantly share code, notes, and snippets.

@nrolland
Created April 29, 2021 17:33
Show Gist options
  • Save nrolland/d794cc9fff6ef65d89b7f754099baf0b to your computer and use it in GitHub Desktop.
Save nrolland/d794cc9fff6ef65d89b7f754099baf0b to your computer and use it in GitHub Desktop.
foldr and foldl on ∫ A : A^{op} ⊗ A → Set
-- post-composition
foldl_foldr f z l = foldr (.>) id (foldr (\x -> (flip f x :)) [] l) z
-- f x .> (f y .> (f z .> id)) rs = f z (f y (f x rs)) -- .> quite not lazy
-- pre-composition = mieux que remplacement des ctors
foldr_foldr f z l = foldr (.) id (foldr (\x -> (f x :)) [] l) z
foldl_foldl f z l = foldl (.) id (foldl (\rl x -> flip f x : rl) [] l) z
foldr_foldl f z l = foldl (.>) id (foldl (\rl x -> f x : rl) [] l) z
(.>) :: (a -> b) -> (b -> c) -> (a -> c)
f .> g = g . f
-- >>> foldl (+) 0 [1, 2, 3]
-- >>> foldr (+) 0 [1, 2, 3]
-- >>> foldl_foldr (+) 0 [1, 2, 3]
-- >>> foldr_foldr (+) 0 [1, 2, 3]
-- >>> foldl_foldl (+) 0 [1, 2, 3]
-- >>> foldr_foldl (+) 0 [1, 2, 3]
-- 6
-- 6
-- 6
-- 6
-- 6
-- 6
-- >>> foldl (flip (:)) [] [1, 2, 3]
-- >>> foldl_foldr (flip (:)) [] [1, 2, 3]
-- >>> foldl_foldl (flip (:)) [] [1, 2, 3]
-- [3,2,1]
-- [3,2,1]
-- [3,2,1]
-- >>> foldr (:) [] [1, 2, 3]
-- >>> foldr_foldr (:) [] [1, 2, 3]
-- >>> foldr_foldl (:) [] [1, 2, 3]
-- [1,2,3]
-- [1,2,3]
-- [1,2,3]
-- >>> take 5 (map (+1) [1..])
-- >>> take 5 (foldr ((:) . (+1)) [] [1..])
-- >>> take 5 (foldr_foldr ((:) . (+1)) [] [1..])
-- [2,3,4,5,6]
-- [2,3,4,5,6]
-- [2,3,4,5,6]
-- >>> take 5 (foldr_foldl ((:) . (+1)) [] [1..]) -- might take some time
-- ProgressCancelledException
-- >>> take 5 (foldl_foldr (flip ((:) . (+ 1))) [] [1 ..]) -- better but still slow
-- ProgressCancelledException
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment