Why `\ x & # 8594; fxx` = `join f`?

I recently learned what pointfree is for \x -> f x x join f, and wanted to understand why. I started here:

join :: Monad m => m (m a) -> m a

then got a dead end because I am not familiar with the "monad function". Can someone help me with a type of inference that explains equality?

+4
source share
3 answers

This is a fairly simple algebraic transformation Monad ((->) r)at the type level. See how we specialize and simplify the type join.

join :: Monad m => m        (m        a)  -> m        a
join ::            ((->) r) (((->) r) a)  -> ((->) r) a  -- Specializing
join ::            (r ->    (r ->     a)) -> (r ->    a) -- Infix
join ::            (r ->     r ->     a)  -> r  ->    a  -- Simplifying
+6
source

x -> m join, (x -> x -> a) -> x -> a. f (, , x -> x -> a x a), x -> a, \x -> f x x.

+3

there is no deep insight here, but a mechanical explanation.

instance Monad ((->) r) where
    f >>= k = \ r -> k (f r) r

where join is defined as

join f = f >>= id

substituting definition

join f = \x -> id (f x) x
       = \x -> f x x
+3
source

Source: https://habr.com/ru/post/1648037/


All Articles