Могут ли GADT использоваться для доказательства неравенств типов в GHC?

Итак, в моих постоянных попытках наполовину понять Карри-Говарда с помощью небольших упражнений Хаскелла, я застрял в этом пункте:

{-# LANGUAGE GADTs #-}

import Data.Void

type Not a = a -> Void

-- | The type of type equality proofs, which can only be instantiated if a = b.
data Equal a b where
    Refl :: Equal a a

-- | Derive a contradiction from a putative proof of @Equal Int [email protected]
intIsNotChar :: Not (Equal Int Char)
intIsNotChar intIsChar = ???

Очевидно, что тип Equal Int Char не имеет (не-нижних) обитателей и, следовательно, семантически должен быть функцией absurdEquality :: Equal Int Char -> a... но для жизни меня я не могу найти способ написать один кроме использования undefined.

Итак, либо:

  • Мне что-то не хватает, или
  • Существует некоторое ограничение языка, делающего эту невозможную задачу, и мне не удалось понять, что это такое.

Я подозреваю, что ответ таков: компилятор не может использовать тот факт, что нет конструкторов Equal, у которых нет a = b. Но если это так, что делает его истинным?

Ответы

Ответ 1

Здесь более короткая версия решения Philip JF, которая является методом зависимых типов, опровергала уравнения в течение многих лет.

type family Discriminate x
type instance Discriminate Int  = ()
type instance Discriminate Char = Void

transport :: Equal a b -> Discriminate a -> Discriminate b
transport Refl d = d

refute :: Equal Int Char -> Void
refute q = transport q ()

Чтобы показать, что все по-другому, вы должны поймать их по-другому, предоставляя вычислительный контекст, который приводит к отдельным наблюдениям. Discriminate предоставляет именно такой контекст: программа уровня уровня, которая обрабатывает два типа по-разному.

Нет необходимости прибегать к undefined для решения этой проблемы. Общее программирование иногда включает отказ от невозможных входов. Даже там, где доступно undefined, я бы рекомендовал не использовать его там, где достаточно полного метода: общий метод объясняет, почему что-то невозможно, и подтверждение typechecker; undefined просто документирует ваше обещание. Действительно, этот метод опровержения заключается в том, как Эпиграмм распределяет "невозможные случаи", гарантируя, что анализ случаев охватывает его домен.

Что касается вычислительного поведения, обратите внимание, что refute, через transport обязательно является строгим в q и что q не может вычислять головную форму в пустом контексте просто потому, что такая нормальная форма головы не существует ( и потому, что вычисление сохраняет тип, конечно). В общей настройке мы будем уверены, что refute никогда не будет вызываться во время выполнения. В Haskell мы, по крайней мере, уверены, что его аргумент расходится или генерирует исключение, прежде чем мы обязаны ответить на него. Ленивая версия, например

absurdEquality e = error "you have a type error likely to cause big problems"

будет игнорировать токсичность e и сказать вам, что у вас есть ошибка типа, когда вы этого не делаете. Я предпочитаю

absurdEquality e = e `seq` error "sue me if this happens"

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

Ответ 2

Я не понимаю проблемы с использованием undefined каждый тип заселен дном в Haskell. Наш язык не сильно нормализуется... Вы ищете не то. Equal Int Char приводит к ошибкам типа не очень хорошо сохранившимся исключениям. См

{-# LANGUAGE GADTs, TypeFamilies #-}

data Equal a b where
    Refl :: Equal a a

type family Pick cond a b
type instance Pick Char a b = a
type instance Pick Int a b = b

newtype Picker cond a b = Picker (Pick cond a b)

pick :: b -> Picker Int a b
pick = Picker

unpick :: Picker Char a b -> a
unpick (Picker x) = x

samePicker :: Equal t1 t2 -> Picker t1 a b -> Picker t2 a b
samePicker Refl x = x

absurdCoerce :: Equal Int Char -> a -> b
absurdCoerce e x = unpick (samePicker e (pick x))

вы можете использовать это, чтобы создать нужную функцию.

absurdEquality e = absurdCoerce e ()

но это приведет к выполнению undefined поведения в качестве его правила вычисления. false должен прерывать программы или, по крайней мере, работать навсегда. Прерывание - это правило вычисления, которое сродни превращению минимальной логики в интуитивно-понятную логику путем добавления нет. Правильное определение

absurdEquality e = error "you have a type error likely to cause big problems"

относительно вопроса в названии: по существу нет. Насколько я знаю, типовое неравенство не реализуется практично в текущем Haskell. Приход изменений в систему типов может привести к тому, что это станет лучше, но на данный момент у нас есть равенства, но не неравенства.