Переменные типа Scoped требуют явных указаний. Зачем?

Question

Если вы хотите использовать переменные типа 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 по-прежнему? Разве не ясно, что переменные типа в аннотациях внутри тела функции ссылаются на одноименные переменные в сигнатуре функции? Или набор текста будет проблематичным или неоднозначным?

Answer 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 применяется к аргументу. И действительно, средство проверки типов отклоняет этот код.

С другой стороны, с одним 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подпись.