On Thu, 2010-03-18 at 20:34 -0700, zaxis wrote:
let f x xs = [x:xs,xs] :t f f :: a -> [a] -> [[a]]
:t (>>=) .f (>>=) .f :: a -> ([[a]] -> [a] -> b) -> [a] -> b
Hmm. You seems to have defined Monad ((->) a). (>>=) . f == \x -> (>>=) (f x) == \x -> (f x >>=) 1. x :: ∀ a. a from type of f 2. f :: ∀ a. a -> [a] -> [[a]] 3. (>>=) :: ∀ m a b. m a -> (a -> m b) -> m b From which follows: 4. (>>=) :: ∀ m b c. Monad m => m b -> (b -> m c) -> m c (from 3) 5. f x :: ∀ a. [a] -> [[a]] (from 1 and 2) 6. (>>=) :: ∀ a c. ([a] -> [[a]]) -> ([[a]] -> [a] -> c) -> ([a] -> c) If it works for all m b c (4) it works for m := [a] -> b := [[a]] 7. (f x >>=) :: ∀ a c. ([[a]] -> [a] -> c) -> ([a] -> c) From 6. Simply substituting first argument 8. \x -> (f x >>=) :: ∀ a. a -> ([[a]] -> [a] -> c) -> ([a] -> c) If you know first-order logic I guess you can see the pattern.
:t (flip (>>=) .f) (flip (>>=) .f) :: a -> [[a]] -> [[a]]
Note that list ([] a == [a]) is monad. :t flip (>>=) flip (>>=) :: (Monad m) => (a -> m b) -> m a -> m b (flip (>>=) .f) == \x -> flip (>>=) (f x) == \x y -> y >>= f x 1. x :: ∀ a. a from type of f 2. f :: ∀ a. a -> [a] -> [[a]] 3. (>>=) :: ∀ m a b. m a -> (a -> m b) -> m b From which follows 4. (>>=) :: ∀ m b c. Monad m => m b -> (b -> m c) -> m c (from 3) 5. f x :: ∀ a. [a] -> [[a]] (from 1 and 2) 6. (>>=) :: ∀ a. [[a]] -> ([a] -> [[a]]) -> [[a]] From 4 for m := [] b := [a] c := [a] 7. (>>= f x) :: ∀ a. [[a]] -> [[a]] From 6 (inserting second argument) 8. y :: ∀ a. [[a]] (forced by 7) 9. y >>= f x :: ∀ a. [[a]] (7 and 8) 10. \x y -> y >>= f x :: ∀ a. a -> [[a]] -> [[a]] (1, 8 and 9) While far from rigours proof I hope it gives some gasp of what's going on. I hope it was helpful Regards