23

我相信以下内容与Set.mapMonotonic coerce. 即可能发生的最坏情况是我将打破Set不变量,如果ab有不同的Ord实例,我将打破不变量:

coerceSet :: Coercible a b=> Set.Set a -> Set.Set b
coerceSet = unsafeCoerce

那是对的吗?

编辑:相关功能问题Sethttps ://github.com/haskell/containers/issues/308

4

2 回答 2

12

应该是安全的。

一个 validcoerce @a @b总是可以用一个 valid 代替unsafeCoerce @a @b。为什么?因为,在核心级别,它们是相同的函数,coerce(它只是返回其输入,如id)。问题是coerce,作为论据,证明被强制的两件事具有相同的表示。对于 normal coerce,这个证明是一个实际的证明,但是对于unsafeCoerce,这个证明只是一个表示“相信我”的标记。这个证明作为类型参数传递,因此,通过类型擦除,对程序的行为没有影响。因此unsafeCoercecoerce只要两者都可能,它们就等价。

现在,这不是故事的结局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,一切都会好起来的。如果您替换coerceunsafeCoerce,调用goo将出现段错误或做其他不好的事情。

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