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

Haskell Wiki хорошо объясняет, как использовать экзистенциальные типы, но я не совсем понимаю теорию, стоящую за ними.

Рассмотрим пример экзистенциального типа:

data S = forall a. Show a => S a      -- (1)

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

data S = S (exists a. Show a => a)    -- (2)

т. е. настоящий "экзистенциальный" тип - я думаю, что он говорит "конструктор данных" S принимает любой тип, для которого Show экземпляр существует и упаковывает его ". Фактически, вы могли бы написать GADT следующим образом:

data S where                          -- (3)
    S :: Show a => a -> S

Я не пробовал компилировать это, но похоже, что оно должно работать. Для меня GADT, очевидно, эквивалентен коду (2), который мы хотели бы написать.

Однако для меня совершенно не очевидно, почему (1) эквивалентно (2). Почему перемещение конструктора данных наружу превращает forall в exists?

Самая близкая вещь, о которой я могу думать, - это законы де Моргана в логике, в которых взаимный порядок отрицания и квантификатора превращает экзистенциальные квантификаторы в универсальные квантификаторы, и наоборот:

¬(∀x. px) ⇔ ∃x. ¬(px)

но конструкторы данных кажутся совершенно отличным от оператора отрицания.

Какая теория лежит в основе способности определять экзистенциальные типы, используя forall вместо несуществующего exists?

3 ответа

Решение

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

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

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

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

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

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

Мы можем вывести (∀x. P ⇒ Q (x)) = P ⇒ (∀x. Q (x)):

  1. (∀x. P ⇒ Q (x))
  2. (∀x. ¬P ∨ Q (x))
  3. ¬P ∨ (∀x. Q (x))
  4. P ⇒ (∀x. Q)

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

  1. (∀x. Q (x) ⇒ P)
  2. (∀x. ¬Q (x) ∨ P)
  3. (¬¬x. ¬Q (x)) ∨ P
  4. (¬∃x. Q (x)) ∨ P
  5. (∃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), он превратился в универсальный квантификатор.

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

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

За исключением того, что нет синтаксиса для exists в Хаскеле.

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

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

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

источники

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

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

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

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

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

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

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без какой-либо ссылки на тип значения, фактически содержащегося в нем. Мы можем только согласиться с тем фактом, что, что бы это ни было, оно будет иметь один (и только один) тип; как мы можем заявить об этом в Хаскеле?

x :: exists a. a

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

data T = MkT (exists a. a)

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

Другие вопросы по тегам