Итак, в моих постоянных попытках наполовину понять Карри-Говарда с помощью небольших упражнений Хаскелла, я застрял в этом пункте:
{-# 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. Но если это так, что делает его истинным?