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

Question

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

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

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

int y = Foo<int>(3);

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

Foo :: forall T. T -> T

Я слышал, как люди говорят, что "это как лямбда-абстракция на уровне типов". Итак, 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 и существует на самом деле не "лямбда на уровне типа". Но тогда что они? Я понимаю, что этот вопрос довольно расплывчатый, но может кто-нибудь прояснить это для меня?

---

Возможное объяснение заключается в следующем:

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

forall n in Integers: P(n)

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

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

С типом:

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

Существует такой же тип. 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#, C# и т. Д. Например, в F# вы делаете id<int> чтобы получить функцию тождества для целых чисел, что не имеет смысла в этой модели: id - это функция для значений, а не функция для типов, которая возвращает функцию для значений.

---

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

Answer 1

Позвольте мне ответить на ваши вопросы отдельно.

• Называть forall "лямбда на уровне типа" неточно по двум причинам. Во-первых, это тип лямбды, а не сама лямбда. Во-вторых, эта лямбда живет на уровне термина, даже если она абстрагируется от типов (лямбды на уровне типов также существуют, они предоставляют то, что часто называют универсальными типами).

• Универсальное количественное определение не обязательно подразумевает "одинаковое поведение" для всех экземпляров. Это конкретное свойство, называемое "параметричностью", которое может присутствовать или не присутствовать. Простое полиморфное лямбда-исчисление является параметрическим, потому что вы просто не можете выразить любое непараметрическое поведение. Но если вы добавите такие конструкции, как typecase (анализ интенсионального типа) или проверили приведение как более слабую форму, то вы потеряете параметрическость. Параметричность подразумевает хорошие свойства, например, она позволяет реализовать язык без какого-либо представления типов во время выполнения. И это порождает очень сильные рассуждения, см., Например, статью Вадлера "Теоремы бесплатно!". Но это компромисс, иногда вы хотите отправить на типы.

• Экзистенциальные типы по существу обозначают пары типа (так называемого свидетеля) и термина, иногда называемого пакетами. Один из распространенных способов их просмотра - реализация абстрактных типов данных. Вот простой пример:

  pack (Int, (λx. x, λx. x)): ∃ T.(Int → T) × (T → Int)

  Это простой ADT, представлением которого является Int, и который предоставляет только две операции (как вложенный кортеж) для преобразования целых чисел в абстрактный тип T и из него. Это основа теорий типов для модулей, например.

• Таким образом, универсальное количественное определение обеспечивает абстракцию данных на стороне клиента, в то время как экзистенциальные типы дважды обеспечивают абстракцию данных на стороне разработчика.

• В качестве дополнительного замечания, в так называемом лямбда-кубе forall и arrow обобщаются на единое понятие Π-типа (где T1→T2 = Π(x:T1).T2 и ∀AT = Π(A:*).T), а также существует, и кортеж можно обобщить на Σ-типы (где T1×T2 = Σ(x:T1).T2 и ∃AT = Σ(A:*).T). Здесь тип * является "типом типов".

Answer 2

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

Во-первых, нельзя сказать, что forall является лямбда на уровне типа, потому что уже есть понятие лямбда на уровне типа, и это отличается от forall, Он появляется в системе F_omega, расширении системы F с вычислением на уровне типов, что полезно, например, для объяснения систем модулей ML (модули F-ing, Андреас Россберг, Клаудио Руссо и Дерек Драйер, 2010).

В (синтаксис) System F_omega вы можете написать, например:

type prod =
  lambda (a : *). lambda (b : *).
    forall (c : *). (a -> b -> c) -> c

