就在什么时候不安全,#.和.#unsafe？

Question

unsafeVacuous在Data.Void.Unsafe与.#和#.在Data.Profunctor.Unsafe两个警告有关使用这些函数与函子/是GADTs profunctors的危险.一些危险的例子很明显:

data Foo a where
  P :: a -> Foo a
  Q :: Foo Void

instance Functor Foo where
  fmap f (P x) = P (f x)
  fmap f Q = P (f undefined)

这里,unsafeVacuous Q将生成Q一个伪造类型的构造函数.

这个例子并不是很麻烦,因为它看起来并不像一个合理的Functor实例.有例子吗？特别是,当仅使用他们的公共API进行操作时,是否有可能构建遵循functor/profunctor法则的有用的那些,但面对这些不安全的函数可能会破坏性？

Answer 1

我不相信有任何真正的函子unsafeVacuous会导致问题。但如果你写得不好，Functor你可以自己制作unsafeCoerce，这意味着它应该被标记为{-# LANGUAGE Unsafe #-}。无效中有一个关于它的问题。

这是unsafeCoerce我想出的

{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
import Data.Void
import Data.Void.Unsafe

type family F a b where
  F a Void = a
  F a b    = b

data Foo a b where
  Foo :: F a b -> Foo a b

instance Functor (Foo a) where
  fmap = undefined

unsafeCoerce :: forall a b. (F a b ~ b) => a -> b
unsafeCoerce a = (\(Foo b) -> b) $ (unsafeVacuous (Foo a :: Foo a Void) :: Foo a b)

main :: IO ()
main = print $ (unsafeCoerce 'a' :: Int)

打印97.