23

我相信以下内容与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

4

2 回答 2

12

这应该是安全的。

一个 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具有相同的表示），则。因此，从单独的定义来看，应该在 上工作，因此您应该是安全的。图书馆必须使用特定的bCoercibleSet a ~#R Set bSetcoerce SetunsafeCoerce containers

type role Set nominal

为了向世界隐藏这个事实，人为地禁用coerce. 但是，您永远不能禁用unsafeCoerce，并且重申unsafeCoerce（在这种情况下）是安全的。

（请注意 theunsafeCoerce和 thecoerce具有相同的类型！请参阅@dfeuer 的答案以获取“过度热心”类型推断使所有内容都变形的情况的示例。）

于 2019-09-17T00:25:20.293 回答
6

是的，这在典型的现实情况下应该是安全的。但是，有可能想出一些人为的例子，但事实并非如此。这是一个使用默认值的方法。我想可能可以使用重叠实例或其他古怪的功能来做类似的事情，但我不知道。

{-# 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将出现段错误或做其他不好的事情。

于 2019-09-17T01:16:00.630 回答