使用'unsafeCoerce'

Question

在Haskell中,有一个名为的函数unsafeCoerce,可以将任何东西变成任何其他类型的东西.这究竟用于什么？比如,为什么我们要以这种"不安全"的方式将事物转化为彼此？

提供unsafeCoerce实际使用方式的示例.Hackage的链接会有所帮助.某些问题中的示例代码不会.

Answer 1

unsafeCoerce让你说服你喜欢的任何属性的类型系统.因此,当您完全确定您声明的属性是真的时,它就是"安全的".所以,例如:

unsafeCoerce True :: Int

是一种违规行为,可能导致不稳定,糟糕的运行时行为.

unsafeCoerce (3 :: Int) :: Int

(显然)很好,不会导致运行时错误行为.

那么什么是非平凡的用途unsafeCoerce？假设我们有一个类型类绑定的存在类型

module MyClass ( SomethingMyClass (..), intSomething ) where

class MyClass x where {}

instance MyClass Int where {}

data SomethingMyClass = forall a. MyClass a => SomethingMyClass a

我们也可以说,这里注意的是,类型类MyClass是没有出口,因此没有其他人都不能创建它的实例.实际上,Int唯一可以实例化它的东西,也是唯一能够实现它的东西.

现在,当我们模式匹配以破坏一个值时,SomethingMyClass我们将能够从内部拉出"某物"

foo :: SomethingMyClass -> ...
foo (SomethingMyClass a) =
  -- here we have a value `a` with type `exists a . MyClass a => a`
  --
  -- this is totally useless since `MyClass` doesn't even have any
  -- methods for us to use!
  ...

现在,在这一点上,正如评论所暗示的那样,我们提取的价值没有类型信息 - 它被存在主义背景"遗忘"了.它可能绝对是实例化的任何东西MyClass.

当然,在这种非常特殊的情况下,我们知道唯一实现的MyClass是Int.所以我们的价值实际上a必须有类型.我们永远无法说服typechecker这是真的,但由于外部证据我们知道它是.Int

因此,我们可以(非常仔细)

intSomething :: SomethingMyClass -> Int
intSomething (SomethingMyClass a) = unsafeCoerce a    -- shudder!

现在,希望我已经建议这是一个可怕的,危险的想法,但它也可能会尝试我们可以利用什么样的信息来了解类型检查者无法做到的事情.

在非病理情况下,这种情况很少见.甚至更罕见的情况是使用我们所知道的东西而且类型识别器本身并不是病态的.在上面的例子中,我们必须完全确定没有人会扩展我们的MyClass模块以实例化更多类型,MyClass否则我们的使用unsafeCoerce会立即变得不安全.

> instance MyClass Bool where {}
> intSomething (SomethingMyClass True)
6917529027658597398

看起来我们的编译器内部漏洞了!

这种行为可能有价值的一个更常见的例子是使用newtype包装器时.我们可能会在newtype包装器中包装一个类型以专门化其instance定义,这是一个相当普遍的想法.

例如,Int没有Monoid定义,因为Ints 上有两个自然的幺半:sums和products.相反,我们使用newtype包装器更明确.

newtype Sum a = Sum { getSum :: a }

instance Num a => Monoid (Sum a) where
  mempty = Sum 0
  mappend (Sum a) (Sum b) = Sum (a+b)

现在,通常编译器非常聪明,并且认识到它可以消除所有这些Sum构造函数,以便生成更高效的代码.可悲的是,有时它不能,特别是在高度多态的情况下.

如果你(a)知道某些类型a实际上只是一个newtype-wrapped b并且(b)知道编译器无法推断出它本身,那么你可能想要做

unsafeCoerce (x :: a) :: b

为了略微提高效率.例如,这经常发生在lens并且在其依赖性的Data.Profunctor.Unsafe模块中表达.profunctorslens

但是让我再次建议你真的需要知道在使用之前发生了什么这样的事情unsafeCoerce是非常不安全的.

最后要比较的是"类型安全cast" Data.Typeable.这个功能看起来有点像unsafeCoerce,但有更多的仪式.

unsafeCoerce ::                             a ->       b
cast         :: (Typeable a, Typeable b) => a -> Maybe b

其中,您可能会认为使用的unsafeCoerce是一个不可伪造的函数typeOf :: Typeable a => a -> TypeRep,TypeRep它是反映值类型的运行时令牌.然后我们有

cast :: (Typeable a, Typeable b) => a -> Maybe b
cast a = if (typeOf a == typeOf b) then Just b else Nothing 
  where b = unsafeCoerce a

因此,cast能够确保运行时的类型a和b 实际上是相同的,并且Nothing如果不是,则可以决定返回.举个例子:

{-# LANGUAGE DeriveDataTypeable        #-}
{-# LANGUAGE ExistentialQuantification #-}

data A = A deriving (Show, Typeable)
data B = B deriving (Show, Typeable)

data Forget = forall a . Typeable a => Forget a

getAnA :: Forget -> Maybe A
getAnA (Forget something) = cast something

我们可以运行如下

> getAnA (Forget A)
Just A
> getAnA (Forget B)
Nothing

因此,如果我们将这种用法cast与我们进行比较,unsafeCoerce我们就会发现它可以实现一些相同的功能.特别是,它允许我们重新发现可能已被遗忘的信息ExistentialQuantification.但是,cast在运行时手动检查类型以确保它们真正相同,因此不能不安全地使用.为此,它要求源类型和目标类型允许通过Typeable类运行时反映其类型.

Answer 2

我唯一被迫使用的unsafeCoerce是有限的自然数.

{-# LANGUAGE DataKinds, GADTs, TypeFamilies, StandaloneDeriving #-}

data Nat = Z | S Nat deriving (Eq, Show)

data Fin (n :: Nat) :: * where
    FZ :: Fin (S n)
    FS :: Fin n -> Fin (S n)

deriving instance Show (Fin n)

Fin n是一种单链接的数据结构,静态地确保它小于n参数化的类型级自然数.

-- OK, 1 < 2 
validFin :: Fin (S (S Z))
validFin = FS FZ

-- type error, 2 < 2 is false
invalidFin :: Fin (S (S Z))
invalidFin = FS (FS FZ)

Fin可用于安全地索引到各种数据结构.它在依赖类型语言中非常标准,但不在Haskell中.

有时候,我们要转换的值Fin n来Fin m这里m大于n.

relaxFin :: Fin n -> Fin (S n)
relaxFin FZ     = FZ
relaxFin (FS n) = FS (relaxFin n)

relaxFin根据定义,它是一个无操作,但是要检查的类型仍然需要遍历该值.所以我们可能只是用unsafeCoerce而不是relaxFin.通过强制包含Fin-s的较大数据结构可以产生更明显的速度提升(例如,您可以使用Fin-s作为绑定变量的lambda项).

这是一个不可否认的异乎寻常的例子,但我发现这很有意思,它非常安全:我无法想到外部库或安全用户代码的方法来搞砸它.我可能错了,我很想知道潜在的安全问题.