Как я могу получить тип (последовательность.). БПМЖ?

Question

Я пытаюсь понять, как работает логический вывод и система типов в Haskell. Сейчас я изучаю случай (sequence .) . fmap. Я получаю типы (sequence .) и (. fmap), как это делает haskell:

(.)      ::                             (b -> c) -> (a -> b) -> a -> c
fmap     :: Functor f                => (a -> b) -> f a -> f b
sequence :: (Traversable t, Monad m) => t (m a)  -> m (t a)

-- Type for . fmap:
a ~ (a -> b)
b ~ (f a -> f b)
. fmap              :: ((f a -> f b) -> c) -> ((a -> b) -> c)

-- Type for sequence:
b ~ t (m a1)
c ~ m (t a2)
sequence .          :: (a1 -> t (m a2)) -> (a1 -> m (t a2))

Но тогда я не могу получить тип (sequence .) . fmap. Я попробовал следующие шаги, а затем застрял:

(sequence .) . fmap - ?

f a ~ a1
f b ~ t (m a2)
b ~ m a2
c ~ (a1 -> m (t a2))
(sequence .) . fmap :: (a -> m a2) -> (a1 -> m (t a2))

Тип, который у меня есть, отличается от типа, который дает haskell.

UPD Благодаря @WillemVanOnsem, у меня есть некоторый прогресс, но потом снова застрял ...

(.)    ::              (b -> c) -> (a -> b) -> a -> c
(fmap) :: Functor f => (z -> u) -> f z -> f u
sequence .          :: (a1 -> t (m a2)) -> (a1 -> m (t a2))

b ~ (a1 -> t (m a2))
c ~ (a1 -> m (t a2))
a ~ (z -> u)
(sequence .) . fmap :: ((a1 -> t (m a2)) -> (a1 -> m (t a2))) ->
                       ((z -> u) -> (a1 -> t (m a2))) ->
                       ((z -> u) -> (a1 -> m (t a2))

Answer 1

Давайте сохраним все переменные нашего типа.

(.)      ::                             (b -> c) -> (a -> b) -> a -> c
fmap     :: Functor f                => (u -> v) -> f u -> f v
sequence :: (Traversable t, Monad m) => t (m x)  -> m (t x)

У нас есть два варианта использования функции .. Я буду использовать a1 и т.п. для первого, и a2 и т.п. для второго.

В (sequence .) у нас есть (b1 -> c1) = (t (m x) -> m (t x)), поэтому b1 = t (m x) и c1 = m (t x). Используя подстановку, . специализируется на (t (m x) -> m (t x)) -> (a1 -> t (m x)) -> a1 -> m (t x), а после применения к sequence у нас есть термин типа (a1 -> t (m x)) -> a1 -> m (t x).

Теперь мы можем посмотреть на второе ., (sequence .) . fmap. Здесь у нас есть (b2 -> c2) = (a1 -> t (m x)) -> a1 -> m (t x) и (a2 -> b2) = (u -> v) -> f u -> f v.

Это означает, что:

b2 = a1 -> t (m x)
c2 = a1 -> m (t x)
a2 = (u -> v)
b2 = f u -> f v

Обратите внимание, что у нас есть b2 там дважды, что означает, что a1 = f u и t (m x) = f v, поэтому мы можем также получить это f = t, v = m x.

Теперь, когда мы знаем все эти типы, мы знаем, что второй . специализирован для

((t u -> t (m x)) -> (t u -> m (t x)) 
  -> ((u -> m x) -> (t u -> t (m x))) 
  -> (u -> m x) 
  -> (t u -> m (t x))

Но мы уже применили оба аргумента ., поэтому тип всего выражения: (u -> m x) -> (t u -> m (t x)).

И оттуда, это просто переименование переменных, ограничения и скобки от того, что дает мне ghci.

> :t (sequence .) . fmap
(sequence .) . fmap
  :: (Monad m, Traversable t) => (a1 -> m a) -> t a1 -> m (t a)