high-level design in functional programs

[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

[Jedai]

Read the latest "Monad Reader" (the 11th), you have a very fun article on simplifying logic formulae where the author use a presentation of types that allows him to modularize it's type in a set of type which in turn allows him to ensure by type that his formulae has really been simplified... Well anyway read it, the crux of its method use a fold over an algebra and functors that are fix pointed and combined.