GADT 可以用来证明 GHC 中的类型不等式吗？

Posted 2023-05-08

【中文标题】GADT 可以用来证明 GHC 中的类型不等式吗？

【英文标题】：Can GADTs be used to prove type inequalities in GHC?

【发布时间】：2012-12-25 17:51:46

【问题描述】：

所以，在我不断尝试通过小型 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。

所以要么：

我错过了什么，或者 语言的某些限制使这项任务成为一项不可能完成的任务，我还没有设法理解它是什么。

我怀疑答案是这样的：编译器无法利用没有没有 a = b 的 Equal 构造函数这一事实。但如果是这样，那它是真的吗？

【问题讨论】：

见：typesandkinds.wordpress.com/2012/12/01/…

@dbaupp：不是重复的——这个问题并没有试图用不等式证明做任何事情。

@C.A.McCann，啊，是的，我想我应该更仔细地阅读，然后再开始胡乱指责。 :)

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

至于计算行为，请注意refute，通过transport 在q 中必然是严格的，并且q 不能在空上下文中计算到头范式，仅仅是因为不存在这样的头范式（当然，因为计算保留了类型）。在总体设置中，我们确信refute 永远不会在运行时被调用。在 Haskell 中，我们至少可以确定它的论点会发生分歧或抛出异常，然后我们才有义务对其作出响应。 lazy 版本，如

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

会忽略e 的毒性，并告诉你你有一个类型错误，而你没有。我更喜欢

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

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

【讨论】：

请注意seq e (error "sue me if this happens") 可以在第一个参数之前评估第二个参数，如果这是一个问题，您可以使用pseq (hackage.haskell.org/package/base-4.9.1.0/docs/…)。

【参考方案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 ()

但这将产生未定义的行为作为其计算规则。 false 应该导致程序中止，或者至少永远运行。中止是类似于通过加非将最小逻辑变成直觉逻辑的计算规则。正确的定义是

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

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