Каким образом (fmap.fmap) суммируется проверка типа [1,2,3] в Haskell?

Question

Я не понимаю, как этот простой тип выражения проверяется в Haskell

(fmap.fmap) sum Just [1, 2, 3]

Тип для композиции fmaps:

fmap.fmap
  :: (Functor f1, Functor f) => (a -> b) -> f (f1 a) -> f (f1 b)

, поэтому я ожидал f1 ~ List и f ~ Maybe, что подразумевает, что тип функции должен быть Integer -> b. Но если проверить тип в ghci, я получу:

t (fmap.fmap) _ Just [1, 2, 3]

<interactive>:1:13: error:
    • Found hole: _ :: [Integer] -> b
      Where: ‘b’ is a rigid type variable bound by
               the inferred type of it :: Maybe b at <interactive>:1:1
    • In the first argument of ‘fmap . fmap’, namely ‘_’
      In the expression: (fmap . fmap) _ Just [1, 2, 3]

Я вижу, что ghci определяет тип функции как [Integer] -> b. Как это возможно?

Answer 1

Нет оснований ожидать f1 ~ [] и f ~ Maybe. Обратите внимание, что вам нужно Just :: f (f1 a). Мы знаем Just :: a -> Maybe a. Поэтому на самом деле f ~ (->) a и f1 ~ Maybe. Тогда у вас есть

fmap . fmap :: (a -> b) -> (a -> Maybe a) -> a -> Maybe b
--             ^^sum^^^    ^^^^^Just^^^^^    ^ [1, 2, 3]

Поскольку мы знаем, что [1, 2, 3] :: a, мы можем вывести a ~ [Integer] сейчас (по умолчанию тип Num eri c равен Integer).

fmap . fmap :: ([Integer] -> b) -> ([Integer] -> Maybe [Integer]) -> [Integer] -> Maybe b

Answer 2

Для потомков, вот совет, как вы можете выяснить такие вещи в будущем. Вы можете задать тип подвыражения в ghci, используя подстановочный знак (если у вас не включен PartialTypeSignatures).

:t ((fmap :: _) . (fmap :: _)) sum Just [1, 2, 3]

Это говорит о том, что внешний тип fmap используется в типе (a1 -> b) -> ([a] -> a1) -> [a] -> b, а внутренний используется с типом (a1 -> b) -> Maybe a1 -> Maybe b. Должно быть ясно, что внутренний fmap просто действует на Maybe. Внешний fmap на первый взгляд выглядит более сложным, но это экземпляр типа (.), который равен fmap в функторе чтения функций.

(.)  :: ( y -> z) -> (  x ->  y) ->   x -> z
fmap :: (a1 -> b) -> ([a] -> a1) -> [a] -> b

x ~ [a]
y ~ a1
z ~ b

Функтор здесь ([a] ->), пишется (->) [a] в реальном коде, потому что Haskell не позволяет разделы оператора на уровне типа.

Это говорит о том, что внешний является (.), и оттуда вы можете встроить определения шаг за шагом, чтобы увидеть, как это оценивается.

(fmap . fmap) sum Just [1, 2, 3]
fmap (fmap sum) Just [1, 2, 3]
(.) (fmap sum) Just [1, 2, 3]
(fmap sum . Just) [1, 2, 3]
fmap sum (Just [1, 2, 3])

Чтобы уменьшить шум и избежать необходимости манипулировать таким количеством переменных типа, чтобы определить, какие из них актуальны, вы можете исправить некоторые типы с помощью сигнатур типов, здесь Int вместо Num a => a.

:t ((fmap :: _) . (fmap :: _)) sum Just [1 :: Int, 2, 3]

Это дает (a -> b) -> ([Int] -> a) -> [Int] -> b для внешнего fmap в функторе (->) [Int] и (a -> b) -> Maybe a -> Maybe b для внутреннего fmap в Maybe.

И ради развлечения, вы можете заменить (.) на fmap!

fmap fmap fmap sum Just [1, 2, 3]