On Sat, Jun 21, 2008 at 7:11 PM, Brent Yorgey
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe