unsafeVacuous，#.和.#什么时候不安全？

Question

unsafeVacuous in Data.Void.Unsafe和#. in Data.Profunctor.Unsafe都警告使用这些函数与属于GADT的函子/终止函子的危险性。一些危险的例子是显而易见的：

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进行操作，但面对这些不安全的函数时，是否有可能构造出遵守函子/终止函数定律的有用函数？

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。