22

因此，在我不断尝试通过小型 Haskell 练习对 Curry-Howard 理解一半的过程中，我被困在了这一点上：

{-# 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 的构造函数这一事实。但如果是这样，那它是真的吗？

4

2 回答 2

22

这是 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可用的地方，我也建议不要在总方法足够的情况下使用它：总方法解释了为什么某事是不可能的并且类型检查器确认；undefined只是记录你的承诺。事实上，这种反驳方法就是 Epigram 如何在确保案例分析涵盖其领域的同时摒弃“不可能的案例”。

至于计算行为，请注意refute, viatransport必须严格，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"

如果诚实的反驳太像努力工作。

于 2013-01-11T11:35:57.207 回答
7

我不明白使用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应该导致程序中止，或者至少永远运行。中止是类似于通过加非将最小逻辑变成直觉逻辑的计算规则。正确的定义是

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

至于标题中的问题：基本上没有。据我所知，类型不等式在当前的 Haskell 中无法以实际的方式表示。即将对类型系统进行的更改可能会导致这种情况变得更好，但截至目前，我们有平等但没有不平等。

于 2013-01-11T07:19:25.603 回答