Named (custom) recursions vs clever comonadic recursions
Hey all, Today I had a small exchange with another reddit user about CT and why is important to Haskell programming... What I don't get yet (as the subject says) is a real-world example on where you might apply cathegory theory to a recursion. Here is the small thread : fbru02: Sorry for maybe the OT posting but I have a question of my own: While learning Haskell and being a curious procrastinator I started learning Category theory but although I get , I don't get it yet. What I want to ask is practical uses of cathegory theory ? I know that it is used for high availability systems for theoretical proof that a System has the correct side effects. Also I know there are in reality recursions that might need this stuff as they are not as simple as what one would write in a toy project. What are this recursion schemes ?? What other uses there are for CT? nbloomf: Disclaimer- I am only beginning to understand this stuff myself. I am also a mathematician, not a computer scientist or a professional programmer. Two papers that give a good overview of what categories can do are "Functional Programming with Bananas, Lenses, etc." and "Recursion Schemes from Comonads". My understanding of the role of categories in FP (at least partly) is as follows. Arbitrary recursion is very useful to writers of programs. However, like arbitrary GOTOs, it can make it hard to see what's "really" happening in a program. A long time ago people figured out that fold/reduce was a common recursive pattern, but it was generally only used on lists and couldn't express all the recursion people wanted to do. More recently it was discovered that if your language is strongly typed, you can think of the types as objects in a category. Then some type constructors become endofunctors, and the traditional fold can be expressed as a particular map, parameterized by the functor, having a nice universal property. Moreover, as the "Recursion schemes from comonads" paper discusses, by parameterizing on the comonad the fold operator can become several different recursion schemes. This means a much smaller amount of code can express a larger number of ideas- even ideas that haven't been had yet. Moreover, it makes optimizations (such as fold fusion) much more powerful. So the real power of category theory is as a metalanguage- these ideas might never have become "obvious" without the language of functors, algebras, initial objects, and such. fbru02 : thank you for great response. Have you yourself used this parametraizing of the comonad? In which context or solving which problem and why couldn't you solving easily making a normal named recursion :D Thanks a lot ! :D Thanks ! -- Federico Brubacher www.fbrubacher.com Colonial Duty Free Shop www.colonial.com.uy
Federico Brubacher wrote:
What I don't get yet (as the subject says) is a real-world example on where you might apply category theory to a recursion.
In a sense, the core task of the paper "Functional Programming with Bananas, Lenses, etc." is to write a general fold function that works for many data types at once, not just for lists. Here is fold for lists: data ListF a b = Empty | Cons a b foldList :: (ListF a b -> b) -> [a] -> b foldList f = foldr (\a b -> f (Cons a b)) (f Empty) sumList :: [Int] -> Int sumList = foldList f where f Empty = 0 f (Cons x s) = x + s and here is fold for binary trees data Tree a = Leaf a | Node (Tree a) (Tree a) data TreeF a b = Leaf' a | Node' b b foldTree :: (TreeF a b -> b) -> Tree a -> b foldTree f (Leaf x ) = f $ Leaf' x foldTree f (Node u v) = f $ Node' (foldTree f u) (foldTree f v) sumTree :: Tree Int -> Int sumTree = foldTree f where f (Leaf' x ) = x f (Node' s t) = s + t In other words, the fold captures the process of traversing the data structure while the user-supplied function tells it how to calculate the result (without performing recursion itself). Both folds are one and the same function when viewed through the right glasses: data Fix f = In { out :: f (Fix f) } fold :: Functor f => (f b -> b) -> Fix f -> b fold f (In x) = f . fmap (fold f) x type Tree a = Fix (TreeF a) foldTree :: (TreeF a b -> b) -> Tree a -> b foldTree = fold instance Functor (TreeF a) where fmap f (Node' b c) = Node' (f b) (f c) fmap f x = x type List a = Fix (ListF a) foldList :: (ListF a b -> b) -> List a -> b foldList = fold instance Functor (ListF a) where fmap f (Cons a b) = Cons a (f b) fmap f x = x Regards, apfelmus PS: The scary name for "fold" is "catamorhpism"
participants (2)
-
apfelmus -
Federico Brubacher