Что такое квантификаторы типов?

Многие статически типизированные языки обладают параметрическим полиморфизмом. Например, в C#можно определить:

T Foo<T>(T x){ return x; }

На сайте вызовов вы можете сделать:

int y = Foo<int>(3);

Эти типы также иногда пишут так:

Foo :: forall T. T -> T

Я слышал, как люди говорят, что «forall похож на лямбда-Типовой уровень». Итак, Foo — это функция, которая принимает тип (, например, int), и возвращает значение (, например, функцию типа int -> int). Многие языки выводят параметр типа, так что вы можете написать Foo(3)вместо Foo<int>(3).

Предположим, у нас есть объект fтипа forall T. T -> T. Что мы можем сделать с этим объектом, так это сначала передать ему тип Q, написав f<Q>. Затем мы возвращаем значение типа Q -> Q. Однако некоторые fнедействительны. Например, этоf:

f<int> = (x => x+1)
f<T> = (x => x)

Итак, если мы «вызовем» f<int>, мы получим значение с типом int -> int, и в общем случае, если мы «вызовем» f<Q>, мы получим значение с типом Q -> Q, так что это хорошо. Однако обычно считается, что это fне является допустимой вещью типа forall T. T -> T, потому что оно делает что-то разное в зависимости от того, какой тип вы ему передаете. Идея forall заключается в том, что это явно не разрешено. Кроме того, если forall — это лямбда для уровня типов, то что тогда существует? (т.е. экзистенциальная квантификация). По этим причинам кажется, что forall и exists на самом деле не являются "лямбдой на уровне типа". Но тогда какие они? Я понимаю, что этот вопрос довольно расплывчатый, но может ли кто-нибудь прояснить это для меня?

Возможное объяснение следующее.:

Если мы посмотрим на логику, кванторы и лямбда — это две разные вещи.Пример квантифицированного выражения::

forall n in Integers: P(n)

Таким образом, есть две части для всего:набора для количественной оценки по (, например. Целые числа)и предикат (, например. Р). Forall можно рассматривать как функцию более высокого порядка:

forall n in Integers: P(n) == forall(Integers,P)

С типом:

forall :: Set<T> -> (T -> bool) -> bool

Exists имеет тот же тип. Forall подобен бесконечной конъюнкции, где S[n] — n--й элемент множества S:

forall(S,P) = P(S[0]) ∧ P(S[1]) ∧ P(S[2])...

Exists подобен бесконечной дизъюнкции:

exists(S,P) = P(S[0]) ∨ P(S[1]) ∨ P(S[2])...

Если провести аналогию с типами, то можно сказать, что аналог типа ∧ вычисляет тип пересечения ∩, а аналог типа ∨ вычисляет тип объединения ∪. Тогда мы могли бы определить forall и exists на типах следующим образом:

forall(S,P) = P(S[0]) ∩ P(S[1]) ∩ P(S[2])...
exists(S,P) = P(S[0]) ∪ P(S[1]) ∪ P(S[2])...

Таким образом, forall является бесконечным пересечением, а exists является бесконечным объединением. Их типы будут:

forall, exists :: Set<T> -> (T -> Type) -> Type

Например, тип полиморфной функции тождества. Здесь Types— множество всех типов, а ->— конструктор типов для функций, а =>— лямбда-абстракция:

forall(Types, t => (t -> t))

Теперь вещь типа forall T:Type. T -> T— это значение , а не функция от типов к значениям. Это значение, тип которого является пересечением всех типов T -> T, где T охватывает все типы. Когда мы используем такое значение, нам не нужно применять его к типу. Вместо этого мы используем суждение о подтипе:

id :: forall T:Type. T -> T
id = (x => x)

id2 = id :: int -> int

Это понижает idтип int -> int. Это верно, потому что int -> intтакже появляется в бесконечном пересечении.

Я думаю, это прекрасно работает и ясно объясняет, что такое forall и чем оно отличается от лямбда, но эта модель несовместима с тем, что я видел в таких языках, как ML, F#, C#, и т. д. Например, в F#вы делаете id<int>, чтобы получить функцию идентификации для целых чисел, что не имеет смысла в этой модели :id — это функция для значений, а не функция для типов, которая возвращает функцию для ценности.

Может ли кто-нибудь со знанием теории типов объяснить, что именно forall и существует? И насколько верно, что «forall — это лямбда на уровне типа»?