Haskell中的异构引用相等

Question

在GHC中，IORef和STRef的等式实例基于以下原始操作：

sameMutVar# :: MutVar# s a -> MutVar# s a -> Int#

我希望能够计算异构引用相等，

sameReference :: IORef a -> IORef b -> Bool

（或者类似于具有潜在不同类型的STRefs）。是否可以使用unsafeCoerce来检查引用相等性？有没有理由说sameMutVar#没有给出异类型签名？

编辑：为了添加一些上下文，我想有这个hetereogenous指针相等，因为我想使用相等方法从IORef as列表中删除一个特定的IORef，其类型是存在量化的。

Answer 1

写作非常安全

sameReference :: IORef a -> IORef b -> Bool
sameReference = unsafeCoerce ((==) :: IORef a -> IORef a -> Bool)

对于具有类型的primop来说，这是完全合理的

sameMutVar# :: MutVar# s a -> MutVar# s b -> Int#

但是设计师显然觉得在不同类型的参考上使用该功能更可能是错误的。

你不能安全地做的是得出结论sameReference (r1 :: IORef a) (r2 :: IORef b) = True暗示a和b是相同的。假设你有

sameRefSameType :: IORef a -> IORef b -> Maybe (a :~: b)

然后你可以轻松写

oops :: Coercible a b => IORef a -> a :~: b
oops r = fromJust (sameRefSameType r (coerce r))

产生伪证据证明任何两种强制性类型都是平等的。你应该能够弄清楚如何使用GADT从那里到mkUC :: IO (a -> b)。

我相信写作是安全的

sameRefCoercibleTypes :: IORef a -> IORef b -> Maybe (Coercion a b)

既然Daniel Wagner提到了稳定的名字，我应该提一下，在这种情况下，那些情况更糟。我需要从一些背景开始。假设你写

f :: Either x Int -> Either x Bool
f (Left x) = Left x
f (Right _) = Right False

在第一种情况下，分配一个新的Left构造函数只是为了改变类型将是一种耻辱。所以GHC有一个低级优化（在核心到核心优化管道之后）试图将其转化为（基本上）

f p@(Left x) = unsafeCoerce p
f (Right _) = Right False

这意味着你可以拥有m :: Either x a和n :: Either x b，其中m和n引用相同的堆对象，尽管a和b具有完全不相关的类型。如果你为m创建一个稳定的名字，为n创建一个稳定的名字，那么那些稳定的名字将相等！如果你的假设也是如此

sameSNCoercibleTypes
  :: StableName a
  -> StableName b
  -> Maybe (Coercion a b)

然后你可以使用m和n“证明”Coercible (Either x a) (Either x b)，你可以将任何a转换成任何b。它有点微妙，但由于它可能，否则假设是不安全的。