Это определение "конструктора типа" prod, такие как prod a b тип церковного кодирования типа продукта (a, b), Если есть вычисления на уровне типов, вам нужно контролировать их, если вы хотите обеспечить завершение проверки типов (в противном случае вы можете определить тип (lambda t. t t) (lambda t. t t), Это делается с помощью "системы типов на уровне типов" или системы типов. prod будет добрым * -> * -> *, Только типы в натуре * могут быть заполнены значениями, типы более высокого типа могут применяться только на уровне типов. lambda (c : k) . .... является абстракцией уровня типа, которая не может быть типом значения и может существовать в любой форме k -> ..., в то время как forall (c : k) . .... классифицировать значения, которые являются полиморфными в некотором типе c : k и обязательно наземного вида *,

Во-вторых, между forall системы F и Pi-типы теории типов Мартина-Лёфа. В Системе F полиморфные значения делают одно и то же для всех типов. В первом приближении можно сказать, что значение типа forall a . a -> a будет (неявно) принимать тип t в качестве ввода и возврата значения типа t -> t, Но это говорит о том, что в процессе могут происходить некоторые вычисления, а это не так. Морально, когда вы создаете экземпляр значения типа forall a. a -> a в значение типа t -> t, значение не меняется. Есть три (связанных) способа думать об этом:

• В системе F количественное определение имеет стирание типов, вы можете забыть о типах, и вы все равно будете знать, какова динамическая семантика программы. Когда мы используем вывод типа ML, чтобы оставить абстракцию и реализацию полиморфизма неявными в наших программах, мы на самом деле не позволяем механизму вывода "заполнять дыры в нашей программе", если вы думаете о "программе" как о динамическом объекте, который будет запущен и вычислить.

• forall a . foo это не то, что "производит экземпляр foo для каждого типа a, но одного типа foo это "универсальный в неизвестном типе a ".

• Вы можете объяснить универсальное количественное определение как бесконечное соединение, но есть условие однородности, что все конъюнкты имеют одинаковую структуру, и, в частности, что все их доказательства одинаковы.

Напротив, типы Pi в теории типов Мартина-Лёфа действительно больше похожи на типы функций, которые что-то принимают и возвращают. Это одна из причин, по которой их можно легко использовать не только для зависимости от типов, но также для зависимости от терминов (зависимых типов).

Это имеет очень важные последствия, если вы обеспокоены обоснованностью этих формальных теорий. Система F является непредсказуемой (количественно определенный тип количественно определяет все типы, включая саму себя), и причина, по которой она все еще звучит, заключается в однородности универсального количественного определения. Хотя введение непараметрических конструкций является разумным с точки зрения программиста (и мы все еще можем рассуждать о параметричности в общем непараметрическом языке), оно очень быстро разрушает логическую согласованность базовой статической системы рассуждений. Предикативную теорию Мартина-Лёфа гораздо проще доказать, что она правильна, и ее правильное расширение.

Описание высокого уровня этого аспекта единообразия / универсальности Системы F см. В статье Фрукарта и Лонго, 97. Замечания Карнапа по Импредикативным Определениям и Теореме Обобщенности. Для более технического исследования сбоя системы F в присутствии непараметрических конструкций см. Параметричность и варианты оператора Джерарда J Роберта Харпера и Джона Митчелла (1999). Наконец, для описания, с точки зрения языкового дизайна, о том, как отказаться от глобальной параметричности, чтобы вводить непараметрические конструкции, но при этом иметь возможность локально обсуждать параметричность, см. Непараметрическая параметричность Джорджа Нейса, Дерека Драйера и Андреаса Россберга 2011.

Это обсуждение различий между "вычислительной абстракцией" и "единообразным абстракцией" было возобновлено благодаря большой работе по представлению переменных-связывателей. Конструкция привязки выглядит как абстракция (и может быть смоделирована лямбда-абстракцией в стиле HOAS), но имеет однородную структуру, которая делает ее скорее скелетом данных, чем семейством результатов. Это много обсуждалось, например, в сообществе LF, "репрезентативные стрелки" в Twelf, "позитивные стрелки" в работе Licata&Harper и т. Д.

В последнее время несколько человек работали над связанным понятием "нерелевантность" (лямбда-абстракции, где результат "не зависит" от аргумента), но все еще не совсем ясно, насколько тесно это связано с параметрическим полиморфизмом. Одним из примеров является работа Натана Мишра-Лингера с Тимом Шеардом (например, " Стирание и полиморфизм в системах чистого типа").

Answer 3

если лямбда - это то, что существует

Ну конечно же, кортеж!

В теории типов Мартина-Лёфа имеется Π типов, соответствующих функциям / универсальной квантификации и Σ-типам, соответствующих кортежам / экзистенциальной квантификации.

Их типы очень похожи на то, что вы предложили (я использую обозначение Agda здесь):

Π : (A : Set) -> (A -> Set) -> Set
Σ : (A : Set) -> (A -> Set) -> Set

В самом деле, Π - бесконечное произведение, а Σ - бесконечная сумма. Обратите внимание, что они не являются "пересечением" и "объединением", как вы предложили, потому что вы не можете сделать это без дополнительного определения того, где типы пересекаются. (какие значения одного типа соответствуют каким значениям другого типа)

Из этих двух конструкторов типов вы можете иметь все нормальные, полиморфные и зависимые функции, нормальные и зависимые кортежи, а также экзистенциально и универсально выраженные выражения:

-- Normal function, corresponding to "Integer -> Integer" in Haskell
factorial : Π ℕ (λ _ → ℕ)

-- Polymorphic function corresponding to "forall a . a -> a"
id : Π Set (λ A -> Π A (λ _ → A))

-- A universally-quantified logical statement: all natural numbers n are equal to themselves
refl : Π ℕ (λ n → n ≡ n)


-- (Integer, Integer)
twoNats : Σ ℕ (λ _ → ℕ)

-- exists a. Show a => a
someShowable : Σ Set (λ A → Σ A (λ _ → Showable A))

-- There are prime numbers
aPrime : Σ ℕ IsPrime

Тем не менее, это совсем не касается параметричности, а параметрическость AFAIK и теория типов Мартина-Лёфа независимы.

Для параметричности люди обычно обращаются к работе Филиппа Уодлера.