«Охраняемые» негативные явления в определении индуктивных типов, всегда плохо?

11

Я знаю, как некоторые негативные события могут окончательно быть плохими:

data False

data Bad a = C (Bad a -> a)

selfApp :: Bad a -> a
selfApp (x@(C x')) = x' x

yc :: (a -> a) -> a
yc f = selfApp $ C (\x -> f (selfApp x))

false :: False
false = yc id

Однако я не уверен, что:

  • все индуктивные типы с отрицательными значениями могут повернуть неправильно

  • если это так, существует известный механический способ сделать это;

Например, я боролся, пытаясь заставить этот тип пойти не так:

type Not a = a -> False

data Bad2 a = C2 (Bad2 (Not a) -> a)

Любой указатель на литературу по этому вопросу будет принята с благодарностью.

Ptival
источник
1
Это Coq? Haskell? Теория псевдотипа? Что вы подразумеваете под "пойти не так"?
Дейв Кларк
@DaveClarke Извините, код написан на Haskell, но проблема больше связана с такими языками, как Coq или Agda, где запрещены негативные события. Под «пойти не так» я подразумеваю возможность написать термин, который расходится, таким образом, имея возможность заселить Ложь, как я это делал в своем примере на Хаскеле.
Ptival

Ответы:

10

Причину запрета негативных явлений можно понять по аналогии с теоремой Кнастера-Тарского. Эта теорема говорит, что

если - полная решетка и f : L L - монотонная функция на L , то множество неподвижных точек f также является полной решеткой. В частности, существует наименьшее фиксированная точка μ F и наибольший фиксированная точка ν F .Lf:LLLfμfνf

В традиционной теории моделей решетки можно рассматривать как суждения, а отношение порядка p q можно понимать как следствие (т. Е. Правда q связана с истинностью p ).LpqQp

Когда мы переходим от теории моделей к теории доказательств, решетки обобщаются на категории. Типы можно рассматривать как объекты категории , а отображение е : P Q представляет собой доказательство того, что Q может быть получена из Q .Ce:PQQQ

Когда мы пытаемся интерпретировать типы, определенные рекурсивными уравнениями, ее, , очевидное, что нужно сделать, это искать обобщение теоремы Кнастера-Тарского. Таким образом, вместо монотонной функции на решетке мы знаем, что нам нуженфунктор F : CC , который отправляет объекты объектам, но обобщает условие монотонности, так что каждое отображение e : P Q получает отображение F ( e ) : F ( P ) F ( Q ) (с условиями когерентности, что F отправляет тождества в тождества и сохраняет композиции так, чтобы FN=μα.1+α F:CCe:PQF(e):F(P)F(Q)F ).F(gf)=F(g)F(f)

Так что если вы хотите, чтобы индуктивный тип данных , вам также необходимо указать функторное действие в терминах для оператора типа F , чтобы быть уверенным, что требуемая фиксированная точка существует. Условие строгой позитивности в Agda и Coq являетсясинтаксическимусловием, подразумевающим этосемантическоеограничение. Грубо говоря, он говорит, что если вы строите оператор типа из сумм и продуктов, то вы всегда можете составить функторное действие, и поэтому любой тип, сформированный таким образом, должен иметь фиксированную точку.μα,F(α)F

В языках с зависимой типизацией у вас также есть индексированные и параметризованные типы, поэтому ваша реальная задача более сложна. Боб Атки (который писал об этом здесь и здесь ) говорит мне, что хорошее место для поиска этой истории:

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

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

Это порождает теории типов, где отрицательные вхождения в рекурсивных типах разрешены, но только когда отрицательные вхождения происходят в специальном конструкторе типа «осторожность». Эта идея была введена Хироши Накано, и связь с теоремой Банаха была сделана мной и Ником Бентоном, а также Ларсом Биркедалом и его соавторами.

Нил Кришнасвами
источник
7

Иногда вы можете решить рекурсивные уравнения «по счастливой случайности».

A(A)A,
  1. AA

    AA1.
    1
  2. A()1

Вывод: есть два решения: пустой тип (который вы назвали False) и тип блока ().

A(A2)2,
data Cow a = Moo ((a -> Bool) -> Bool)

A22AA22A

N22N,
2N22NInteger(Integer -> Bool) -> Bool
Андрей Бауэр
источник
3

Трудно что-либо добавить к объяснениям Андрея или Нила, но я попробую. Я собираюсь попытаться рассмотреть синтаксическую точку зрения, а не пытаться раскрыть основную семантику, потому что объяснение более элементарно, и я дам более простой ответ на ваш вопрос.

λ

Важнейшей ссылкой является следующее:

Мендлер, Н. (1991). Индуктивные типы и ограничения типов в лямбда-исчислении второго порядка. Боюсь, я не нашел ссылку в Интернете. Заявления и доказательства могут быть найдены в докторской диссертации Накса (очень рекомендуется прочитать!).

Вad

Вadзнак равноВadA

A

λИкс:Вad,Икс Икс:ВadA

и так

(λИкс:Вad,Икс Икс) (λИкс:Вad,Икс Икс):A

Вadзнак равноF(Вad)
F(Икс)ИксF(Икс)

Конечно, вы работаете не с эквалайзерами, а с конструкторами , т.е.

data Bad = Pack (Bad -> A)

а не строгое равенство. Однако вы можете определить

unpack :: Bad -> (Bad -> A)
unpack (Pack f) = f

этого достаточно для того, чтобы этот результат продолжался:

 (\x:Bad -> unpack x x) (Pack (\x:Bad -> unpack x x))

A


Во втором примере все немного сложнее, так как у вас есть что-то вроде

Вadзнак равноВad'A

Вad'ВadВad aВad (NоT a)

type Not a = a -> False

с участием

data Not a = Not a

Это было бы легко решить, если бы Haskell разрешил такие определения типов:

type Acc = Not Acc

В этом случае вы можете создать циклический комбинатор точно так же, как и раньше. Я подозреваю, что вы можете нести подобную (но более сложную) конструкцию, используя

data Acc = D (Not Acc)

Проблема здесь в том, что построить изоморфизм

Bad Acc <-> Bad (Not Acc)

Вы должны иметь дело со смешанной дисперсией.

Коди
источник