[Haskell-cafe] Pretty little definitions of left and right folds

[Luke Palmer]

On Sat, Jun 21, 2008 at 7:11 PM, Brent Yorgey <byorgey at seas.upenn.edu> wrote:
> First, given finite sets A (representing an 'alphabet') and S
> (representing 'states'), we can describe a finite state machine by a
> function phi : A x S -> S, which gives 'transition rules' giving a new
> state for each combination of alphabet character and state.  If we
> squint and wave our hands and ignore the fact that types aren't
> exactly sets, and most of the types we care about have infinitely many
> values, this is very much like the Haskell type (a,s) -> s, or
> (curried) a -> s -> s, i.e. a -> (s -> s).  So we can think of a
> Haskell function phi :: a -> (s -> s) as a sort of 'state machine'.
>
> Also, for a monoid M and set S, an action of M on S is given by a
> function f : M x S -> S for which
>
>  (1)  f(1,s) = s, and
>  (2)  f(mn,s) = f(m,f(n,s)).
>
> Of course, in Haskell we would write f :: m -> (s -> s), and we would
> write criteria (1) and (2) as
>
>  (1)  f mempty = id
>  (2)  f (m `mappend` n) = f m . f n
>
> Now look at the type of foldright:
>
>  foldright :: (a -> (s -> s)) -> ([a] -> (s -> s))

Wow!  I commend you on this excellent, enlightening post!

Luke

> We can see that foldright exactly corresponds to the observation that
> any state machine with alphabet a and states s induces a monoid action
> on s by the free monoid [a].  It's not hard to check that the
> function produced by foldright indeed satisfies the requirements to be
> a monoid action.
>
> First, recall that
>
>  foldright f = chain where
>      chain (a:as) = (f a).(chain as)
>      chain _ = id
>
> Now, we can easily prove (1):
>
>  (foldright f) []
> = chain []
> = id
>
> The proof of (2) is by induction on the length of m. The base case is
> obvious, given the proof of (1).
>
>  (foldright f) (m ++ n)
> =                          { defn. of foldright, assume m = x:xs }
>  chain ((x:xs) ++ n)
> =                          { defn. of (++) }
>  chain (x:(xs ++ n))
> =                          { defn. of chain }
>  f x . chain (xs ++ n)
> =                          { inductive hypothesis }
>  f x . chain xs . chain n
> =                          { defn. of chain, associativity of (.) }
>  chain (x:xs) . chain n
> =                          { defn. of foldright, m }
>  (foldright f) m . (foldright f) n
>
>
> How'd I do?  I'm still trying to figure out how the generalization to
> Traversable fits in here.  I'm guessing this is where the monoid
> homomorphisms come in.
>
> -Brent
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>