Переменные типа с переменным типом требуют явных foralls. Зачем?

Если вы хотите использовать GHC лексически скопированные переменные типа, вам также нужно использовать явное универсальное количественное определение, То есть вы должны добавить объявления forall к подписям типа ваших функций:

{-# LANGUAGE ExplicitForAll, ScopedTypeVariables #-}

f :: forall a . [a] -> [a]      -- The `forall` is required here ...
f (x:xs) = xs ++ [x :: a]       -- ... to relate this `a` to the ones above.

На самом деле это имеет какое-то отношение к количественной оценке, или авторы расширений просто кооперируют ключевое слово forall в качестве удобного маркера для того, где применяется новое более широкое охват?

Другими словами, почему мы не можем оставить forall, как обычно? Разве не ясно, что переменные типа в аннотациях внутри тела функции относятся к переменным с тем же именем в сигнатуре функции? Или написание будет как-то проблематичным или двусмысленным?

Ответы

Ответ 1

Да, квантификатор имеет смысл и необходим для того, чтобы типы имели смысл.

Прежде всего обратите внимание, что в Haskell на самом деле нет такой вещи, как "неквалифицированная" подпись типа. Подписи без forall действительно неявно определяются количественно. Этот код...

f :: [a] -> [a]                         -- No `forall` here ...
f (x:xs) = xs ++ [x :: a]               -- ... or here.

... действительно означает следующее:

f :: forall a . [a] -> [a]              -- With a `forall` here ...
f (x:xs) = xs ++ [x :: forall a . a]    -- ... and another one here.

Итак, дайте понять, что это говорит. Важно отметить, что переменные типа с именем a в сигнатурах для f и для x связаны отдельными кванторами. Это означает, что они являются разными переменными, несмотря на совместное использование имени. Таким образом, приведенный выше код эквивалентен этому:

f :: forall a . [a] -> [a]
f (x:xs) = xs ++ [x :: forall b . b]    -- I've changed `a` to `b`

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

С другой стороны, с одним forall в сигнатуре для f...

f :: forall a . [a] -> [a]              -- A `forall` here ...
f (x:xs) = xs ++ [x :: a]               -- ... but not here.

... a в сигнатуре на x привязывается квантором в начале сигнатуры типа f, поэтому этот a представляет тот же тип, что и тип, представленный переменными, называемыми a в подписи f.