确保两个 (G) ADT 在 (GHC) Haskell 中具有相同的底层表示

Posted 2023-04-18

【中文标题】确保两个 (G) ADT 在 (GHC) Haskell 中具有相同的底层表示

【英文标题】：Ensuring that two (G)ADTs have the same underlying representation in (GHC) Haskell

【发布时间】：2021-02-02 14:06:34

【问题描述】：

在 Haskell 中，有时出于性能考虑，人们会使用 unsafeCoerce（或更安全的 coerce）在具有相同内部表示的类型之间进行转换。我所知道的最常见的例子是新类型列表：

newtype Identity a = Identity a

f :: [Identity a] -> [a]
f = coerce

现在，我正在处理的代码库中有两个 GADT，看起来像这样精简：

data Typ where
    PredT :: Typ
    ProcT :: [Typ] -> Typ
    IntT :: Typ
    ListT :: Typ -> Typ


data HKTyp v (f :: * -> * -> *) where
    HKPredT :: HKTyp v f
    HKProcT :: [HKTyp v f] -> HKTyp v f
    HKIntT :: HKTyp v f
    HKListT :: f v (HKTyp v f) -> HKTyp v f  

我需要这些类型不同（而不是使用后者作为前者的概括），因为单例库（或至少模板 haskell 函数）不喜欢更高种类的数据。现在，因为我必须将这些类型分开，所以我希望它们之间有一些转换函数：

newtype Id v a = Id a

promoteHK :: Typ -> HKTyp v Id
promoteHK PredT = HKPredT
promoteHK (ProcT ts) = HKProcT (fmap promoteHK ts)
promoteHK IntT = HKIntT
promoteHK (ListT x) = HKListT (Id $ promoteHK x)

demoteHK :: HKTyp v Id -> Typ
demoteHK HKPredT = PredT
demoteHK (HKProcT (Id ts)) = ProcT (fmap demoteHK ts)
demoteHK HKIntT = IntT
demoteHK (HKListT (Id x)) = HKListT x

这些写起来很机械，但这不是问题。

虽然我确信在许多情况下，GHC 可以在编译时内联和 beta-reduce demoteHK 和 promoteHK 的应用程序，因此不会导致执行这些转换的任何运行时成本，但我真的希望能够写

f :: [Typ] -> [HKTyp v Id]
f = coerce

为了避免遍历数据结构，因为这些类型非常相似，因此（我假设）应该在内存中具有相同的底层表示。

我的问题有两个。

这些类型实际上在 GHC 中具有相同的内存表示吗？ GHC 中是否对 (G)ADT 在内存中的布局方式提供了强有力的保证，以使您通常可以执行此类操作？

【问题讨论】：

@chi 是的，很好。我已经更正了。

我很想在这两种类型之间尝试unsafeCoerce，看看是否会导致崩溃。如果可以的话，它们有不同的运行时表示。否则，无法得出明确的结论。不多，但总比没有好。我怀疑当前的 GHC 使用相同的表示并且强制是安全的，但是 GHC 开发人员不想保证永远都是这种情况（？）

@chi 查看#unsafeCoerce 的文档，情况似乎确实如此。如果 GHC 开发人员保证了这个用例，我想它会在那里记录。这似乎是未来不太可能改变的事情（即标记的联合在内部按列出的构造函数的顺序使用标签），因此可能值得提出 GHC 建议，将此案例包含在Data.Coerce 系统中，这样unsafeCoerce 不必使用。

回答我的问题 1，在 GHCI 上进行测试，这些类型似乎具有相同的表示。

也许您的代码库版本是 GADT，但您显示的 data decls 使用 GADT 语法但不是 GADT。也就是说，构造函数 sigs all end ... -> Typ resp ... -> HKTyp v f （并且没有限制）。

【参考方案1】：

我还没有测试过下面的性能，可能GHC已经够复杂了，实际上不能优化它，但是它会让我们构建一个更好的工具。这个想法是使用Generics。

计划是定义一个类型类，它强制具有相同Generic 结构的两种类型以及一个使用该类的函数。考虑以下几点：

-# LANGUAGE DeriveGeneric #-
import GHC.Generics

class GenericCoerce a b where
  genericCoerce' :: a x -> b x

genericCoerce :: (Generic x, Generic y, GenericCoerce (Rep x) (Rep y)) => x -> y
genericCoerce = to . genericCoerce' . from

当然，我们仍然需要定义使两个Reps 具有强制力的原因，但就像您的promoteHK 和demoteHK 定义一样，这有点机械：

-# LANGUAGE LambdaCase #-
-# LANGUAGE EmptyCase #-

instance GenericCoerce V1 V1 where
  genericCoerce' = \case

instance GenericCoerce U1 U1 where
  genericCoerce' = id

instance (GenericCoerce f f', GenericCoerce g g') => GenericCoerce (f :+: g) (f' :+: g') where
  genericCoerce' (L1 x) = L1 (genericCoerce' x)
  genericCoerce' (R1 x) = R1 (genericCoerce' x)

instance (GenericCoerce f f', GenericCoerce g g') => GenericCoerce (f :*: g) (f' :*: g') where
  genericCoerce' (x :*: y) = genericCoerce' x :*: genericCoerce' y

