Serokell 对 GHC 的工作：依值类型，第5部分

# Serokell 对 GHC 的贡献：依赖类型篇（第五部分） 来源：https://serokell.io/blog/serokell-s-work-on-ghc-dependent-types-part-5 本文延续了 Serokell GHC 团队分享将依赖类型引入 Haskell 进展的优良传统。自上次报告以来，发生了许多事情，值得详细回顾。 在本期中，Vladislav Zavialov 介绍了三项主要贡献以及一系列较小的改进，推动依赖型 Haskell 更接近成为现实。 ## 概要 本报告的亮点包括： - 在 GADT 中支持可见的`forall` - 基于命名空间的导入 - 种检查中的类型实例 之后，我们将介绍其他改进： - 统一`HsType`和`HsExpr`的进展 - 在必需类型参数中使用星号种语法 - 必需类型参数中的 Pun 检测 - 新增类型族：`Tuple`、`Constraints`、`Tuple#`、`Sum#` - 重构内建名称和 Pun 名称的名称解析 ## 在 GADT 中支持可见的`forall` Haskell 依赖类型的设计，正如 GHC 提案 #378（https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-dependent-type-design.rst）《依赖类型的设计》中所述，包含对至少 6 种量词的支持： ``` 量词 依赖性 可见性 擦除 ------------------------------------------------------------ forall a. ty 依赖 不可见 擦除 forall a -> ty 依赖 可见 擦除 foreach a. ty 依赖 不可见 保留 foreach a -> ty 依赖 可见 保留 Eq a => ty 非依赖 不可见 保留 t1 -> t2 非依赖 可见 保留 ``` 我们关注的是`foreach a -> ty`，也称为依赖积、依赖函数或 Π 类型（三者同义）。但在处理如此宏大的目标之前，先解决其他量词是有帮助的，例如`forall a -> ty`，通常称为可见`forall`或 VDQ（可见依赖量化）。 大多数关于 VDQ 的设计问题在 2021 年 GHC 提案 #281（https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst）《项类型中的可见 forall》被接受时已解决，此后我们一直在持续实现它，逐一攻克工程挑战。 该方向的最新进展是在 GADT 中实现了 VDQ。从 GHC 9.14 开始，`RequiredTypeArguments`扩展允许如下声明： ``` data T a where Typed :: forall a -> a -> T a ``` 在这个例子中，`Typed`数据构造器接受两个可见参数：一个*类型*，然后是该类型的*值*，例如`Typed Int 42`或`Typed String "hello"`。这确实具有依赖类型的特征！以下是它在不同上下文中的一些示例： ``` -- 表达式 t1 = Typed Int 42 t2 = Typed String "hello" t3 = Typed (Int -> Bool) even -- 模式 f1 (Typed a x) = x :: a f2 (Typed Int n) = n*2 f3 (Typed ((->) w Bool) g) = not . g -- 类型（使用 DataKinds） type T1 = Typed Nat 42 type T2 = Typed Symbol "hello" type T3 = Typed (Type -> Constraint) Num ``` 需要注意的是，为什么这还不算真正的依赖类型：类型参数保证会被擦除，即对数据在堆上的表示没有影响，因此不能对其进行模式匹配： ``` f4 (Typed a x) = case a of -- 不行！这是编译时错误 Int -> negate x Bool -> not x _ -> x ``` 尽管如此，允许这种形式的量化带来了自身的技术挑战，而这些挑战现已解决。这意味着在添加正确的依赖类型时，我们不必担心语法上的小问题。 以下是实现这一目标所面临的挑战。 第一个挑战是，GHC 对构造器模式`MkE @tp1 @tp2 p1 p2`的 AST 将类型参数和项参数完全分开存放。我们将其重构为使用混合列表表示： ``` ConPat "MkE" [tp1, tp2] [p1, p2] -- 旧 ConPat "MkE" [InvisP tp1, InvisP tp2, p1, p2] -- 新 ``` 新表示的直接效果是改善了错误信息。考虑模式`Con x @t y`。以前它会导致解析错误，因为`@t`不能出现在`x`之后，现在它被报告为`[GHC-14964]`。 更有趣的是，形式`Con x @t y`原则上变得可表示，因此可以在整个编译过程中正确处理它。 第二个挑战是允许在构造器签名中使用可见的`forall`。经过几次尝试才正确实现，因为控制隐式量化的 forall-or-nothing 规则意味着一些量词必须保存在单独的字段中。类型检查器也进行了更新，不再假设所有没有`@`标记的子模式都是值参数。确实，它们中的一部分或全部可能最终成为必需的类型参数。 第三个挑战是更新数据构造器的核心表示，以允许在量词列表中出现不同可见性的 foralls： ``` - dcUserTyVarBinders :: [InvisTVBinder] + dcUserTyVarBinders :: [TyVarBinder] ``` 这一变化不仅需要在整个 GHC 代码库中进行机械性的修改，还导致了晦涩的核心 Lint 错误。这个补丁被搁置了几个月，直到`@mniip`在 ZuriHac 2025 上帮助调试了这个问题。结果发现，用于确定是否引入数据构造器包装器的谓词返回了假阴性。 随着这三个挑战的解决，GHC 现在可以处理以下示例（该示例旨在压力测试该功能，而非展示实际用例）： ``` newtype Checker a b c where C :: forall a. forall b -> forall c. (a -> (c, b)) -> Checker a b c cDouble = C Double (length &&& read) -- ghci> map (test cDouble) ["1.5", "0.5", "1.05", "0.05"] -- [(3,True),(3,True),(4,True),(4,False)] test :: Show b => Checker String b c -> String -> (c, Bool) test (C t f) s = fmap (\r -> show @t r == s) (f s) ``` 就是这样：我们在 Haskell 程序中自由混合项和类型又近了一步。未来的相关工作包括 GADT 中的嵌套量化（#18389 (https://gitlab.haskell.org/ghc/ghc/-/issues/18389)）和模式同义词中的 VDQ（#23704 (https://gitlab.haskell.org/ghc/ghc/-/issues/23704)）。 ## 基于命名空间的导入 Haskell 有两个命名空间，正如 GHC 提案 #581（https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0581-namespace-specified-imports.rst）所解释的： - *类型命名空间*，包括类型构造器、类型同义词、类型族和类型类的名称； - *数据命名空间*，包括项级值、函数、数据构造器和模式同义词的名称。 这种分离允许我们定义名称相同的类型构造器和数据构造器： ``` data T = T ``` 在使用处，GHC 根据上下文推断指的是哪个`T`。例如，在`t :: T`中，出现的`T`解析为类型构造器，而在`t = T`中则解析为数据构造器。 在导入/导出列表、fixity 声明、pragma、TH 名称引用以及最明显的，在`DataKinds`和`RequiredTypeArguments`混合项和类型时，依赖上下文选择命名空间会产生歧义。 避免这些问题的最简单方法是避免引入同名的类型和数据构造器，依赖类型风格的 Haskell 往往这样做。然而，我们不能期望所有库都采用这种约定，因此我们仍然需要一种不依赖上下文的方式来区分`T`和`T`。 经过多次尝试，以及多位作者提出的不少于三个提案后，共识是引入如下形式的基于命名空间的导入： ``` import Data.Monoid as M.Type (type ..) import Data.Monoid as M (data ..) ``` 注意新的`..`语法；这是一个通配符，代表指定命名空间中的所有名称。 回想一下，`Data.Monoid`模块导出了以下新类型： ``` newtype All = All {getAll :: Bool} newtype Alt f a = Alt {getAlt :: f a} newtype Any = Any {getAny :: Bool} newtype Ap f a = Ap {getAp :: f a} newtype Dual a = Dual {getDual :: a} newtype Endo a = Endo {appEndo :: a -> a} newtype First a = First {getFirst :: Maybe a} newtype Last a = Last {getLast :: Maybe a} newtype Product a = Product {getProduct :: a} newtype Sum a = Sum {getSum :: a} ``` 使用上述导入，可以将类型构造器引用为`M.Type.Dual`、`M.Type.Endo`、`M.Type.Product`等，而数据构造器则分别引用为`M.Dual`、`M.Endo`和`M.Product`。 起初，这似乎是一个易于实现的功能：一种新的导入/导出项形式，只需根据命名空间说明符选择名称即可。然而，当我们开始着手解决这个问题时，发现了大量必须先修复的既有错误： - 在从属导入和导出列表中，使用`type`命名空间说明符以前会被静默忽略（#12488 (https://gitlab.haskell.org/ghc/ghc/-/issues/12488)、#22581 (https://gitlab.haskell.org/ghc/ghc/-/issues/22581)） - 在`hiding`子句内的从属导入列表中，不存在的项会导致使用`-Wdodgy-imports`时产生较差的警告信息（#25983 (https://gitlab.haskell.org/ghc/ghc/-/issues/25983)） - 在`hiding`子句内的从属导入列表中，不存在的项会导致整个导入声明被丢弃（#25984 (https://gitlab.haskell.org/ghc/ghc/-/issues/25984)） - 在从属导入列表中，如果存在同名的关联类型，则无法引用类方法（#25991 (https://gitlab.haskell.org/ghc/ghc/-/issues/25991)） 发现了这么多边界情况，不清楚导入/导出逻辑中还潜伏着多少其他错误，但我们决定谨慎地进行准备工作： - 我们引入了在单个导入/导出项中使用`data`关键字的选项，例如`import Data.Proxy as D (data Proxy)`。 - 根据提案，我们弃用了`pattern`命名空间说明符，并引入了`-Wpattern-namespace-specifier`警告以帮助迁移到新的`data`语法。 - 我们增加了`-Wduplicate-exports`和`-Wdodgy-exports`的测试覆盖率，这揭示了一些拼写错误和死代码。 终于，基础看起来足够稳固，可以着手实际的功能了。下一步是在导入和导出列表中添加对顶层基于命名空间的通配符`type ..`和`data ..`的支持： ``` import M (type ..) -- 从 M 导入所有类型和类构造器 import M (data ..) -- 从 M 导入所有数据构造器和项 ``` ``` module M (type .., f) where -- 导出在 M 中定义的所有类型和类构造器， -- 以及函数 'f' ``` 然后我们进行了一次重构，之后实现继续并达到了另一个里程碑：在导入和导出列表中支持从属的基于命名空间的通配符`X(type ..)`和`X(data ..)`： ``` import M (Cls(type ..)) -- 导入 Cls 及其所有关联类型 import M (Cls(data ..)) -- 导入 Cls 及其所有方法 ``` ``` module M (R(data ..), C(type ..)) where -- 导出 R 及其所有数据构造器和记录字段； -- 导出 C 及其所有关联类型，但不导出其方法 ``` 此时，GHC 可以处理提案中的所有示例，因此我们可以宣布胜利了。研究规范时发现了几个仍在处理的边界情况（#27268 (https://gitlab.haskell.org/ghc/ghc/-/issues/27268)），但这些情况在实践中不太可能出现。 瞧，Haskellers 又有了一种处理“可怕的命名空间问题”的工具。 ## 种检查中的类型实例 如果你曾在模块中编写过`$(return [])`来帮助 GHC 进行种检查，那么你就知道本节将讨论什么。如果没有，请继续阅读：这是一个重要的改进。 我们很高兴地宣布，经过 10 年的尝试，我们终于教会了 GHC 在种检查期间查找开放类型族实例，无论它们在源文件中出现的顺序如何。考虑以下程序： ``` type family Open a type family F a :: Open a type instance F Int = True type instance Open Int = Bool ``` 在种检查`F Int = True`实例时，我们需要知道`Open Int = Bool`，因此我们最好先检查另一个类型实例，否则会看到以下错误： ``` error: [GHC-83865] • Expected kind ‘Open Int’, but ‘True’ has kind ‘Bool’ • In the type ‘True’ In the type instance declaration for ‘F’ ``` 但请再看这一行： ``` type instance F Int = True ``` 它提到了`F`、`Int`和`True`。没有任何指向`Open`！那么我们如何知道要先种检查另一个实例呢？ 我们尝试了各种启发式方法，但每次都发现了无法处理的边界情况。与此同时，大约每年都会报告一次该问题的一些变体： - #12088 (https://gitlab.haskell.org/ghc/ghc/-/issues/12088) “种检查中的类型/数据族实例”（2016 年 5 月 20 日） - #12239 (https://gitlab.haskell.org/ghc/ghc/-/issues/12239) “依赖类型族无法归约”（2016 年 6 月 29 日） - #13790 (https://gitlab.haskell.org/ghc/ghc/-/issues/13790) “除非强制，否则 GHC 不在种类签名中归约类型族”（2017 年 6 月 5 日） - #14668 (https://gitlab.haskell.org/ghc/ghc/-/issues/14668) “声明顺序可能导致类型检查失败”（2018 年 1 月 14 日） - #15561 (https://gitlab.haskell.org/ghc/ghc/-/issues/15561) “类型错误取决于 GADT 和类型族定义的顺序”（2018 年 8 月 24 日） - #16410 (https://gitlab.haskell.org/ghc/ghc/-/issues/16410) “声明顺序很重要”（2019 年 3 月 8 日） - #16448 (https://gitlab.haskell.org/ghc/ghc/-/issues/16448) “未解析的类型族种类错误”（2019 年 3 月 16 日） - #16693 (https://gitlab.haskell.org/ghc/ghc/-/issues/16693) “声明顺序影响接受的程序”（2019 年 5 月 25 日） - #19611 (https://gitlab.haskell.org/ghc/ghc/-/issues/19611) “依赖种类的类型族实例的类型检查在范围内没有足够的等式”（2021 年 3 月 28 日） - #20875 (https://gitlab.haskell.org/ghc/ghc/-/issues/20875) “别名和类型族的声明顺序”（2021 年 12 月 26 日） - #21172 (https://gitlab.haskell.org/ghc/ghc/-/issues/21172) “种类族不归约”（2022 年 3 月 5 日） - #22257 (https://gitlab.haskell.org/ghc/ghc/-/issues/22257) “依赖类型族不能与其实例分离”（2022 年 10 月 5 日） - #25238 (https://gitlab.haskell.org/ghc/ghc/-/issues/25238) “开放类型族的种类归约取决于数据类型声明顺序”（2024 年 9 月 5 日） - #25833 (https://gitlab.haskell.org/ghc/ghc/-/issues/25833) “Splice 似乎破坏了类型族的类型推断”（2025 年 3 月 8 日） Haskellers 非常擅长编写打破编译器的程序，感谢这些错误报告，我们积累了优秀的测试用例集。 现在让我们深入了解技术细节。 在重命名模块中的类型、类和实例声明后，GHC 对重命名后的声明进行依赖分析，以确定种检查它们的顺序。依赖分析返回拓扑排序的 SCC（强连通分量）列表，其中 SCC 代表一组相互递归的声明。 如果依赖分析是完整的，即它能够发现所有声明之间的所有依赖关系，那么 GHC 可以...