[Haskell-cafe] Pretty little definitions of left and right folds
Luke Palmer
lrpalmer at gmail.com
Sat Jun 21 22:17:51 EDT 2008
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
>
More information about the Haskell-Cafe
mailing list