Как Haskell выполняет бета-преобразование для получения типа?

Вывод типа — дело механическое.^(*) Суть в том, что стрелка функции -> на самом деле является здесь бинарным оператором, ассоциированным справа (пока приложение/сопоставление ассоциируется слева).

Таким образом, A -> B -> C на самом деле A -> (B -> C) на самом деле (->) A ((->) B C) на самом деле ((->) A) (((->) B) C). В этой форме ясно, что он состоит из двух частей, поэтому может совпадать, например, с f t, отмечая эквивалентности f ~ ((->) A) и t ~ (((->) B) C) (или в псевдокоде f ~ (A ->), а также t ~ (B -> C) в обычной записи).

При применении терминов двух типов выполняется структурное объединение. Сопоставляются структуры двух терминов, сопоставляются их части, а результирующие эквивалентности отмечаются как подстановки (... ~ ...), доступные для выполнения и обеспечивающие дальнейшие упрощения результирующих типовых терминов (и если некоторая несовместимость должна была быть устранена). обнаружен таким образом, тип будет отклонен).

Это следует общему правилу вывода структуры/типа, основанному на логическом правиле Modus Ponens:

      A -> B     C
     --------------
           B         , where   A ~ C

И поэтому,

liftA2 :: A f =>       (   a     -> b   -> c  ) -> f      a         -> f b -> f c
       (<$>) :: F h =>  (d -> e) -> h d -> h e
             (,) ::                                s -> (t -> (s, t))
---------------------------------------------------------------------------------
liftA2 (<$>) (,) ::                                                    f b -> f c
---------------------------------------------------------------------------------
                                  b ~ h d         f ~ (s->)
                        a ~ d->e         c ~ h e        a ~ t->(s,t)
                           \_ _ _ _ _ _ _ _ _ _ _ _ _ _ a ~ d->e
                       ----------------------------------------------------
                                                          d ~ t   e ~ (s,t)

liftA2 (<$>) (,) ::         f     b    -> f     c       
                  ~         (s -> b  ) -> (s -> c      )
                  ~  F h => (s -> h d) -> (s -> h e    )
                  ~  F h => (s -> h t) -> (s -> h (s,t))

(написание A вместо Applicative и F вместо Functor в качестве сокращения). Подстановки прекращаются, когда больше нет переменных типа для замены.

Существует некоторая свобода выбора каких переменных типов для замены на каждом шаге, но результирующие термины в любом случае будут эквивалентны вплоть до последовательного переименования переменных типов. Например, мы могли бы выбрать

                  ~  F h => (s -> h d) -> (s -> h e    )
                  ~  F h => (s -> h d) -> (s -> h (s,t))
                  ~  F h => (s -> h d) -> (s -> h (s,d))

В процессе было обнаружено ограничение Applicative ((->) s). Это проверяется, так как этот экземпляр существует для всех s. Мы можем увидеть это, набрав :i Applicative в командной строке GHCi. Просматривая список экземпляров, которые он печатает, мы находим instance Applicative ((->) a) -- Defined in `Control.Applicative'.

Если бы такого экземпляра не было, создание типа остановилось бы и сообщило об ошибке, а не просто пропустило бы ее. Но поскольку ограничение сохраняется, оно просто исчезает, поскольку не ограничивает производный тип Functor h => (s -> h t) -> (s -> h (s,t)). Оно уже запеклось.

Экземпляр определяет (f <*> g) x = f x $ g x, но само определение не требуется для производных типов, только тот факт, что оно существует. Что касается liftA2, то он определяется как

liftA2 h f g x = (h <$> f <*> g) x   -- for any Applicative (sans the `x`)
               = (h  .  f <*> g) x   -- for functions
               = (h . f) x (g x)
               = f x `h` g x         -- just another combinator

(да, (<*>) = liftA2 ($) ), так что

liftA2 (<$>) (,) g s = (,) s <$> g s
                     = do { r <- g s       -- in pseudocode, with
                          ; return (s, r)  --  "Functorial" Do
                          }

Или другими словами, liftA2 (<$>) (,) = \ g s -> (s ,) <$> g s.

С типом Functor m => (s -> m t) -> s -> m (s,t). Что является тем, что мы получили.

^(*) См. также:

• Haskell: как определить тип выражения вручную