On 5/22/12 11:13 AM, John Simon wrote:
- Is `case _ of x:xs -> x:xsr where xsr = something xs` a common
idiom? It happened twice in my code, and it seems odd to split the
first element away from the rest of the list as it's processed.
I don't know how common it is in practice, but that's fmap for the
PreList functor. Allow me to explain...
(tl;dr: there's some non-trivial theoretical backing, if you're
interested in recursion theory. Though again, I'm not sure how often it
actually comes up for lists.)
Here's the list type, if we defined it ourselves:
data List a = Nil | Cons a (List a)
Like other recursive types, we can decompose this into a non-recursive
type plus a generic version of recursion:
data Fix f = MkFix (f (Fix f))
-- N.B., MkFix :: f (Fix f) -> Fix f
data PreList a recurse = PreNil | PreCons a recurse
type List' a = Fix (PreList a)
The new List' is essentially the same as the old List:
to :: List a -> List' a
to Nil = Fix PreNil
to (Cons x xs) = Fix (PreCons x (to xs))
fro :: List' a -> List a
fro (MkFix PreNil) = Nil
fro (MkFix (PreCons x xs)) = Cons x (fro xs)
-- and we can prove:
-- > to . fro == id
-- > fro . to == id
There's a whole bunch of other machinery that comes from this
perspective, but the important thing is that it all depends on the fact
that PreList is a functor in a very specific way, namely that it applies
the function to all the recursion sites (i.e., "one level down" if we're
thinking of the fixed-point version):
instance Functor (PreList a) where
fmap f PreNil = PreNil
fmap f (PreCons x xs) = PreCons x (f xs)
Of course, Fix(PreList a) ---aka List a--- has its own functor instance,
but that's unrelated.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
