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

Question

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

{-# 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 Char@.
intIsNotChar :: Not (Equal Int Char)
intIsNotChar intIsChar = ???

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

Так что либо:

1. Я что-то упустил или
2. Есть некоторые ограничения в языке, которые делают это невыполнимой задачей, и мне не удалось понять, что это такое.

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

Answer 1

Вот более короткая версия решения Филиппа Дж. Ф., в котором теоретики зависимого типа опровергают уравнения годами.

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 доступно, я бы рекомендовал не использовать его там, где достаточно метода total: метод total объясняет, почему что-то невозможно, и проверка типов подтверждает; undefined просто документирует ваше обещание. Действительно, этот метод опровержения - это то, как Epigram обходится без "невозможных случаев", обеспечивая при этом, чтобы анализ случая охватывал его область.

Что касается вычислительного поведения, обратите внимание, что 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"

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

Answer 2

Я не понимаю проблемы с использованием undefined в Хаскеле каждый тип обитает снизу. Наш язык не сильно нормализуется... Вы ищете не то, что нужно. 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 ()

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

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

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