Многие статически типизированные языки имеют параметрический полиморфизм. Например, в С# можно определить:
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 и exist на самом деле не "лямбда на уровне типа". Но что они? Я понимаю, что этот вопрос довольно расплывчатый, но может ли кто-нибудь прояснить это для меня?
Возможное объяснение следующее:
Если мы посмотрим на логику, кванторы и лямбда - две разные вещи. Пример количественного выражения:
forall n in Integers: P(n)Таким образом, для forall есть две части: набор для количественной оценки (например, целые числа) и предикат (например, P). Forall можно рассматривать как функцию более высокого порядка:
forall n in Integers: P(n) == forall(Integers,P)С типом:
forall :: Set<T> -> (T -> bool) -> boolExists имеет тот же тип. Forall - бесконечная конъюнкция, где S [n] - n-й элемент множества S:
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 и существовать по типам следующим образом:
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 является бесконечным пересечением, и существует бесконечный союз. Их типы:
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 #, С# и т.д. Например, в F # вы выполняете
id<int>, чтобы получить функцию идентификации в int, что не имеет смысла в этой модели: id - это функция для значений, а не функция для типов, возвращающая функцию на значения.
Может ли кто-нибудь, кто знает теорию типов, объяснить, что именно существует и существует? И насколько это верно, что "forall лямбда на уровне уровня"?
