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

关键词：

【中文标题】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 中无法以实际的方式表示。即将对类型系统进行的更改可能会导致这种情况变得更好，但截至目前，我们有平等但没有不平等。

【讨论】：

Java中的参数化类型（GADT）

...tion<C,O>Collection<O>doAction(C<O>predicate)这样我就可以轻松地声明类classSelector<T>...然后将 查看详情

我无法让基于 GADT 的玩具动态类型与参数类型一起使用

】我无法让基于GADT的玩具动态类型与参数类型一起使用【英文标题】：Ican\'tgetmyGADT-basedtoyDynamictypetoworkwithparametrictypes【发布时间】：2012-06-1415:57:08【问题描述】：因此，为了帮助我理解一些更高级的Haskell/GHC功能和概念，我决... 查看详情

类型等式约束和多态性

】类型等式约束和多态性【英文标题】：Typeequalityconstraintsandpolymorphism【发布时间】：2021-01-0116:53:25【问题描述】：等式约束的确切语义是什么？这两种类型完全等价吗？f::Int->IO[T]g::(a~T)=>Int->IO[a]g是只对T有效的单态函数... 查看详情

Scala 中单例类型的 GADT 类型细化

】Scala中单例类型的GADT类型细化【英文标题】：GADTtyperefinementforsingletontypesinScala【发布时间】：2021-02-0218:03:58【问题描述】：我有一个简单的GADT声明如下：sealedtraitT[A]objectTcaseclassMkT[A<:StringwithSingleton](name:A)extendsT[A]现在我想编... 查看详情

我可以告诉 GHC 随意选择使用哪个实例，因为我不在乎吗？

】我可以告诉GHC随意选择使用哪个实例，因为我不在乎吗？【英文标题】：CanItellGHCtoarbitrarilyselectwhichinstancetouse,becauseIdon\'tcare?【发布时间】：2016-03-3106:09:08【问题描述】：我有一些这样的代码：-#OPTIONS_GHC-Wall#--#LANUAGEVariousLanguag... 查看详情

数据声明 Haskell 中的类型约束

...s必须是Num类型类的东西，例如Int或Double。使用Haskell和GHC可以做到吗？【问题讨论】：这是可能的，但几乎绝不是您应该做的。将Nums约束 查看详情

我可以派生一个新类型的“数据”实例吗？

】我可以派生一个新类型的“数据”实例吗？【英文标题】：CanIderiveanewtypeinstanceof`Data`?【发布时间】：2018-09-2510:55:21【问题描述】：我有一个新类型T：newtypeT=TText我想为它派生Data。所以-XGeneralizedNewtypeDeriving-XDerivingStrategies我愿... 查看详情

中断也是ghc中的异步异常吗？(代码片段)

...如果被屏蔽的线程以某种方式阻塞，则在屏蔽状态下仍然可以接收异步异常有一个不同的函数，uninterruptibleMask，它完全阻止了异步异常。默认情况下，POSIX中断信号会导致主线程中出现AsyncException。如果我理解正确，我认为这与... 查看详情

使用 Haskell 类型族或 GADT 的模块化算术？

】使用Haskell类型族或GADT的模块化算术？【英文标题】：ModularArithmeticusingHaskellType-FamiliesorGADTs?【发布时间】：2015-12-2520:28:45【问题描述】：我经常有机会在Haskell中执行模运算，其中模通常很大并且通常是素数（例如2000000011）。... 查看详情

差分约束系统相关证明（存在负环则无解证明）

先引用网上的关于差分约束的解释：一、引例1、一类不等式组的解给定n个变量和m个不等式，每个不等式形如x[i]–x[j]<=a[k](0<=i,j<n,0<=k<m，a[k]已知)，求x[n-1]–x[0]的最大值。例如当n=4，m=5，不等式组如图一-1-1所示的情... 查看详情

琴生不等式及证明

琴生不等式及证明证明使用数学归纳法证明。 查看详情

关于2-范数三角不等式的证明

...瓣上11年有同学也问了，看了评论有了思路，可以用柯西不等式。sqrt（(x1+y1)^2+...+(xn+yn)^2)=sqrt(x1^2+...+xn^2+y1^2+...+yn^2+2*x1*y1+...+2*xn*yn)<=sqrt(x1^2+...+xn^2+y1^2+...+yn^2+?2*sqrt(x1^2+...+xn^2)*sqrt 查看详情

函数返回gadt的任何构造函数的结果(代码片段)

...为它已经推断出a是TFoo。但是，这是令人惊讶的，因为您可以使用常规总和类型：dataThing=FooInt|BarStringcombine::[Thing]combine=[Foo1,Bar"abc"]无论如何返回GADT参数的类型参数？在人为例子的背景之外，我需要GADT，所以我可以输入某些函数... 查看详情

pinsker不等式的简单证明

Pinsker不等式的简单证明网上有很多很多关于Pinsker不等式的证明方法，但是我没有看到一个用数学归纳法证明的，也没有看到一个不加先验定义的自包含的证明。下面我给出一个关于一个极简的证明。任何的引用请注明本... 查看详情

pinsker不等式的简单证明

Pinsker不等式的简单证明网上有很多很多关于Pinsker不等式的证明方法，但是我没有看到一个用数学归纳法证明的，也没有看到一个不加先验定义的自包含的证明。下面我给出一个关于一个极简的证明。任何的引用请注明本... 查看详情

mt33证明琴生不等式

解答：这里数学归纳法证明时指出关键的变形.评:撇开琴生不等式自身的应用和意义外，单单就这个证明也是一道非常不错的练习数学归纳法的经典题目。 查看详情

Ghc：部分编译 Haskell 代码？

...型错误，所有表达式都会加载到ghc解释器中。很不错：我可以和:t一起玩弄各种表情的类型。我的问题是：如果某处有一个小错误，ghci就无法加载任何东西（甚至导入的模块都不能加载！！），这使 查看详情

mt19舒尔不等式设计理念及证明

评：舒尔的想法是美妙的，当然他本身也有很多意义，在机械化证明的理念里，它也占据了一方田地。 查看详情