1

Пытаюсь понять как работает вывод типа в haskell на конкретном примере, а именно ((sequence .) . fmap). Для упрощения я решил получить типы для отдельных подвыражений - тут всё прошло гладко и я получил такие же типы, что и ghci:

-- Сначала тип для (sequence .):
(.)      :: (b -> c) ->
            (a -> b) -> 
            (a -> c)

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

b ~ t (m a)
c ~ m (t a)

(sequence .)  :: (a1 -> t (m a2)) ->
                 (a1 -> m (t a2))

Всё чётко, такой же тип возвращает и ghci. Теперь определим тип для (sequence .) . aka (.) (sequence .):

(.)           :: (b -> c) ->
                 (a -> b) -> 
                 (a -> c)

(sequence .)  :: (a1 -> t (m a2)) ->
                 (a1 -> m (t a2))

b ~ (a1 -> t (m a2))
c ~ (a1 -> m (t a2))

(.) (sequence .) :: (a -> (a1 -> t (m a2))) ->
                    (a -> (a1 -> m (t a2))) 

Снова всё ок, такой же тип возвращает ghci. Теперь финальная часть, определим тип для (.) (sequence .) (fmap) (для упрощения символы в типе для fmap изменены):

fmap             :: Functor f => (z -> u) -> f z -> f u

(.) (sequence .) :: (a -> (a1 -> t (m a2))) ->
                    (a -> (a1 -> m (t a2))) 

a  ~ (z -> u)
a1 ~ f z
t (m a2) ~ f u

(.) (sequence .) (fmap) :: ((z -> u) -> (f z -> m (t a2))

Полученный тип несколько отличается от возвращаемого ghci:

Prelude Control.Monad> :t (sequence .) . fmap
(sequence .) . fmap
  :: (Traversable t, Monad m) => (a1 -> m a2) -> t a1 -> m (t a2)

Собственно вопрос - почему u ghci раскрыл в m a2? Понятно, что это следует из замены t (m a2) ~ f u Вопрос два - почему f z ghci меняет на t a1 (короче говоря, почему подменяется тип структуры?)

3
  • Из t (m a2) ~ f u следует что t ~ f. На первый вопрос вы сами ответили.
    – talex
    11 янв 2019 в 9:42
  • @talex, просто непонятно, в каком случае мы продолжаем замену, в каком - оставляем как есть. Причём как я думал, замена производится всегда в одном направлении, а здесь мы делаем обратную замену -- u -> (m a2)
    – aryndin
    11 янв 2019 в 9:44
  • Всегда осуществляем. Компилятор придумывает свои имена, но конкретные имена не важны. Важна структура.
    – talex
    11 янв 2019 в 9:45

1 ответ 1

1

Упростим определения до:

foo :: (a -> a1 -> t (m a2)) ->
       (a -> a1 -> m (t a2)) 

fmap :: (z -> u) -> f z -> f u

Теперь рассмотрим как сопостовляются типы при вызове foo fmap

  • a -> a1 -> t (m a2) соответствует (z -> u) -> f z -> f u
  • a соответствует z -> u
  • a1 соответствует f z
  • t (m a2) соответствует f u
    • t соответствует f
    • m a2 соответствует u

Это возможно только если u имеет форму c1 c2. Произведем замену.

fmap :: (z -> с1 с2) -> f z -> f (с1 с2)

Повторим попытку сопоставить.

  • a -> a1 -> t (m a2) соответствует (z -> с1 с2) -> f z -> f (с1 с2)
  • a соответствует z -> с1 с2
  • a1 соответствует f z
  • t (m a2) соответствует f с1 с2
    • t соответствует f
    • m a2 соответствует с1 с2
      • m соответствует c1
      • a2 соответствует c2

Теперь подставим найденные соответствия в оставшуюся не сопоставленой часть foo: a -> a1 -> m (t a2)

  • a заменим на z -> с1 с2: (z -> с1 с2) -> a1 -> m (t a2)
  • a1 заменим на f z: (z -> с1 с2) -> f z -> m (t a2)
  • m заменим на c1: (z -> с1 с2) -> f z -> c1 (t a2)
  • t заменим на f: (z -> с1 с2) -> f z -> c1 (f a2)
  • a2 заменим на c2: (z -> с1 с2) -> f z -> c1 (f c2)

Получим тип структурно эквивалентный тому что требовалось получить: (a1 -> m0 a0) -> t0 a1 -> m0 (t0 a0)

`

Ваш ответ

By clicking “Отправить ответ”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Всё ещё ищете ответ? Посмотрите другие вопросы с метками или задайте свой вопрос.