Почему аннотация этого типа неверна?

Я попытался следовать статье Габриэля Гонсалеса и столкнулся с несоответствием типов . Рассмотрим следующий короткий модуль:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE Rank2Types #-}

module Yoneda where

newtype F a = F a deriving (Show, Functor)

type G f a = forall a'. (a -> a') -> f a'

fw :: Functor f => G f a -> f a
fw x = x id

bw :: Functor f => f a -> G f a
bw x = \f -> fmap f x

Он компилируется нормально. (И с ghc 8.2.2 и с 8.4.3.) Но когда тыкаю в repl, fw и bw не сочиняются:

λ :t bw . fw

<interactive>:1:6: error:
    • Couldn't match type ‘a’ with ‘G f a1’
      ‘a’ is a rigid type variable bound by
        the inferred type of it :: Functor f => a -> (a1 -> a') -> f a'
        at <interactive>:1:1
      Expected type: a -> f a1
        Actual type: G f a1 -> f a1
    • In the second argument of ‘(.)’, namely ‘fw’
      In the expression: bw . fw

Когда я смотрю на bw более внимательно, оказывается, что типы функтора, которые он принимает и возвращает, различны:

λ :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'

— Хоть я и указал в подписи типа, что они должны быть одинаковыми! И какие бы аннотации типов я ни добавлял к fw и bw, они не хотят унифицироваться.

Если я уберу подпись типа из fw, все будет работать гладко. В частности, предполагаемая сигнатура типа будет следующей:

fw :: ((a -> a) -> t) -> t

Итак, получается, что квантификатор forall все портит. Но я не понимаю, почему. Разве это не должно означать "подойдет любой тип a -> a', включая a -> a"? Кажется, что один и тот же синоним типа G f a действует по-разному в сигнатурах типов fw и bw!

Что тут происходит?

Еще немного экспериментов:

λ (fw . bw) (F 1)
...error...
λ (fw (bw (F 1)))
F 1
λ :t fw . undefined
...error...
λ :t undefined . fw
...error
λ :t bw . undefined
bw . undefined :: Functor f => a1 -> (a2 -> a') -> f a'
λ :t undefined . bw
undefined . bw :: Functor f => f a -> c

Итак, (как указал @chi в ответе) никакая функция не может быть составлена ​​из fw. Но не так для bw. Почему?


types haskell higher-rank-types isomorphism category-theory
person Ignat Insarov    schedule 29.07.2018    source источник
comment
Это выглядит как (плохая) ошибка для меня.   -  person Daniel Wagner    schedule 29.07.2018
comment
:type не очень точен, особенно для функций. Возможно, есть ошибка, которая портит подпись bw. Попробуйте использовать :type +v bw.   -  person HTNW    schedule 29.07.2018
comment
Я получаю bw :: Functor f => f a -> (a -> a') -> f a'. Как вы получили f1 и f2 выше?   -  person chi    schedule 29.07.2018

Ответы (2)


arrow_upward
3
arrow_downward

Это вопрос предикативности.

По существу, если у нас есть полиморфное значение f :: forall a . SomeTypeDependingOn a и мы используем его в каком-то более крупном выражении, это может преобразовать тип a в любой тип T, необходимый для соответствия этому контексту. Однако предикативность требует, чтобы T не содержало foralls. Это ограничение необходимо для вывода типа.

В вашем коде bw . fw вы используете полиморфную функцию . (композиция). Он имеет полиморфный тип, где одна переменная типа t обозначает домен второй функции, которую нужно составить (g в f . g). Для bw . fw для проверки типа мы должны выбрать t ~ G f a, но G f a = (forall a' . ...), так что это нарушает предикативность.

Обычное решение — использовать оболочку newtype.

newtype G f a = G { unG :: forall a'. (a -> a') -> f a' }

который «скрывает» forall под конструктором, так что t ~ G f a становится разрешенным. Чтобы использовать это, нужно использовать изоморфизмы G и unG по мере необходимости, обертывая и разворачивая по мере необходимости. Это требует от программиста дополнительной работы, но именно эта работа позволяет алгоритму вывода выполнять свою работу.

В качестве альтернативы не используйте . и создавайте свои функции в точечном стиле.

test :: Functor f => G f a -> G f a
test x = bw (fw x)

О типе bw, как сообщает GHCi:

> :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'

Этот тип является результатом "forall подъема", который по существу "перемещает" универсальные квантификаторы следующим образом:

a1 -> ... -> forall b. F b   =====>     forall b. a1 -> ... -> F b

Подъем выполняется автоматически, чтобы облегчить вывод типа.

Подробнее в defail, у нас есть

bw :: forall f a . Functor f => f a -> G f a
-- by definition of G
bw :: forall f a . Functor f => f a -> (forall a'. (a -> a') -> f a')
-- after hoisting
bw :: forall f a a'. Functor f => f a -> (a -> a') -> f a'

Поскольку теперь все квантификаторы находятся на верхнем уровне, при составлении bw с другой функцией, как в bw . h или h . bw, мы можем сначала создать экземпляр f, a, a' для переменных нового типа, а затем выполнить унификацию таких переменных, чтобы они соответствовали типу h.

Например, в bw . undefined мы поступаем следующим образом

 -- fresh variables for (.)
 (.) :: (b -> c) -> (a -> b) -> a -> c
 -- fresh variables for bw
 bw :: Functor f . f a1 -> (a1 -> a') -> f a'
 -- fresh variables for undefined
 undefined :: a2

 So we get:
 b = f a1
 c = (a1 -> a') -> f a'
 a2 = a -> b

 Hence the type of (bw . undefined) is
 a -> c
 = a -> (a1 -> a') -> f a'
 (assuming Functor f)

GHCi согласен, за исключением того, что он выбирает другие имена для переменных типа. Этот выбор, конечно, несущественен.

(bw . undefined) :: Functor f => a1 -> (a2 -> a') -> f a'

Ах-ха! Кажется, есть проблема с GHCi-8.2.2, которой нет в GHC 8.4.3.

-- GHCi 8.2.2
> :set -XRankNTypes
> type G f a = forall a'. (a -> a') -> f a'
> bw :: Functor f => f a -> G f a ; bw x = \f -> fmap f x
> :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'

-- GHCi 8.4.3
> :set -XRankNTypes
> type G f a = forall a'. (a -> a') -> f a'
> bw :: Functor f => f a -> G f a ; bw x = \f -> fmap f x
> :t bw
bw :: Functor f => f a -> (a -> a') -> f a'
person chi    schedule 29.07.2018
comment
Спасибо. Я провел еще несколько экспериментов и убедился, что действительно проблемы начинаются с .. Однако для fw это не проблема, хотя его тип также имеет G. - person Ignat Insarov; 29.07.2018
comment
Для меня это не объясняет сигнатуру типа, данную bw перед рассмотрением композиции. Почему тип bw упоминает неограниченный, несвязанный тип f2? Кажется, даже GHC не считает, что тип не связан — если вы примените bw к значению, которое унифицируется с f2 a, GHC также установит f1 таким же образом! - person Daniel Wagner; 29.07.2018
comment
@DanielWagner Я не могу воспроизвести f2. Может быть, ОП использует другое определение, где G также количественно определяет f? - person chi; 29.07.2018
comment
@chi Я могу, в 8.2.2 (единственная версия, которая у меня есть, поэтому, возможно, в других версиях нет этой ошибки). - person Daniel Wagner; 29.07.2018
comment
@DanielWagner А, думаю, все. Смотрите мое последнее редактирование. - person chi; 29.07.2018

arrow_upward
0
arrow_downward

Квантификатор forall заставляет ваш тип принимать все a -> a', но на самом деле вам нужно в fw ограничение, гарантирующее, что тип параметра и возвращаемый тип совпадают, и именно это означает подпись a -> a.

Так что да, версия forall принимает функцию a -> a, но принимает не только такие функции. Как указано выше, компилятор говорит вам, что fw должен принимать только функцию с типом a -> a.

person Ruifeng Xie    schedule 29.07.2018