Короче говоря: из-за вывода типа Haskell знает, что m и f на самом деле являются частично конкретизированной стрелкой.

Получение типа

Что ж, давайте посчитаем. Функция join . (flip fmap) в основном является вашим заданным лямбда-выражением \x -> join . x с аргументом (flip fmap), поэтому:

h = (\x -> join . x) (flip fmap)

Теперь лямбда-выражение имеет тип:

(\x -> join . x) :: Monad m =>   (a -> m (m b)) -> (a -> m b)

Теперь аргумент flip fmap имеет тип:

flip fmap        :: Functor f => f c -> ((c -> d) -> f d)

(здесь мы используем c и d вместо a и b, чтобы избежать путаницы между двумя возможно разными типами).

Это означает, что тип flip fmap совпадает с типом аргумента лямбда-выражения, поэтому мы знаем, что:

  Monad m =>   a   -> m (m b)
~ Functor f => f c -> ((c -> d) -> f d)
---------------------------------------
a ~ f c, m (m b) ~ ((c -> d) -> f d)

Итак, теперь мы знаем, что a имеет тот же тип, что и f c (это значение тильды ~).

Но мы должны сделать некоторые дополнительные вычисления:

  Monad m =>   m (m b)
~ Functor f => ((c -> d) -> f d)
--------------------------------
m ~ (->) (c -> d), m b ~ f d

Следовательно, мы знаем, что m совпадает с (->) (c -> d) (по сути, это функция, в которой мы знаем тип ввода, здесь (c -> d), а тип вывода — это параметр типа m.

Итак, это означает, что m b ~ (c -> d) -> b ~ f d, значит, это означает, что f ~ (->) (c -> d) и b ~ d. Дополнительным следствием является то, что начиная с a ~ f c мы знаем, что a ~ (c -> d) -> c

Итак, чтобы перечислить, что мы получили:

f ~ m
m ~ (->) (c -> d)
b ~ d
a ~ (c -> d) -> c

Итак, теперь мы можем «специализировать» типы как нашего лямбда-выражения, так и нашей функции flip fmap:

(\x -> join . x)
    :: (((c -> d) -> c) -> (c -> d) -> (c -> d) -> d) -> ((c -> d) -> c) -> (c -> d) -> d
flip fmap
    ::  ((c -> d) -> c) -> (c -> d) -> (c -> d) -> d

а тип flip fmap теперь идеально совпадает с типом аргумента лямбда-выражения. Таким образом, тип (\x -> join . x) (flip fmap) является типом результата типа лямбда-выражения, а именно:

(\x -> join . x) (flip fmap)
    :: ((c -> d) -> c) -> (c -> d) -> d

Но сейчас мы конечно еще не получили реализацию этой функции. Однако мы уже на шаг впереди.

Получение реализации

Поскольку теперь мы знаем, что m ~ (->) (c -> d), мы знаем, что должны искать экземпляр стрелки монады:

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

Таким образом, для заданной функции f :: r -> a в качестве левого операнда и функции k :: a -> (r -> b) ~ a -> r -> b в качестве операнда мы создаем новую функцию, которая отображает переменную x в k, применяемую к f, применяемую к x, и x. Таким образом, это способ выполнить своего рода предварительную обработку входной переменной x, а затем выполнить обработку с учетом предварительной обработки и исходного представления (хорошо, это эта интерпретация, которую может использовать читатель-человек). ).

Теперь join :: Monad m => m (m a) -> m a реализован как:

-- specialized for `m ~ (->) a
join f = \r -> id (f r) r

Поскольку id :: a -> a (функция тождества) возвращает свой аргумент, мы можем упростить его до:

-- specialized for `m ~ (->) a
join f = \r -> (f r) r

-- specialized for `m ~ (->) a
join f x = f x x

Кроме того, мы знаем, что экземпляр Functor для типа стрелки определяется как:

instance Functor ((->) r) where
    fmap = (.)

Таким образом, он в основном используется как «постпроцессор» для результата функции: мы создаем новую функцию, которая будет выполнять постобработку с данной функцией.

Итак, теперь, когда мы достаточно настроили функцию для данного Functor/Monad, мы можем получить реализацию как:

-- alternative implementation
h = (.) (\f x -> f x x) (flip (.))

или используя больше лямбда-выражений:

h = \a -> (\f x -> f x x) ((flip (.)) a)

которые мы можем теперь дополнительно специализировать как:

h = \a -> (\f x -> f x x) ((\y z -> z . y) a)

-- apply a in the lambda expression
h = \a -> (\f x -> f x x) (\z -> z . a)

-- apply (\z -> z . a) in the first lambda expression
h = \a -> (\x -> (\z -> z . a) x x)

-- cleaning syntax
h a = (\x -> (\z -> z . a) x x)

-- cleaning syntax
h a x = (\z -> z . a) x x

-- apply lambda expression
h a x = (x . a) x

-- remove the (.) part
h a x = x (a x)

Таким образом, h в основном принимает два аргумента: a и x, затем выполняет приложение функции с a в качестве функции и x в качестве параметра, а вывод снова передается в функцию x.

Пример использования

В качестве примера использования вы используете:

h (\f -> f u) (\x -> x + v)

или лучше:

h (\f -> f u) (+v)

поэтому мы можем проанализировать это следующим образом:

   h (\f -> f u) (+v)
-> (+v) ((\f -> f u) (+v))
-> (+v) ((+v) u)
-> (+v) (u+v)
-> ((u+v)+v)

Итак, мы добавляем u+v к v.

Типы выстраиваются проще с >>>:

                          a   ->     b                       >>>
                                     b              -> c     ::
                          a   ->                       c   

Здесь у нас есть

join . flip fmap  ==  flip fmap >>> join

flip fmap :: Functor f => f a -> ((a -> b) -> f b )
join      :: Monad   m =>        (m          (m b)) -> m b
----------------------------------------------------------
flip fmap >>> join ::
 (Functor f, Monad m) =>  f a  ->                      m b   , ((a -> b) ->) ~ m, f ~ m
                   ::
 (Functor f, Monad f) =>  f a  ->                      f b   , f ~ ((a -> b) ->)
                   ::    ((a -> b) -> a) -> ((a -> b) -> b)

Простой, механический, обыденный.

Чтобы увидеть, что он делает, проще всего повозиться с определениями комбинаторного стиля,

(join . flip fmap) f g x =
 join (flip fmap f) g x =          -- join f x = f x x
 (`fmap` f) g g x =                -- f `fmap` g = f . g
 (g . f) g x 
 g (f g) x 

Так что x нам все-таки не нужен (или нужен?). Определения функций join и fmap даны на полях. Мы прибыли в

(join . flip fmap) f g = g (f g)   -- f :: (a -> b) -> a,  g :: a -> b 
                                   -- f g :: a  , g (f g) :: b

Другой способ — исходить из типов, руководствуясь правилом modus ponens,

            ((a -> b) -> a)    (a -> b)        --       f  g
            ---------------------------
(a -> b)                 a                     --  g   (f  g)
---------------------------------------
      b