instance GenericCoerce cs1 cs2 => GenericCoerce (M1 t m cs1) (M1 t m' cs2) where
  genericCoerce' (M1 x) = M1 (genericCoerce' x)

instance (Generic x, Generic y, GenericCoerce (Rep x) (Rep y)) => GenericCoerce (K1 t x) (K1 t y) where
  genericCoerce' (K1 x) = K1 (genericCoerce x)

这实际上适用于非常基本的情况！考虑如下数据类型：

data Foo = Bar | Baz
  deriving (Generic, Show)

我们得到了我们想要的行为：

> genericCoerce @Bool @Foo True
Baz

> genericCoerce @Foo @Bool Bar
False

但是，这种Generic 强制执行方式的问题在于，它与普通 强制数据类型的方式不能很好地配合。具体来说，给定类型的类型代表和包装在新类型包装器中的该类型的类型代表不相同。

一种可能的解决方案是使用（喘气）不连贯的实例。这对你来说可能有点过分，但如果你对它们没意见，请考虑以下两个额外的实例：

-- instances to handle newtype constructor
instance -# INCOHERENT #- (Generic x, Rep x ~ D1 m x', GenericCoerce x' y) => GenericCoerce (C1 m2 (S1 m3 (Rec0 x))) y where
  genericCoerce' = genericCoerce' . unM1 . from . unK1 . unM1 . unM1

instance -# INCOHERENT #- (Generic y, Rep y ~ D1 m y', GenericCoerce x y') => GenericCoerce x (C1 m2 (S1 m3 (Rec0 y))) where
  genericCoerce' = M1 . M1 . K1 . to . M1 . genericCoerce'

这两个实例专门针对其中一种类型具有新类型包装器的情况。不连贯的实例被认为是危险的，如果你的强制中有很多嵌套类型/新类型，那么可能会出现问题。也就是说，有了这两个实例，您就可以使用您给出的示例：

promoteHK :: Typ -> HKTyp v Id
promoteHK = genericCoerce

demoteHK :: HKTyp v Id -> Typ
demoteHK = genericCoerce

在行动：

> promoteHK PredT
HKPredT

> promoteHK (ListT PredT)
HKListT (Id HKPredT)

> promoteHK (ListT (ListT (ListT PredT)))
HKListT (Id (HKListT (Id (HKListT (Id HKPredT)))))

> demoteHK (HKProcT [HKIntT, HKPredT])
ProcT [IntT,PredT]

---

到目前为止，我还没有完全回答你的问题。您问两种看似同构的类型是否真的在 GHC 中具有相同的内存表示，以及 GHC 中是否有任何保证可以让您通常做这样的事情（我假设“像这样的事情”，你的意思是同构数据类型之间的强制)。

据我所知，GHC 不提供任何保证，但genericCoerce 为我们提供了更坚实的基础。排除不连贯的实例 hack，genericCoerce 的原始版本将具有幻像类型参数的数据类型转换为具有不同幻像参数的相同数据类型。从技术上讲，我不能保证 GHC 会以相同的方式存储相同运行时数据的多个实例，但在我看来这是一个很容易做出的假设。

一旦我们添加了不连贯的实例和新类型的包装器恶作剧，我们就站在不那么坚实的基础上，但一切正常的事实是一些安慰。

确实，现在我们看到 genericCoerce 的核心确实是一个强制（我们正在构建 same 数据类型从刚刚被破坏的每个案例），并且如果我们相信 newtype-wrapper 不连贯的实例也可以起到强制的作用，那么我们可以这样写：

genericCoerceProbablySafe :: (Generic x, Generic y, GenericCoerce (Rep x) (Rep y)) => x -> y
genericCoerceProbablySafe = unsafeCoerce

我们获得了比genericCoerce 更好的性能和比unsafeCoerce 更高的类型安全性，我们已将您的问题简化为：“GenericRep 是 GHC 如何存储内存的准确代理（最多新类型包装器）？”

【讨论】：

你说这解决了“简明定义的标准”。但是OP从未将其列为标准！列出的唯一标准是性能和正确性。一开始的正确变体在性能方面肯定不会比手写转换好（而且几乎可以肯定更糟，考虑到所涉及的所有间接性）。当然，您的 unsafeCoerce 最后实现将具有良好的性能，但您只是假设它完全正确，并且 OP 明确询问该假设是否正确。

我看错了。 OP 在显示了很长的定义后说“我真的很想能够写f = coerce”，我没有意识到接下来的几行是那句话的延续。至于unsafeCoerce，我做了两个明确的假设：1）GenericCoerce 约束将限制函数只在具有相同Generic 结构的类型上调用，2）Generic 代表模仿内存代表.因此，我将 OP 的问题从“我们对 GADT 的内存有任何保证吗”减少到“我们可以假设 Generic 代表模仿内存吗？”我认为这是一种进步。

@DanielWagner 我已经更新了答案，试图更清楚地了解结论。它没有明确回答 OP 的问题，但确实提供了思考这些问题的替代方法。感谢您推动我走向清晰和改进。