假定单位类型相等是否安全？

Question

假设所有类型的()都是一样的吗？也就是说，可以使用以下方式来打破类型安全性？

-- Bad postulate 
unitsEqual :: (x ::()) :~: (y ::()) 
unitsEqual = unsafeCoerce (Refl :: '() :~: '()) 

Answer 1

这在GHC 7.8.3（见下面的代码）下是不安全的。如user2407038注释，GHC 7.10.3拒绝以下内容。毫不奇怪，这个数据族足够邪恶，以至于检查器被改为禁止它。我仍然在试着看7.10.3下是否有办法做到这一点。

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 

module UnitsEqual where 
import Unsafe.Coerce 
import Data.Type.Equality 

data family Yeah (a ::()) b c 
data instance Yeah '() b c = Yeah { yeah :: b } 
data instance Yeah a b c = Nope c 

-- Entirely valid 
castYeah :: x :~: y -> Yeah x p q -> Yeah y p q 
castYeah Refl x = x 

-- Bad postulate 
unitsEqual :: (x ::()) :~: (y ::()) 
unitsEqual = unsafeCoerce (Refl :: '() :~: '()) 

-- Oh no! This doesn't actually cast, but 
-- it's horrible enough. It consistently produces 
-- either segmentation faults or nonsense, 
-- whether the types are the same or not. 
uc :: a -> b 
uc a = yeah $ castYeah unitsEqual (Nope a) 

我 相信，但是，它 是安全地假定

voidsEqual :: (a :: Void) :~: (b :: Void) 

，因为有区分任何卡住/假类型居住 Void的没有明显的方法。

Answer 2

声明：这个答案主要是猜测，因为这种行为让我很困惑，我仍然不太确定类型检查器中的Any的语义。

在你的榜样，无论是Yeah可能被拒绝，当它计算它发现一个模棱两可的类型变量，它实例来Any的Nope a类型。这是使得例如length []工作。

你可以做同样的一个GADT，这是在GHC 7.10受理：

data Yeah (a ::()) b c where 
    Yeah :: b -> Yeah '() b c 
    Nope :: c -> Yeah Any b c 

要写入uc你需要一个功能

yeah :: Yeah '() b c -> b 
yeah (Yeah a) = a 
yeah (Nope _) = error "???" 

在第二种情况下，平等'() ~ Any是给出的，我认为是平凡的错误，例如'True ~ 'False，Int ~ Bool等typechecker知道这些事实：

okay :: 'True :~: 'False -> x 
-- okay Refl = error "???" -- Compiler rejects this case 
okay x = case x of 

但不是这一个！

really :: Any :~: '() -> x 
really Refl = error "???" -- Perfectly valid pattern match 

你不能真正调用这个函数：

>:t really Refl 

<interactive>:1:8: Warning: 
    Couldn't match type `Any' with '() 
    Expected type: Any :~: '() 
     Actual type: '() :~: '() 
    In the first argument of `really', namely `Refl' 
    In the expression: really Refl 

同时uc typechecks（定义不变），它不再打破：

>uc 'a' :: Int 
*** Exception: ??? 

这似乎是在typechecker做不相信'() :~: Any是无人居住的，因为它不是，因为typechecker是内部允许产生这样的证明，但用户仍然禁止来回自己写它。

这一切，说：我认为，如果你假装Any不存在，那么unitsEqual是合理的，并且不健全从Any存在就产生了。这似乎是由反假明确 - Any :~: '() - 但似乎是Any，说x ~ y是平凡假只有x和y是不同的类型也不x或y是Any特殊typechecker规则。

voidEqual同样是不合理的，因为Any :: Void，Any Any :: Void，Any Any Any :: Void等