Я знаю, как некоторые негативные события могут окончательно быть плохими:
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)
Любой указатель на литературу по этому вопросу будет принята с благодарностью.
lo.logic
type-theory
soundness
Ptival
источник
источник
Ответы:
Причину запрета негативных явлений можно понять по аналогии с теоремой Кнастера-Тарского. Эта теорема говорит, что
В традиционной теории моделей решетки можно рассматривать как суждения, а отношение порядка p ≤ q можно понимать как следствие (т. Е. Правда q связана с истинностью p ).L p≤q q p
Когда мы переходим от теории моделей к теории доказательств, решетки обобщаются на категории. Типы можно рассматривать как объекты категории , а отображение е : P → Q представляет собой доказательство того, что Q может быть получена из Q .C e:P→Q Q Q
Когда мы пытаемся интерпретировать типы, определенные рекурсивными уравнениями, ее, , очевидное, что нужно сделать, это искать обобщение теоремы Кнастера-Тарского. Таким образом, вместо монотонной функции на решетке мы знаем, что нам нуженфунктор F : C → C , который отправляет объекты объектам, но обобщает условие монотонности, так что каждое отображение e : P → Q получает отображение F ( e ) : F ( P ) → F ( Q ) (с условиями когерентности, что F отправляет тождества в тождества и сохраняет композиции так, чтобы FN=μα.1+α F:C→C e:P→Q F(e):F(P)→F(Q) F ).F(g∘f)=F(g)∘F(f)
Так что если вы хотите, чтобы индуктивный тип данных , вам также необходимо указать функторное действие в терминах для оператора типа F , чтобы быть уверенным, что требуемая фиксированная точка существует. Условие строгой позитивности в Agda и Coq являетсясинтаксическимусловием, подразумевающим этосемантическоеограничение. Грубо говоря, он говорит, что если вы строите оператор типа из сумм и продуктов, то вы всегда можете составить функторное действие, и поэтому любой тип, сформированный таким образом, должен иметь фиксированную точку.μ α .F( α ) F
В языках с зависимой типизацией у вас также есть индексированные и параметризованные типы, поэтому ваша реальная задача более сложна. Боб Атки (который писал об этом здесь и здесь ) говорит мне, что хорошее место для поиска этой истории:
Как отмечает Андрей, принципиально, хорошо или нет отрицательный случай, зависит от того, какая у вас модель теории типов. По сути, когда у вас есть рекурсивное определение, вы ищете фиксированную точку, и в математике существует множество теорем о фиксированной точке.
Лично я часто использовал теорему Банаха о неподвижной точке, которая гласит, что если у вас есть строго сжимающая функция в метрическом пространстве, то она имеет единственную неподвижную точку. Эта идея была введена в семантику Морисом Ниватом (IIRC) и была тщательно изучена Америкой и Руттеном, а недавно Биркедал и его сотрудники были связаны с популярной операционной техникой, называемой «пошаговая индексация».
Это порождает теории типов, где отрицательные вхождения в рекурсивных типах разрешены, но только когда отрицательные вхождения происходят в специальном конструкторе типа «осторожность». Эта идея была введена Хироши Накано, и связь с теоремой Банаха была сделана мной и Ником Бентоном, а также Ларсом Биркедалом и его соавторами.
источник
Иногда вы можете решить рекурсивные уравнения «по счастливой случайности».
Вывод: есть два решения: пустой тип (который вы назвали
False
) и тип блока()
.Integer
(Integer -> Bool) -> Bool
источник
Трудно что-либо добавить к объяснениям Андрея или Нила, но я попробую. Я собираюсь попытаться рассмотреть синтаксическую точку зрения, а не пытаться раскрыть основную семантику, потому что объяснение более элементарно, и я дам более простой ответ на ваш вопрос.
Важнейшей ссылкой является следующее:
Мендлер, Н. (1991). Индуктивные типы и ограничения типов в лямбда-исчислении второго порядка. Боюсь, я не нашел ссылку в Интернете. Заявления и доказательства могут быть найдены в докторской диссертации Накса (очень рекомендуется прочитать!).
и так
Конечно, вы работаете не с эквалайзерами, а с конструкторами , т.е.
а не строгое равенство. Однако вы можете определить
этого достаточно для того, чтобы этот результат продолжался:
Во втором примере все немного сложнее, так как у вас есть что-то вроде
с участием
Это было бы легко решить, если бы Haskell разрешил такие определения типов:
В этом случае вы можете создать циклический комбинатор точно так же, как и раньше. Я подозреваю, что вы можете нести подобную (но более сложную) конструкцию, используя
Проблема здесь в том, что построить изоморфизм
Вы должны иметь дело со смешанной дисперсией.
источник