[Haskell-cafe] Re: Why does `flip` cause function type so different ?

[Maciej Piechotka]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: This is a digitally signed message part
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20100318/71097065/attachment.bin