Если вы достаточно усердно пытаетесь реализовать функцию, вы можете убедить себя, что это невозможно. Если вы не уверены, аргумент можно сделать более формальным: мы исчерпывающе перечисляем программы, чтобы найти, что ни одна из них невозможна. Оказывается, есть только полдюжины значимых дел для рассмотрения.
Интересно, почему этот аргумент не приводится чаще.
Абсолютно неточное резюме:
- Акт I: поиск корректуры очень прост.
- Акт II: также зависимые типы.
- Акт III: Haskell все еще хорош для написания программ с зависимой типизацией.
Я. Игра поиска в поиске
Сначала мы определим пространство поиска.
Мы можем сократить любое определение Haskell до одной из форм
lem = (exp)
для некоторого выражения (exp). Теперь нам нужно найти только одно выражение.
Посмотрите на все возможные способы создания выражения в Haskell: https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-220003 (это не учитывает расширения, упражнение для читателя).
Он умещается на странице в одном столбце, так что это не , что большой для начала. Кроме того, большинство из них являются сахаром для некоторой формы применения функции или сопоставления с образцом;мы также можем удалить классы типов с передачей словаря, поэтому у нас остаётся смехотворно маленькое лямбда-исчисление:
- лямбда-выражений,
\x -> ... - сопоставление с образцом,
case ... of ... - приложение-функция,
f x - конструкторы,
C (включая целочисленные литералы) - константы,
c (для примитивов, которые нельзя записать в терминахконструкции выше, так что различные встроенные модули (seq) и, возможно, FFI, если это считается) - переменных (связанных лямбда-выражениями и падежами)
Мы можем исключить каждую константу наоснование, что я думаю, что вопрос действительно о чистом лямбда-исчислении (или читатель может перечислить константы, чтобы исключить константы черной магии, такие как undefined, unsafeCoerce, unsafePerformIO, которые заставляют все разрушаться (любой тип обитаем идля некоторых из них система типов несостоятельна, и ее следует оставить с константами белой магии, на которые можно обобщить настоящий теоретический аргумент с помощью хорошо финансируемого тезиса).
Мы также можемразумно предположить, что мы хотим получить решение без рекурсии (чтобы избавиться от шума, такого как lem = lem и fix, если вы чувствовали, что раньше не могли с ним расстаться), и которое на самом деле имеет нормальную форму или предпочтительноканоническая форма относительно βη-эквивалентности. Другими словами, мы уточняем и исследуем множество возможных решений следующим образом.
lem :: _ -> _ имеет тип функции, поэтому мы можем предположить WLOG , что его определениеначинается с лямбды:
-- Any solution
lem = (exp)
-- is η-equivalent to a lambda
lem = \refutation -> (exp) refutation
-- so let's assume we do have a lambda
lem = \refutation -> _hole
Теперь перечислим, что может быть под лямбдой.
Это может быть конструктор, который затем имеетбыть Refl, но нет никаких доказательств того, что Choose x y ~ 2 в контексте (здесь мы могли бы формализовать и перечислить равенства типов, о которых проверяет типограф и может вывести, или сделать синтаксис приведений (доказательств равенств) явным и сохранитьиграть в эту игру с поиском доказательства с ними), так что это не проверка типа:
lem = \refutation -> Refl
Может быть, есть какой-то способ создать это доказательство равенства, но тогда выражение будет начинаться с чего-то еще, что происходитбыть другим случаем доказательства.
Это может быть некоторое применение конструктора C x1 x2 ... или переменной refutation (применено или нет);но нет никакого способа, который был бы хорошо напечатан, он должен каким-то образом произвести (:~:), и Refl действительно единственный путь.
Или это может быть case,WLOG, нет ни вложенного case слева, ни какого-либо конструктора, потому что выражение может быть упрощено в обоих случаях:
-- Any left-nested case expression
case (case (e) of { C x1 x2 -> (f) }) { D y1 y2 -> (g) }
-- is equivalent to a right-nested case
case (e) of { C x1 x2 -> case (f) of { D y1 y2 -> (g) } }
-- Any case expression with a nested constructor
case (C u v) of { C x1 x2 -> f x1 x2 }
-- reduces to
f u v
Таким образом, последний подкласс является регистром переменной:
lem = \refutation -> case refutation (_hole :: x :~: y) of {}
и мы должны построить x :~: y. Перечислим способы заполнения _hole еще раз. Это либо Refl, но доказательств нет, либо (пропуская несколько шагов) case refutation (_anotherHole :: x :~: y) of {},d у нас на руках бесконечный спуск, что тоже абсурдно. Другой возможный аргумент здесь заключается в том, что мы можем извлечь case из приложения, чтобы исключить этот случай из рассмотрения WLOG.
-- Any application to a case
f (case e of C x1 x2 -> g x1 x2)
-- is equivalent to a case with the application inside
case e of C x1 x2 -> f (g x1 x2)
Больше нет случаев. Поиск завершен, и мы не нашли реализацию (x :~: y -> Void) -> Choose x y :~: 2. КЭД.
Чтобы прочитать больше по этой теме, я думаю, что курс / книга о лямбда-исчислении до тех пор, пока доказательство нормализации простого типа лямбда-исчисления не даст вам базовые инструменты для начала. Следующий тезис содержит введение по этому вопросу в первой части, но, по общему признанию, я плохо разбираюсь в сложности такого материала: Какие типы имеют уникального обитателя? Сосредоточив внимание на чистой программной эквивалентности , Габриэль Шерер.
Не стесняйтесь предлагать более адекватные ресурсы и литературу.
II. Исправление предложения и доказательство его зависимыми типами
Ваша первоначальная интуиция о том, что это должно кодировать действительное предложение, определенно верна. Как мы можем исправить это, чтобы сделать его доказуемым?
Технически, тип, на который мы смотрим, количественно определяется с помощью forall:
forall x y. (x :~: y -> Void) -> Choose x y :~: 2
Важной особенностью forall является то, что он не имеет значения квантификатор. Переменные, которые он вводит , не могут использоваться "напрямую" в терминах этого типа. Хотя этот аспект становится более заметным в присутствии зависимых типов, он все еще пронизывает Haskell сегодня , предоставляя другую интуицию, почему это (и многие другие примеры) не являются «доказуемыми» в Haskell: если вы думаете о том, почемувы думаете, что предложение является действительным, вы, естественно, начнете с разделения случая на предмет того, равно ли x равен y, но даже для такого разделения случая вам нужен способ решить с какой стороны вына который, конечно, придется взглянуть на x и y, поэтому они не могут быть неактуальными. forall в Хаскеле совсем не похоже на то, что большинство людей имеют в виду «для всех».
Некоторое обсуждение вопроса актуальности можно найти в тезисе Зависимые типы в Хаскеле ,Ричардом Айзенбергом (в частности, раздел 3.1.1.5 для начального примера, раздел 4.3 для релевантности в зависимом Haskell и раздел 8.7 для сравнения с другими языками с зависимыми типами).
Для зависимого Haskell потребуется релевантный квантификатор для дополнения forall, и который приблизил бы нас к доказательству этого:
foreach x y. (x :~: y -> Void) -> Choose x y :~: 2
Тогда мы, вероятно, могли бы написать это:
lem :: foreach x y. (x :~: y -> Void) -> Choose x y :~: 2
lem x y p = case x ==? u of
Left r -> absurd (p r) -- x ~ y, that's absurd!
Right Irrefl -> Refl -- x /~ y, so Choose x y = 2
Это также предполагаетпервоклассное понятие неравенства /~, дополняющее ~, чтобы помочь Choose уменьшить, когда оно находится в контексте и функции принятия решения (==?) :: foreach x y. Either (x :~: y) (x :/~: y). На самом деле, этот механизм не является необходимым, это просто приводит к более короткому ответу.
На данный момент я придумываю вещи, потому что Dependent Haskell еще не существует, но это легко выполнимо в связанных языках с зависимой типизацией(Coq, Agda, Idris, Lean), по модулю адекватная замена семейства типов Choose (семейства типов в некотором смысле слишком сильны, чтобы их можно было переводить как простые функции, поэтому это может быть обманом, но я отвлекся).
Вот сопоставимая программа в Coq, показывающая также, что lem применяется к 1 и 2, и подходящее доказательство сводится к доказательству с помощью рефлексивности choose 1 2 = 2.
https://gist.github.com/Lysxia/5a9b6996a3aae741688e7bf83903887b
III. Без зависимых типов
Критическим источником трудностей здесь является то, что Choose является семейством закрытых типов с перекрывающимися экземплярами. Это проблематично, потому что не существует надлежащего способа выразить тот факт, что x и y не равны в Haskell, знать, что первое предложение Choose x x не применимо.
Более плодотворный путьесли вы в псевдо-зависимом Haskell, используйте булево равенство типов:
-- In the base library
import Data.Type.Bool (If)
import Data.Type.Equality (type (==))
type Choose x y = If (x == y) 1 2
Альтернативная кодировка ограничений равенства становится полезной для этого стиля:
type x ~~ y = ((x == y) ~ 'True)
type x /~ y = ((x == y) ~ 'False)
с этим,мы можем получить другую версию предложения типа выше,выражается в текущем Haskell (где SBool - тип синглтона Bool), что, по сути, может быть прочитано как добавление предположения о том, что равенство x и y разрешимо. Это не противоречит предыдущему утверждению о «неактуальности» forall, функция проверяет логическое значение (или, скорее, SBool), которое откладывает проверку x и y для любого, кто вызывает lem.
lem :: forall x y. SBool (x == y) -> ((x ~~ y) => Void) -> Choose x y :~: 2
lem decideEq p = case decideEq of
STrue -> absurd p
SFalse -> Refl