Почему разница в выводе типа по сравнению с шаблоном as в двух похожих определениях функций? - PullRequest
Новая
       43

Почему разница в выводе типа по сравнению с шаблоном as в двух похожих определениях функций?

26 голосов
/ 30 марта 2019

У меня есть следующие два похожих определения функций: 

left f (Left x) = Left (f x)
left _ (Right x) = Right x

left' f (Left x) = Left (f x)
left' _ r@(Right _) = r

Когда я проверяю сигнатуры типов двух функций, меня смущают следующие типы: 

ghci> :t left
left :: (t -> a) -> Either t b -> Either a b
ghci> :t left'
left' :: (a -> a) -> Either a b -> Either a b

Полагаю, left и left' должны иметь одинаковую сигнатуру типа, но вывод типа haskell дает мне сюрприз.

Я не могу понять, почему сигнатуры типов left и left' отличаются. Кто-нибудь может дать мне некоторую информацию? Спасибо!

Ответы [ 2 ]

25 голосов
/ 30 марта 2019

Во второй строке left': 

left' _ r@(Right _) = r
--      ^^^^^^^^^^^   ^

Поскольку вы используете шаблон as, вам необходимо, чтобы тип ввода был равен типу возвращаемого значения, поскольку очевидно, что это одно и то же значение. Тип left' затем ограничивается чем-то вида a -> b -> b.

Затем это ограничение распространяется в обратном направлении, что, в свою очередь, ограничивает тип функции - надеюсь, вы увидите, как; это не так уж сложно.

Однако во второй строке left вы создаете новое значение 

left _ (Right x) = Right x
--                 ^^^^^^^

Тип этого нового значения не был ограничен, и, следовательно, такая же проблема не возникает; это может быть что-то вроде a -> b -> c, что вы хотите.

По этой причине тип left' более ограничен, чем тип left, что делает их типы неравными.

Чтобы проиллюстрировать эту концепцию более конкретно, я опишу вам более точно, как это ограничение распространяется назад.

Мы знаем, что подпись left' имеет вид (a -> b) -> Either a q -> Either b q. Однако в строке 2 указывается Either a q = Either b q, что означает a = b, поэтому тип теперь становится (a -> a) -> Either a q -> Either a q.

.
19 голосов
/ 30 марта 2019

Проблема здесь в том, что есть некоторые «скрытые» типы, которые имеют значение. Механизм определения типа может вывести те из них в первом случае, но не может во втором случае.

Когда мы используем 

Right :: forall a b. b -> Either a b

нам на самом деле нужно выбрать, какие типы a и b. К счастью, вывод типа делает этот выбор для нас в большинстве случаев. Тип b легко выбрать: это тип значения внутри аргумента Right. Тип a вместо этого может быть чем угодно - механизм вывода должен полагаться на контекст, чтобы «принудительно» сделать выбор для a. Например, обратите внимание, что все эти проверки типов: 

test0 :: Either Int Bool
test0 = Right True

test1 :: Either String Bool
test1 = Right True

test2 :: Either [(Char, Int)] Bool
test2 = Right True

Теперь в вашей первой функции 

left :: (t -> a) -> Either t b -> Either a b
left f (Left x) = Left (f x)
left _ (Right x) = Right x

Первый совпадающий Right x на самом деле Right x :: Either t b, где неявные аргументы типа выбираются равными t и b. Это заставляет x иметь тип b. С этой информацией вывод типа пытается определить тип для второго Right x. Там он может видеть, что он должен иметь форму Either ?? b, начиная с x :: b, но, как это случилось с нашими test примерами выше, мы можем использовать что угодно для ??. Таким образом, механизм вывода типов выбирает другую переменную типа a (тип может быть t, но может быть и другим).

Вместо этого во второй функции 

left' :: (t -> t) -> Either t b -> Either t b
left' f (Left x) = Left (f x)
left' _ r@(Right _) = r

мы даем имя (r) шаблону Right _. Как и выше, предполагается, что тип Either t b. Однако теперь мы используем имя r справа от =, поэтому вывод типа не должен ничего выводить и может (на самом деле must ) просто повторно использовать имеющийся тип уже выведено за r. Это делает тип вывода тем же Either t b, что и для входа, и, в свою очередь, заставляет f иметь тип t -> t.

Если это сбивает с толку, вы можете попытаться полностью избежать вывода типов и предоставить явный выбор для типов, используя синтаксис Right @T @U для выбора функции U -> Either T U. (Для этого вам нужно будет включить расширения ScopedTypeVariables, TypeApplications.) Тогда мы можем написать: 

left :: forall t a b. (t -> a) -> Either t b -> Either a b
left f (Left x) = Left @a @b (f x)
left _ (Right x) = Right @a @b x
                      -- ^^ -- we don't have to pick @t here!

Мы также можем иметь 

left :: forall t b. (t -> t) -> Either t b -> Either t b
left f (Left x) = Left @t @b (f x)
left _ (Right x) = Right @t @b x

и все будет работать нормально. GHC предпочитает первый тип, поскольку он является более общим, позволяя a быть чем угодно (включая t, но также включая другие типы).

Нет приложения типа для указания во втором определении, так как оно использует то же значение r справа и слева: 

left' :: forall t b. (t -> t) -> Either t b -> Either t b
left' f (Left x) = Left @t @b (f x)
left' _ r@(Right x) = r
                   -- ^^ -- can't pick @a here! it's the same as on the LHS
...