GHC 类型的强制转换到底是什么？答案

【问题标题】：What exactly are GHC type coercions?GHC 类型的强制转换到底是什么？
【发布时间】：2025-12-12 07:50:01
【问题描述】：

我一直在查找 haskell 的核心语言以了解它是如何工作的。我在互联网搜索中发现的一项功能是类型强制。我知道它们用于实现 GADT，但我不太了解。我在网上找到的所有描述对我来说都是相当高级的，虽然我对系统 F 有相当的了解。谁能以一种可以理解的方式向我解释类型强制？

【问题讨论】：

标签： haskell ghc lambda-calculus

【解决方案1】：

基本上，Haskell 通过评估这种简单的核心语言进行编译。为了保持简单，通常不希望将诸如 GADT 或类型类之类的构造直接添加到语言中，而是在编译器的最前端将它们编译成更简单但更通用（和冗长）的构造核。另外请记住，Core 是类型化的，因此我们必须确保我们可以以类型化的方式对所有这些内容进行编码，这是一个非常复杂的问题。

为了对 GADT 进行编码，它们被细化为具有存在性和强制的普通数据类型。基本思想是强制转换是一种称为相等类型的类型，写作t ~ t'。这个 type 是为了见证证据，即使我们可能不知道，t 和 t' 在引擎盖下是相同的类型。它们像任何其他类型一样被传递，因此处理方式没有什么特别之处。还有一套类型构造函数用于操作这些类型构成关于相等性的小证明，例如sym :: t ~ t' -> t' ~ t。最后，在术语级别有一个运算符，它接受t 类型的术语和t ~ t' 类型的类型，并被键入为t' 类型的术语。例如cast e T :: t'，但该术语的行为与e 相同。我们刚刚使用了 t' 和 t 相同的证明来转换 e 以使类型检查器满意。

这是基本思路

代表平等的种类
表示相等证明的类型
cast 在术语级别使用这些证明

还要注意，通过将证明隔离到类型级别，它们最终不会产生运行时成本，因为类型将被删除。

我认为System F with Type Equality Coercions 是一个很好的参考，当然 SPJ 的所有出版物都可以提供帮助。

【讨论】：

【解决方案2】：

@jozefg 应该得到答案，但这里有一个 GADT 对存在量化脱糖的例子。还不是核心，但朝着它迈出了一步。

data Foo :: * -> * where
  Bar :: Int -> Foo Int
  Oink :: b -> c -> d -> Foo (f b)

通过

data Foo a where
  Bar :: (a ~ Int) => Int -> Foo a
  Oink :: (a ~ f b) => b -> c -> d -> Foo a

到

data Foo a
  = (a ~ Int) => Bar Int
  | forall b c d f. (a ~ f b) => Oink b c d

感谢/u/MitchellSalad on /r/haskell。

【讨论】：