Those particular papers? Maybe not. Papers like them? Absolutely.
Joel's challenge is a trivial example of recursion. It's just using foldr (http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v%3Afoldr) to fold a list, mapping (^2) over it first. Thus: foldr (+) 0 . map (^2) which can be reduced to foldr ((+) . (^2)) 0. But the real questions are: why is it valid to combine the map in that way? and, critically, why does foldr have the type that it does? Both of these are very real questions about recursion. Solving Joel's problem isn't hard, knowing why the solution looks the way it does is vastly more important.
Lists are the simplest variety of recursion worth discussing (well, Peano integers are simpler) and so they often elide important issues that you encounter with non-linear recursion. Consider this challenge: You have binary trees data Tree a = Leaf a | Branch (Tree a) (Tree a), write the version of foldr for this data type so someone else could use it to define sumOfSquares using only addition, function composition, and squaring. Since addition is a monoid it would be easy to get this wrong, so make sure it could also be used to define toList :: Tree a -> List a using only cons and nil, retaining the order of the leaves. [You can use list concatenation too, but that can be easily defined in terms of list's foldr, see how? Using list concatenation results in O(n^2) complexity, but you can do a continuation-passing transformation for where you'd want to use it, to get it back to O(n).] If you can solve this one without breaking a sweat, then writing a foldr (aka catamorphism (http://knol.google.com/k/edward-kmett/catamorphisms/3qi7x2qrdushx/2#), aka bananna brackets) for bushes (data Bush a = Leaf a | Branch (Bush (Bush a)) (Bush (Bush a))) shouldn't be too hard, despite the non-uniform recursion.
Once you've seen all of these and the catamorphisms for other recursive data types, it should become clear how we can generalize them all into a single function cata (http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Morphism-Cata.html) which takes an F-algebra (phi :: f a -> a) and returns a function to fold the least-fixed-point (using the isorecursive (http://en.wikipedia.org/wiki/Recursive_type#Isorecursive_types) definition) of a functor (some type constructor f which has a version of map :: forall a b. (a -> b) -> (f a -> f b) defined). The generalization to cata isn't necessary to have a decent grasp of recursion, but it is really helpful. Here (http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf) is a very readable paper applying that category-theoretic treatment to the problem of defining extensible unions in a System-Fw typed language. Eventually I'll write up a version of my masters thesis as a journal article. The encoding we use for Dyna's Prolog-like terms is a hybridization of Swierstra's paper and this one (http://web.cecs.pdx.edu/~sheard/papers/generic.ps) by Tim Sheard. Tim is big on metaprogramming so his paper is higher-level than what I'd call a necessary understanding of recursion, but the two-level types idea —like the coproduct types of Swierstra— are tools that every programmer should have in their repertoire.
While the category theory jargon may be rocket surgery, I really don't think any of the rest of this stuff is.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
chiming
no subject
Date: 2009-01-08 12:19 am (UTC)From:Joel's challenge is a trivial example of recursion. It's just using foldr (http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v%3Afoldr) to fold a list, mapping (^2) over it first. Thus:
foldr (+) 0 . map (^2)which can be reduced tofoldr ((+) . (^2)) 0. But the real questions are: why is it valid to combine the map in that way? and, critically, why does foldr have the type that it does? Both of these are very real questions about recursion. Solving Joel's problem isn't hard, knowing why the solution looks the way it does is vastly more important.Lists are the simplest variety of recursion worth discussing (well, Peano integers are simpler) and so they often elide important issues that you encounter with non-linear recursion. Consider this challenge: You have binary trees
data Tree a = Leaf a | Branch (Tree a) (Tree a), write the version of foldr for this data type so someone else could use it to define sumOfSquares using only addition, function composition, and squaring. Since addition is a monoid it would be easy to get this wrong, so make sure it could also be used to definetoList :: Tree a -> List ausing only cons and nil, retaining the order of the leaves. [You can use list concatenation too, but that can be easily defined in terms of list's foldr, see how? Using list concatenation results in O(n^2) complexity, but you can do a continuation-passing transformation for where you'd want to use it, to get it back to O(n).] If you can solve this one without breaking a sweat, then writing a foldr (aka catamorphism (http://knol.google.com/k/edward-kmett/catamorphisms/3qi7x2qrdushx/2#), aka bananna brackets) for bushes (data Bush a = Leaf a | Branch (Bush (Bush a)) (Bush (Bush a))) shouldn't be too hard, despite the non-uniform recursion.Once you've seen all of these and the catamorphisms for other recursive data types, it should become clear how we can generalize them all into a single function cata (http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Morphism-Cata.html) which takes an F-algebra (
phi :: f a -> a) and returns a function to fold the least-fixed-point (using the isorecursive (http://en.wikipedia.org/wiki/Recursive_type#Isorecursive_types) definition) of a functor (some type constructorfwhich has a version ofmap :: forall a b. (a -> b) -> (f a -> f b)defined). The generalization tocataisn't necessary to have a decent grasp of recursion, but it is really helpful. Here (http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf) is a very readable paper applying that category-theoretic treatment to the problem of defining extensible unions in a System-Fw typed language. Eventually I'll write up a version of my masters thesis as a journal article. The encoding we use for Dyna's Prolog-like terms is a hybridization of Swierstra's paper and this one (http://web.cecs.pdx.edu/~sheard/papers/generic.ps) by Tim Sheard. Tim is big on metaprogramming so his paper is higher-level than what I'd call a necessary understanding of recursion, but the two-level types idea —like the coproduct types of Swierstra— are tools that every programmer should have in their repertoire.While the category theory jargon may be rocket surgery, I really don't think any of the rest of this stuff is.