从GADT存在的安全使用unsafeCoerce？

Question

说我有

{-# LANGUAGE GADTs #-}

import Unsafe.Coerce 

data Any where
    Any :: a -> Any

type Index = Int

newtype Ref a = Ref Index

mkRef :: a -> Index -> (Any, Ref a)
mkRef x idx = (Any x, Ref idx)

(any0, ref0) = mkRef "hello" 0
(any1, ref1) = mkRef 'x' 1
(any2, ref2) = mkRef (666 :: Int) 2

anys :: [Any]
anys = [any0, any1, any2]

derefFrom :: Ref a -> [Any] -> a
(Ref idx) `derefFrom` pool = case pool !! idx of
    Any x -> unsafeCoerce x

如果我只使用derefFrom适当构造的参数,这段代码会按预期工作吗？看起来如此,但我不知道可能会有什么问题.

通过适当构造的论点,我的意思是:

ref0 `derefFrom` anys
ref1 `derefFrom` anys
ref2 `derefFrom` anys

(我将通过mkRef在monad中封装使用来确保Ref使用相应的列表正确生成s来使这更安全.)

Answer 1

是; 只要你可以确定unsafeCoerce只会被调用来强制实际上是目标类型的值,那么它是安全的.

Answer 2

我不会用GADT存在主义来做这件事.这不是unsafeCoerce文档明确说的有用的用法.我会跟他们说什么去,并使用Any从GHC.Prim作为中间类型.AnyGHC在几个方面都很特别 - 其中之一就是保证每种类型的价值都能安全地往返unsafeCoerce.

但还有更多需要考虑的问题.monadic包装并不像你想象的那么简单.假设您以最简单的方式编写它,如下所示:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import qualified Data.IntMap.Strict as M

import Control.Applicative

import Control.Monad.State.Strict

import GHC.Prim (Any)
import Unsafe.Coerce


newtype Ref a = Ref Int

newtype Env a = Env (State (M.IntMap Any, Int) a)
    deriving (Functor, Applicative, Monad)


runEnv :: Env a -> a
runEnv (Env s) = evalState s (M.empty, 0)


mkRef :: a -> Env (Ref a)
mkRef x = Env $ do
    (m, c) <- get
    let m' = M.insert c (unsafeCoerce x) m
        c' = c + 1
    put (m', c')
    return $ Ref c


readRef :: Ref a -> Env a
readRef (Ref c) = Env $ do
    (m, _) <- get
    return . unsafeCoerce $ m M.! c


writeRef :: Ref a -> a -> Env ()
writeRef (Ref c) x = Env $ do
    (m, c') <- get
    let m' = M.insert c (unsafeCoerce x) m
    put (m', c')


-- a stupid example of an exceedingly imperative fib function
fib :: Int -> Env Int
fib x = do
    res <- mkRef 1
    let loop i = when (i <= x) $ do
            r <- readRef res
            writeRef res $ r * i
            loop (i + 1)
    loop 2
    readRef res


main :: IO ()
main = print $ runEnv (fib 5)

这...功能的排序,如果你正确使用它.但是有很多方法可以错误地使用它.这是一个崩溃的简单示例,但更复杂的示例可能有不正确的类型强制.

main :: IO ()
main = do
    let x = runEnv $ mkRef "Hello"
        y = runEnv $ readRef x
    print y

幸运的是,我们不需要从头开始解决这个问题 - 我们可以从历史的教训中吸取教训.ST可能有类似的问题与STRef上下文之间的值泄漏.此解决方案在这一点上是众所周知的:确保通过使用通用量化的类型变量Ref来避免s runEnv.

该代码看起来更像是这样的:

{-# LANGUAGE RankNTypes, GeneralizedNewtypeDeriving #-}

import qualified Data.IntMap.Strict as M

import Control.Applicative

import Control.Monad.State.Strict

import GHC.Prim (Any)
import Unsafe.Coerce


newtype Ref s a = Ref Int

newtype Env s a = Env (State (M.IntMap Any, Int) a)
    deriving (Functor, Applicative, Monad)


runEnv :: (forall s. Env s a) -> a
runEnv (Env s) = evalState s (M.empty, 0)


mkRef :: a -> Env s (Ref s a)
mkRef x = Env $ do
    (m, c) <- get
    let m' = M.insert c (unsafeCoerce x) m
        c' = c + 1
    put (m', c')
    return $ Ref c


readRef :: Ref s a -> Env s a
readRef (Ref c) = Env $ do
    (m, _) <- get
    return . unsafeCoerce $ m M.! c


writeRef :: Ref s a -> a -> Env s ()
writeRef (Ref c) x = Env $ do
    (m, c') <- get
    let m' = M.insert c (unsafeCoerce x) m
    put (m', c')


-- a stupid example of an exceedingly imperative fib function
fib :: Int -> Env s Int
fib x = do
    res <- mkRef 1
    let loop i = when (i <= x) $ do
            r <- readRef res
            writeRef res $ r * i
            loop (i + 1)
    loop 2
    readRef res


main :: IO ()
main = print $ runEnv (fib 5)

当然,在这一点上,我所做的只是重新实现ST.这种方法涉及证明你自己使用的unsafeCoerce是正确的,在长期运行带有短期引用的计算的情况下,不会立即收集引用,并且性能比较差ST.因此,虽然它是安全的,但对任何事情都不是一个好的解决方案.

所以,这个巨大的答案一直在问这是否是一个XY问题.你认为这是一个很好的解决方案,你想解决什么？