我相信以下内容与Set.mapMonotonic coerce
. 即可能发生的最坏情况是我将打破Set
不变量,如果a
或b
有不同的Ord
实例,我将打破不变量:
coerceSet :: Coercible a b=> Set.Set a -> Set.Set b
coerceSet = unsafeCoerce
那是对的吗?
编辑:相关功能问题Set
:https ://github.com/haskell/containers/issues/308
我相信以下内容与Set.mapMonotonic coerce
. 即可能发生的最坏情况是我将打破Set
不变量,如果a
或b
有不同的Ord
实例,我将打破不变量:
coerceSet :: Coercible a b=> Set.Set a -> Set.Set b
coerceSet = unsafeCoerce
那是对的吗?
编辑:相关功能问题Set
:https ://github.com/haskell/containers/issues/308
这应该是安全的。
一个 validcoerce @a @b
总是可以用一个 valid 代替unsafeCoerce @a @b
。为什么?因为,在核心级别,它们是相同的函数,coerce
(它只是返回其输入,如id
)。问题是coerce
,作为论据,证明被强制的两件事具有相同的表示。对于 normal coerce
,这个证明是一个实际的证明,但是对于unsafeCoerce
,这个证明只是一个表示“相信我”的标记。这个证明作为类型参数传递,因此,通过类型擦除,对程序的行为没有影响。因此unsafeCoerce
,coerce
只要两者都可能,它们就等价。
现在,这不是故事的结局Set
,因为在 .coerce
上不起作用Set
。为什么?让我们看看它的定义。
data Set a = Bin !Size !a !(Set a) !(Set a) | Tip
从这个定义中,我们看到a
没有出现在任何类型等式等内部。这意味着我们在Set
: if a ~#R b
(如果与-<code>~#R is unboxeda
具有相同的表示),则。因此,从单独的定义来看,应该在 上工作,因此您应该是安全的。图书馆必须使用特定的b
Coercible
Set a ~#R Set b
Set
coerce
Set
unsafeCoerce
containers
type role Set nominal
为了向世界隐藏这个事实,人为地禁用coerce
. 但是,您永远不能禁用unsafeCoerce
,并且重申unsafeCoerce
(在这种情况下)是安全的。
(请注意 theunsafeCoerce
和 thecoerce
具有相同的类型!请参阅@dfeuer 的答案以获取“过度热心”类型推断使所有内容都变形的情况的示例。)
是的,这在典型的现实情况下应该是安全的。但是,有可能想出一些人为的例子,但事实并非如此。这是一个使用默认值的方法。我想可能可以使用重叠实例或其他古怪的功能来做类似的事情,但我不知道。
{-# language GADTs, TypeOperators, ExistentialQuantification #-}
import Data.Coerce
import Unsafe.Coerce
import Data.Type.Equality
data Buh a = Buh (a :~: Rational) a
data Bah = forall a. Bah (a :~: Rational) a
instance Show Bah where
show (Bah Refl x) = show x
goo :: Rational -> Bah
goo x = case coerce p of
Buh pf m ->
let _q = truncate m
in Bah pf 12
where
p = Buh Refl x
如果你打电话goo
,一切都会好起来的。如果您替换coerce
为unsafeCoerce
,调用goo
将出现段错误或做其他不好的事情。