PAYATHON 2026

GHC 为何不自动推断 closed type families 的单射性？

数据阿明

原则上，GHC 可以为能够通过检查的 closed type families 推断单射性。要求显式声明，主要是为了让代码对单射性的依赖清楚可见，也让 GHC 在后续修改破坏这一性质时，直接指出有问题的类型族方程。

为什么选择显式注解？

设计论文《Injective Type Families for Haskell》的第 3.4 节讨论了这个问题：自动推断 closed type families 的单射性在理论上可行，但重构时可能产生意外的编译错误。调用方可能在不知情的情况下依赖推断出的单射性；定义发生变化后，错误却出现在远处的模块，甚至另一个包中。显式注解则让 GHC 在破坏声明的方程处报错。设计论文，第 3.4 节

closed 的意思是其他声明不能继续添加方程。维护者仍然可以编辑原来的定义，因此当前方程具有的性质未必会在下次修改后保留。

一个具体例子

需要让结果类型决定输入类型时，可以启用 TypeFamilyDependencies 并显式声明：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}

module Example where

type family F a = r | r -> a where
  F Int  = Bool
  F Bool = Char

preserve :: F a -> F a
preserve x = x

r -> a 表示结果类型决定参数 a。从 F a ~ F b 可以推出 a ~ b。这使 GHC 能够处理某些只在类型族应用中出现的类型变量，解决相关的类型歧义。GHC 用户指南：Injective type families

假设维护者随后在 where 块中增加：

  F Char = Bool

此时 F Int 和 F Char 都得到 Bool，结果无法唯一确定输入，因而违反 r -> a。

保留显式注解时，GHC 会拒绝这个违反声明的方程。若采用题设中的自动推断方案，编译器可能不再赋予 F 单射性，依赖该性质的 preserve 类型签名便可能无法通过歧义检查。错误因此可能从定义处转移到使用处。

检查注解不等于完整判定单射性

GHC 的检查算法有保守限制，不能证明所有实际上成立的单射性性质。因此，可以考虑自动采用检查器能够证明的性质，但不能由此推断 GHC 能完整判定任意类型族是否单射。设计论文，第 4 节

实际使用时，先确定结果必须决定哪些参数，再用 | r -> ... 列出。多参数类型族可以只声明其中部分参数具有单射性。之后修改方程时保留注解，让编译器检查这项约定是否仍然成立。GHC 用户指南：注解语法

备注：内容仅供参考。