是否可以在自定义类型和标准库类型之间建立 Coercible 实例?

问题描述

举个简单的例子,假设我想要一个类型来表示井字游戏标记

data Mark = Nought | Cross

Bool 相同的

Prelude> :info Bool
data Bool = False | True    -- Defined in ‘GHC.Types’

但是它们之间没有 Coercible Bool Mark ,即使我导入 GHC.Types 也没有(我最初认为 GHC 可能需要 Bool 的定义位置可见),这是唯一的方法此实例似乎是通过 newtype

也许我可以用双向模式定义 newtype Mark = Mark Bool 并定义 NoughtCross,我希望有比这更简单的东西。

解决方法

不幸的是,你运气不好。作为 documentation for Data.Coerce explains,“可以假设存在以下三种实例:”

  • 自实例,如instance Coercible a a

  • 用于在表示或幻像类型参数不同的数据类型的两个版本之间进行强制的实例,如 instance Coercible a a' => Coercible (Maybe a) (Maybe a')

  • 新类型之间的实例。

此外,“尝试手动声明 Coercible 的实例是错误的”,这就是您所得到的。任意不同的数据类型之间没有实例,即使它们看起来相似。


这可能看起来令人沮丧,但请考虑这一点:如果在 CoercibleBool 之间有一个 Mark 实例,是什么阻止它强制 Nought 到 {{1 }} 和 TrueCross?可能 FalseBool 在内存中以相同的方式表示,但不能保证它们在语义上足够相似以保证 Mark 实例。


您使用 newtype 和模式同义词的解决方案是一种很好的、​​安全的解决问题的方法,即使它有点烦人。

另一种选择是考虑使用 Coercible。例如,从 this other question

查看 Generic 的想法 ,

这是不可能的,模式同义词现在是一个很好的解决方案。我经常使用这样的代码来为恰好与现有原始类型同构的类型派生有用的实例。

module Mark
  ( Mark(Nought,Cross)
  ) where

newtype Mark = Mark Bool
  deriving stock (…)
  deriving newtype (…)
  deriving (…) via Any
  …

pattern Nought = Mark False
pattern Cross = Mark True

无关 ADT 之间的强制也不在 list of permitted unsafe coercions 上。最后我知道,在 GHC 的实践中,MarkBool 之间的强制转换只有在相关值被完全评估时才会起作用,因为它们的构造函数数量很少,所以构造函数索引存储在运行时指针的标记位。但是不能可靠地强制类型为 MarkBool 的任意 thunk,并且该方法不能推广到具有多于 {4,8} 个构造函数的类型(分别针对 {32,64 }-位系统)。

此外,对象的代码生成器和运行时表示都会定期更改,因此即使现在可以使用(我不知道),将来也可能会崩溃。

我希望我们在未来得到一个通用的 Coercible,它可以容纳更多的强制,而不仅仅是 newtype-of-TT,甚至更好,这允许我们为数据类型指定稳定的 ABI。据我所知,没有人在 Haskell 中积极致力于这方面的工作,尽管在 Rust 中为 safe transmute 进行了一些类似的工作,所以也许有人会将其走私回功能区。

(说到 ABI,您可以为此使用 FFI,而且我已经在编写外部代码并且知道 Storable 实例匹配的情况下这样做了。{ {3}} 一个适当大小的缓冲区,alloca 一个类型为 Bool 的值,poke Ptr Bool 到一个 Ptr MarkcastPtr Markpeek 整个shebang。)

,

Coercible Bool Mark 不是必需的。 Mark-instances 可以通过没有它的 Bool 派生。

Generic 类型的泛型表示 (Rep) 是 Coercible 可以相互转换:

   from           coerce              to
A -----> Rep A () -----> Rep Via () -----> Via 

对于数据类型 Mark 这意味着可以通过 Eq 的实例派生实例 (Bool,..)。

type Mark :: Type
data Mark = Nought | Cross
 deriving
 stock Generic

 deriving Eq
 via Bool <-> Mark

Bool <-> Mark 是如何工作的?

type    (<->) :: Type -> Type -> Type
newtype via <-> a = Via a

首先,我们捕获可以在两种类型的通用表示之间coerce 的约束:

type CoercibleRep :: Type -> Type -> Constraint
type CoercibleRep via a = (Generic via,Generic a,Rep a () `Coercible` Rep via ())

给定这个约束,我们可以从 a 移动到它的 via 类型,创建中间 Reps:

translateTo :: forall b a. CoercibleRep a b => a -> b
translateTo = from @a @() >>> coerce >>> to @b @()

现在我们可以轻松地为这种类型编写一个 Eq 实例,我们假设一个 Eq via 实例用于 via 类型(在我们的例子中为 Bool

instance (CoercibleRep via a,Eq via) => Eq (via <-> a) where
 (==) :: (via <-> a) -> (via <-> a) -> Bool
 Via a1 == Via a2 = translateTo @via a1 == translateTo @via a2

Semigroup 的实例需要将 via 转换回 a

instance (CoercibleRep via a,Semigroup via) => Semigroup (via <-> a) where
 (<>) :: (via <-> a) -> (via <-> a) -> (via <-> a)
 Via a1 <> Via a2 = Via do
  translateTo @a do
     translateTo @via a1 <> translateTo @via a2

现在我们可以推导出 EqSemigroup

-- >> V3 "a" "b" "c" <> V3 "!" "!" "!"
-- V3 "a!" "b!" "c!"
type V4 :: Type -> Type
data V4 a = V4 a a a a
 deriving
 stock Generic

 deriving (Eq,Semigroup)
 via (a,a,a) <-> V4 a

从一开始就使用 newtype 可以避免这种样板文件,但是一旦它启动就可以重复使用。编写一个新类型并使用模式同义词来掩盖它很简单。