所以，在我不断尝试通过小哈斯克尔练习半懂咖喱霍华德，我已经得到停留在这一点上：
{-# 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 。
因此，要么：
- 我失去了一些东西，或
- 还有，使这个不可能完成的任务了语言的一些限制，我没有设法去了解它是什么。
我怀疑，答案是这样的：编译器是无法利用的事实，有没有Equal没有A = B的构造函数。 但是，如果是这样的话，让他真的吗？
这里是菲利普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"
如果诚实的反驳实在是太像辛勤工作。
我不明白，使用问题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 ()
但是，这将产生不确定的行为作为它的计算规则。 false应该会导致程序中止，或者至少是永远运行。 正在中止的计算规则是类似于通过添加不转动最小的逻辑到逻辑intiutionistic。 正确的定义是
absurdEquality e = error "you have a type error likely to cause big problems"
如在标题的问题：基本上没有。 据我所知，不等式是不是在目前的哈斯克尔实际的方式表达的。 即将更改类型的系统可能会导致这个越来越漂亮，但截至目前，我们有平等但不inequalites。
