Расчет типа `карты. foldr`

Question

map :: (a -> b) -> [a] -> [b]
foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b

Что такое систематический c способ определения типа для map . foldr? Я знаю, как сделать это для map foldr, но запутался, когда дело доходит до композиции.

Спасибо!

Answer 1

Очевидно, что должен быть системный c способ, иначе компилятор Haskell не сможет сделать вывод типа.

Один из способов сделать это самостоятельно - это вставить типы шаг за шагом:

У нас есть следующие типы:

(.) :: (b -> c) -> (a -> b) -> (a -> c)
map :: (a' -> b') -> [a'] -> [b']
foldr :: Foldable t => (a'' -> b'' -> b'') -> b'' -> t a'' -> b''

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

1. поставьте map в (.)

Если мы предоставим универсальную c функцию f в (.), мы получим следующие типы:

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

выберите f будет map:

map :: (a' -> b') -> [a'] -> [b']

равно

map :: (a' -> b') -> ([a'] -> [b'])

, поскольку f имеет тип (b -> c), мы можем заключить:

b :: (a' -> b')
c :: ([a'] -> [b'])

введите наши предполагаемые типы:

(.) f :: (a -> b) -> (a -> c)
(.) map :: (a -> (a' -> b')) -> (a -> ([a'] -> [b']))

мы можем опустить несколько скобок:

(.) map :: (a -> (a' -> b')) -> a -> ([a'] -> [b'])
(.) map :: (a -> (a' -> b')) -> a -> [a'] -> [b']
(.) map :: (a -> a' -> b') -> a -> [a'] -> [b']

2. поставьте foldr в (.) map

Снова начните с замены универсальной c функции g:

(.) map :: (a -> a' -> b') -> a -> [a'] -> [b']
(.) map g :: a -> [a'] -> [b']
g :: (a -> a' -> b')

выберите g равным foldr:

foldr :: Foldable t => (a'' -> b'' -> b'') -> b'' -> t a'' -> b''

равно

foldr :: Foldable t => (a'' -> b'' -> b'') -> b'' -> (t a'' -> b'')

, поскольку g имеет тип (a -> a' -> b'), мы можем сделать вывод:

a :: (a'' -> b'' -> b'')
a' :: b''
b' :: Foldable t => t a'' -> b''

вставить наши предполагаемые типы:

(.) map foldr :: a -> [a'] -> [b']
(.) map foldr :: Foldable t => (a'' -> b'' -> b'') -> [b''] -> [t a'' -> b'']

Какого типа мы получаем при запросе ghci для типа:

> :t ((.) map foldr)
((.) map foldr) :: Foldable t => (a1 -> a2 -> a2) -> [a2] -> [t a1 -> a2]

Answer 2

Хорошо, вместо использования автоматического c метода для вывода типа, который я думал, возможно, вам будет интересен более интуитивный ответ:

Как я уверен, вы знаете, map . foldr - это эквивалентно (\x -> map (foldr x)). Давайте начнем с этого.

Каким должен быть тип x? Ну, поскольку это первый параметр foldr, он должен выглядеть как функция, которая принимает некоторое значение, некоторый аккумулятор и возвращает что-то того же типа, что и аккумулятор (по определению foldr). Таким образом:

x :: (a -> b -> b)

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

После применения (foldr x) мы возвращаем функцию, которая все еще ожидает начальное значение аккумулятора, а затем - любой складываемый тип и возвращает значение того же типа, что и аккумулятор (например, сумма каждого элемента в списке).

Итак, тип (foldr x) должен быть

Foldable t => b -> t a -> b

Хорошо, но мы еще не закончили, посмотрим, что произойдет с использованием map сейчас же.

карта должна сначала получить функцию (по определению). Возвращаемое значение (foldr x) выглядит так, что означает, что это использование карты учитывает, что (b -> t a -> b) является типом функции, которую необходимо применить к каждому элементу списка.

Может быть, это яснее записано как (b -> (t a -> b)). Таким образом, это использование карты предполагает, что ей дана функция, которая принимает некоторый ввод типа b и возвращает функцию, которая сама принимает складную a и возвращает b.

Хорошо, мы почти там. Теперь для map все еще нужен другой аргумент: список, элементы которого имеют тот же тип, что и входные данные функции, к которой она будет применяться. Таким образом, поскольку функция, которую мы хотим применить (результат (foldr x)), принимает b, наше использование карты займет [b].

Итак, теперь у нас есть:

 (a -> b -> b) -> [b] -> …

Нам просто не хватает типа выходного значения этой композиции функций, которая является типом выходного значения этого спецификатора c использование карты. Поскольку функция, применяемая с map, возвращает что-то типа (t a -> b), то список вещей, которые мы, очевидно, вернем, будет иметь тип [t a -> b].

Так что в итоге у вас будет

Foldable t => (a -> b -> b) -> [b] -> [t a -> b]

как тип map . foldr.

Answer 3

map . foldr на самом деле (.) map foldr. Добавляя тип (.) в микс, мы получаем

        foldr :: Foldable t =>           (a -> (r->r)) -> (r -> (t a -> r))
    map :: (i -> j) -> ([i] -> [j])
(.) ::    (   b     ->      c      ) -> (    d         ->     b            ) -> (d -> c)
-----------------------------------------------------------------------------------------
--            4             2                1                3
-----------------------------------------------------------------------------------------
(.) map foldr :: Foldable t =>                                                  (d -> c)
    where                        d ~ a -> (r -> r)       -- 1
                                 c ~ [i] -> [j]          -- 2
                                 b ~ r -> (t a -> r)     -- 3
                                   ~ i ->      j         -- 4
                                 -------------------
                                 i ~ r                   -- 5
                                 j ~       t a -> r      -- 6

, таким образом

map . foldr :: Foldable t => a -> (r -> r) -> [i] -> [j]          -- by 1,2
            ~  Foldable t => a -> (r -> r) -> [r] -> [t a -> r]   -- by 5,6

Здесь мы использовали приложение правило вывода типа,

     f   :: A -> B
       x :: A
    ---------------
     f x ::      B

(также известный как modus ponens в logi c).

Мы также можем использовать правило вывода типа состав , которое является правилом приложения, специализированным для (.) или, что эквивалентно, (>>>) = flip (.):

           g ::      B -> C
     f       :: A -> B
    ------------------------
     f >>> g :: A ->      C
     g  .  f :: A ->      C

Чтобы соответствовать этому шаблону, мы немного по-другому записываем типы и получаем результат немедленно :

          map ::                                (i ->      j    ) -> ([i] -> [    j   ])
foldr         :: Foldable t => (a -> (r->r)) -> (r -> (t a -> r))
------------------------------------------------------------------------------------
foldr >>> map :: Foldable t => (a -> (r->r)) ->                       [r] -> [t a -> r]
map  .  foldr :: Foldable t => (a -> (r->r)) ->                       [r] -> [t a -> r]

Это намного более интуитивно понятно.