Блог

 nestedApply :: (Applicative f, Applicative g) => g (f (a -> b)) -> f a -> g (f b)
 

Как указывает тип, как это (a->b) применить к этому a в контексте f ?

Спасибо за помощь.

Это один из тех случаев, когда полезно сосредоточиться на типах. Я постараюсь сделать это простым и объясню причины.

Давайте начнем с описания задачи. У нас есть gfab :: g(f(a->b)) и fa :: f a , и мы хотим иметь g(f b) .

 gfab :: g (f (a -> b))
fa   :: f a
??1  :: g (f b)
 

Поскольку g это функтор, для получения типа g T мы можем начать со значения ??2 типа g U и применить fmap к ??3 :: U -> T нему . В нашем случае у нас есть T = f b , поэтому мы ищем:

 gfab :: g (f (a -> b))
fa   :: f a
??2  :: g U
??3  :: U -> f b
??1 = fmap ??3 ??2  :: g (f b)
 

Теперь, похоже, нам следует выбрать ??2 = gfab . В конце концов,это единственное значение типа g Something , которое у нас есть. Мы получаем U = f (a -> b) .

 gfab :: g (f (a -> b))
fa   :: f a
??3  :: f (a -> b) -> f b
??1 = fmap ??3 gfab :: g (f b)
 

Давайте превратим ??3 в лямбду, (x :: f (a->b)) -> ??4 с. ??4 :: f b (Тип x можно опустить, но я решил добавить его, чтобы объяснить, что происходит)

 gfab :: g (f (a -> b))
fa   :: f a
??4  :: f b
??1 = fmap ( (x :: f (a->b)) -> ??4) gfab :: g (f b)
 

Как создавать ??4 . Ну, у нас есть значения типов f (a->b) и f a , поэтому мы можем <*> их получить f b . Мы, наконец, получаем:

 gfab :: g (f (a -> b))
fa   :: f a
??1 = fmap ( (x :: f (a->b)) -> x <*> fa) gfab :: g (f b)
 

Мы можем просто превратить это в:

 nestedApply gfab fa = fmap (<*> fa) gfab
 

Сейчас это не самый элегантный способ сделать это, но понимание процесса важно.

С

 nestedApply :: (Applicative f, Applicative g) 
            => g (f (a -> b))  
            ->    f  a 
            -> g (f       b )
 

чтобы (a->b) применить это к этому a в контексте f , нам нужно действовать в контексте g .

И это просто fmap .

Это становится яснее с перевернутой подписью, сосредоточив внимание на ее последней части

 flip nestedApply :: (Applicative f, Applicative g) 
            =>    f  a 
            -> g (f (a -> b))     --- from here
            -> g (f       b )     --- to here
 

Итак, что мы имеем здесь, так это

 nestedApply gffun fx = fmap (bar fx) gffun
 

с bar fx применением под g покровом fmap для нас. Который

 bar fx ::         f (a -> b)
            ->    f       b   
 

т.е.

 bar ::            f  a
            ->    f (a -> b)
            ->    f       b   
 

и это просто <*> не так, снова перевернуто. Таким образом, мы получаем ответ,

 nestedApply gffun fx  =  fmap (<*> fx) gffun
 

Как мы видим, используются только fmap возможности g , поэтому нам нужно только

 nestedApply :: (Applicative f, Functor g) => ...
 

в подписи типа.

Это легко, когда пишешь это на листе бумаги, в 2D. Который мы имитируем здесь с диким отступом, чтобы получить это вертикальное выравнивание.

_{Да, мы, люди, научились сначала писать на бумаге, а печатать на пишущей машинке гораздо позже. Последнее поколение или два были вынуждены печатать линейным шрифтом с помощью современных устройств с юных лет, но теперь каракули и разговоры (а также жесты и указывания), надеюсь, снова возьмут верх. Изобретательные режимы ввода в конечном итоге будут включать 3D-рабочие процессы, и это будет определенным прогрессом. 1D плохо, 2D хорошо, 3D лучше. Например, многие диаграммы теории категорий гораздо легче проследить (и, по крайней мере, представить), когда они нарисованы в 3D. Эмпирическое правило таково: это должно быть легко, а не сложно. Если он слишком занят, ему, вероятно, нужно другое измерение.}

Просто играем, соединяем провода под обертками. Несколько самоочевидных диаграмм, и все готово.

Вот вам несколько типов мандал (опять же, перевернутых):

 -- <

gt;               -- <*>               -- =<<

f     a              f     a              f     a

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

f          b         f          b         f    (     f b)   -- fmapped, and

                                          f            b    -- joined

 

и, конечно же, мать всех приложений,
 --      $
      a
      a -> b
           b
 
он же Modus Ponens (да, тоже перевернутый).