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

Question

因此,在我不断尝试通过小型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 的事实.但如果是这样,那是什么让它成真呢？

Answer 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可用的地方,我建议不要在总方法足够的情况下使用它:总方法解释了为什么某些东西是不可能的,并且typechecker确认了; undefined只记录你的承诺.实际上,这种反驳方法是Epigram如何免除"不可能的案例",同时确保案例分析涵盖其领域.

至于计算行为,请注意refute,via 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"

如果诚实的反驳太过艰苦了.

Answer 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应该导致程序中止,或者至少可以运行.中止是一种计算规则,类似于通过添加not而将最小逻辑转换为语言逻辑.正确的定义是

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

关于标题中的问题:基本上没有.据我所知,类型不等式在当前的Haskell中不能用实际的方式表示.类型系统的改变可能导致这种情况越来越好,但截至目前,我们有平等但不平等.