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

所以，在我不断尝试通过小哈斯克尔练习半懂咖喱霍华德，我已经得到停留在这一点上：GADT可以用来证明GHC中的类型不等式吗？

{-# 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 [email protected] 
intIsNotChar :: Not (Equal Int Char) 
intIsNotChar intIsChar = ???

显然类型Equal Int Char无（无底）居民，因此在语义上应该有一个absurdEquality :: Equal Int Char -> a函数......但在我的生活中，我找不到任何方法来编写除undefined以外的其他方法。

因此，要么：

我失去了一些东西，或
没有使这个不可能完成的任务了语言的一些限制，我没有设法去了解它是什么。

我怀疑答案是这样的：编译器无法利用的事实，即没有a = b的构造函数Equal。但是，如果是这样，是什么原因呢？

来源

2013-01-11 Luis Casillas

请参阅：http://typesandkinds.wordpress.com/2012/12/01/decidable-propositional-equality-in-haskell/ – glaebhoerl

@dbaupp：不是重复的 - 该问题不是试图做任何事情一个不平等的证明。 –

@ C.A.McCann，嗯，我想我应该仔细阅读，然后才开始肆意指责。 :) – huon

下面是菲利普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中，我们至少可以确定，在我们必须回应它之前，它的论点会发生分歧或抛出异常。一个懒版本，如

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-11 11:35:57 pigworker

请注意，seq e（错误“起诉我，如果发生这种情况”）可以评估第一个参数之前的第二个参数，如果这是一个问题，你可以使用'pseq'（http://hackage.haskell.org /package/base-4.9.1.0/docs/Prelude.html#v:seq）。 – sdcvvc

我不明白使用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-11 07:19:25

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

回答

相关问题