Какова теоретическая основа для экзистенциальных типов?

Ответ 1

Прежде всего, взгляните на "соответствие Карри Говарда", в котором говорится, что типы в компьютерной программе соответствуют формулам в интуиционистской логике. Интуиционистская логика подобна "обычной" логике, которую вы изучили в школе, но без закона исключенного исключения из среднего или двойного отрицания:

• Не аксиома: P ⇔ ¬¬P (но P ⇒ ¬¬P в порядке)

• Не аксиома: P ∨ ¬P

Законы логики

Вы находитесь на правильном пути с законами DeMorgan, но сначала мы будем использовать их для получения новых. Соответствующая версия законов DeMorgan:

• ∀x. P (x) = ¬∃x. ¬P (х)
• ∃x. P (x) = ¬∀x. ¬P (х)

Мы можем получить (∀x. P ⇒ Q (x)) = P ⇒ (∀x. Q (x)):

• (∀x. P ⇒ Q (x))
• (∀x. ¬P ∨ Q (x))
• ¬P ∨ (∀x. Q (x))
• P ⇒ (∀x. Q)

И (∀x. Q (x) ⇒ P) = (∃x. Q (x)) ⇒ P (этот используется ниже):

• (∀x. Q (x) ⇒ P)
• (∀x. ¬Q (x) ∨ P)
• (¬¬∀x. ¬Q (x)) ∨ P
• (¬∃x. Q (x)) ∨ P
• (∃x. Q (x)) ⇒ P

Заметим, что эти законы справедливы и в интуиционистской логике. Два приведенных нами закона приводятся в приведенной ниже статье.

Простые типы

Простейшие типы легко работать. Например:

data T = Con Int | Nil

Конструкторы и аксессоры имеют следующие типы сигнатур:

Con :: Int -> T
Nil :: T

unCon :: T -> Int
unCon (Con x) = x

Конструкторы типов

Теперь давайте создадим конструкторы типа. Возьмите следующее определение данных:

data T a = Con a | Nil

Это создает два конструктора,

Con :: a -> T a
Nil :: T a

Конечно, в Haskell переменные типа неявно определяются количественно, поэтому они действительно:

Con :: ∀a. a -> T a
Nil :: ∀a. T a

Аксессуар также легко:

unCon :: ∀a. T a -> a
unCon (Con x) = x

Количественные типы

Добавьте добавочный квантор существования ∃ к нашему исходному типу (первый, без конструктора типов). Вместо того, чтобы вводить его в определение типа, которое не похоже на логику, введите его в определения конструктора/аксессора, которые выглядят как логика. Мы определим определение данных позже, чтобы оно соответствовало.

Вместо Int теперь мы будем использовать ∃x. t. Здесь t - это какое-то выражение типа.

Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)

На основе правил логики (второе правило выше) мы можем переписать тип Con на:

Con :: ∀x. t -> T

Когда мы переместили экзистенциальный квантор вовне (prenex form), он превратился в универсальный квантификатор.

Итак, теоретически эквивалентны следующие:

data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil

Кроме того, в Haskell нет синтаксиса для exists.

В неинтуиционистской логике допустимо выводить из типа unCon следующее:

unCon :: ∃ T -> t -- invalid!

Причина, по которой это неверно, заключается в том, что такое преобразование не допускается в интуиционистской логике. Таким образом, невозможно написать тип для unCon без ключевого слова exists, и невозможно поставить подпись типа в prenex-форме. Трудно сделать проверку типа гарантией прекращения в таких условиях, поэтому Haskell не поддерживает произвольные кванторы существования.

Источники

"Первоклассный полиморфизм с типом вывода", Марк П. Джонс, Материалы 24-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования (web)

Ответ 2

Плоткин и Митчелл установили семантику для экзистенциальных типов, в своей знаменитой статье, который установил связь между абстрактными типами в языках программирования и экзистенциальными типами в логике,

Митчелл, Джон С.; Плоткин, Гордон Д.; Абстрактные типы имеют экзистенциальные Тип, ACM-транзакции на языках программирования и системах, том. 10, № 3, июль 1988 г., стр. 470-502

На высоком уровне

Абстрактные объявления типов данных появляются на типизированных языках программирования, таких как Ada, Alphard, CLU и ML. Эта форма декларации связывает список идентификаторов с типом с связанными операциями, составное "значение" мы называем алгеброй данных. Мы используем типизированный тип второго порядка лямбда-исчисление SOL, чтобы показать, как могут быть заданы типы алгебр данных, переданы как параметры и возвращаются как результаты вызовов функций. В процесс, мы обсуждаем семантику абстрактного типа данных декларации и просмотр связи между типизированным программированием языков и конструктивной логики.

Ответ 3

Это указано в связанной с вами статье wiki haskell. Я возьму некоторые строки кода и комментарии от него и попытаюсь объяснить.

data T = forall a. MkT a

Здесь у вас есть тип T с конструктором типа MkT :: forall a. a -> T, правильно? MkT является (грубо) функцией, поэтому для любого возможного типа a функция MkT имеет тип a -> T. Итак, мы согласны с тем, что с помощью этого конструктора мы можем построить такие значения, как [MkT 1, MkT 'c', MkT "hello"], все из них типа T.

foo (MkT x) = ... -- what is the type of x?

Но что происходит, когда вы пытаетесь извлечь (например, через сопоставление с образцом) значение, заключенное в T? Аннотации этого типа только говорят T, без какой-либо ссылки на тип фактически содержащегося в нем значения. Мы можем только согласиться с тем, что, что бы это ни было, у него будет один (и только один) тип; как мы можем утверждать это в Haskell?

x :: exists a. a

Это просто говорит, что существует тип a, к которому принадлежит x. На этом этапе должно быть ясно, что, удалив определение forall a из MkT и явно указывая тип обернутого значения (то есть exists a. a), мы можем добиться того же результата.

data T = MkT (exists a. a)

В нижней строке это тоже самое, если вы добавляете условия для реализованных типов, как в ваших примерах.