Type-checked non-empty strings：利用 GHC 类型系统实现编译期字符串校验

背景

在 Bellroy 的软件工程中，有一个核心设计目标是“使无效状态不可表示”（make invalid states unrepresentable）。这意味着通过类型系统的设计，让程序在编译阶段就排除掉不可能出现的错误数据，从而避免在运行时处理这些异常。

对于文本数据，Bellroy 经常使用 NonEmptyText 这一类型。顾名思义，该类型确保其值至少包含一个字符。为了在代码中便捷地构造这种类型，他们过去大量使用了 Template Haskell (TH) 的宏调用，例如 $$(NonEmptyText.make "hello")。

然而，随着内部数据密集型包 bellroy-data（包含货运提供商信息、会计系统数据、产品数据、税码等）的规模扩大，这种基于 TH 的方法带来了性能瓶颈。该包中包含了数千个类似的 TH 插值调用，导致编译时间显著增加。为了解决这一问题，团队探索并应用了一种结合 GHC（Glasgow Haskell Compiler）近年来特性的新技术，旨在通过纯类型级计算来替代部分 TH 逻辑，从而提升构建效率。

核心内容

这项技术是 GHC 在过去约 15 年中引入的一系列特性的结晶，特别是 GHC 9.10 引入的 RequiredTypeArguments（必需类型参数）。该特性允许将类型级字符串字面量作为参数传递给函数，就像传递普通值一样。

1. 基础实现：类型族约束

最初，团队尝试使用类型族（Type Family）来检查字符串是否为空。通过定义 IsNonEmptySymbol 类型族，可以在类型层面判断输入字符串：

type family IsNonEmptySymbol symbol :: Constraint where
  IsNonEmptySymbol "" = Unsatisfiable (Text "Expected a non-empty string")
  IsNonEmptySymbol _ = (()::Constraint)

配合 make 函数：

make :: forall symbol -> (IsNonEmptySymbol symbol) => NonEmptyText
make symbol = NonEmptyText (fromString (symbolVal (Proxy :: Proxy symbol)))

这种方式虽然能实现编译期检查（例如 make "" 会报错），但存在局限性。由于 IsNonEmptySymbol 是类型族而非类型类（Typeclass），它不能像普通类型类约束那样被打包进 Dict，也无法与 Data.SOP.hcfoldMap 等函数配合使用。

2. 进阶技巧：利用 OVERLAPPING 实例

为了解决类型族无法作为普通约束使用的问题，团队将逻辑重构为类型类，并利用 OVERLAPPING pragama（重叠实例 pragma）来实现自定义错误消息。

class IsNonEmptySymbol symbol

-- 当输入为空字符串 "" 时，触发此实例，抛出自定义错误
instance {-# OVERLAPPING #-} Unsatisfiable (Text "Expected a non-empty string") => IsNonEmptySymbol ""

-- 通用实例，匹配所有其他字符串
instance IsNonEmptySymbol a

工作原理： 当 GHC 解析 IsNonEmptySymbol 约束时，如果传入空字符串 ""，它会发现两个匹配的实例：

1. instance IsNonEmptySymbol ""（带有 OVERLAPPING 标记）
2. instance IsNonEmptySymbol a（通用实例）

如果没有 OVERLAPPING，GHC 会因为实例重叠而报错，因为它无法确定选择哪一个。然而，这正是我们想要的效果：我们故意让冲突发生在“禁止”的情况下。加上 OVERLAPPING 后，GHC 会优先选择带有 OVERLAPPING 标记的特定实例，从而触发 Unsatisfiable 错误，向用户展示清晰的自定义错误信息：“Expected a non-empty string”。

3. 扩展应用：DynamoDB 表名校验

这种技巧可以推广到任何可以在类型层面定义谓词的类型。例如，验证 DynamoDB 表名是否符合正则表达式 /^[a-zA-Z_.-]{3,255}$/。

由于简单的空字符串检查不够复杂，这里需要一种算法化的方法。团队使用类型族 IsValidTableName__ 来驱动内部类型类的解析，从而在类型类层面暴露自定义错误消息。

核心逻辑包括：

• 递归解析：使用 IsValidTableName_go 类型族遍历字符串字符，检查长度是否在 3 到 255 之间，以及字符是否合法（仅允许字母、下划线、点、连字符）。
• 错误分发：IsValidTableName_ 类型类根据 IsValidTableName__ 的计算结果（True 或 False）选择实例。如果结果为 False，则触发 Unsatisfiable 错误。

class (KnownSymbol a) => IsValidTableName a
instance (KnownSymbol a, IsValidTableName_ validity a) => IsValidTableName a

class (IsValidTableName__ a ~ wasValid) => IsValidTableName_ (wasValid :: Bool) a
instance (IsValidTableName__ a ~ 'True) => IsValidTableName_ 'True a
instance (Unsatisfiable ('Text "Encountered invalid TableName")) => IsValidTableName_ 'False a

4. 局限性

尽管强大，这种技术在处理复杂算法时仍面临挑战：

• 类型级编程限制：类型族不支持 let 绑定或 case 模式匹配，必须通过额外的类型参数和辅助类型族来表达逻辑。
• 递归深度限制：GHC 默认的类型级归约（reduction）限制为 20 步。对于长度为 n 的字符串，O(n) 复杂度的类型级验证器在解析超过 20 个字符时会遇到瓶颈。因此，这种方法适用于短字符串或简单验证，不适用于复杂的类型级解析器。

关键要点

• 编译期优化：将数千个 Template Haskell 调用替换为基于 RequiredTypeArguments 的类型级检查，使大型数据包的编译时间减少了约 10%。
• 无效状态不可表示：通过类型系统强制约束，确保 NonEmptyText 等类型在编译期就排除空字符串，从根源上消除运行时错误。
• 类型类与类型族的结合：利用 OVERLAPPING 实例技巧，解决了类型族无法作为普通类型类约束使用的问题，实现了优雅的自定义错误消息机制。
• 适用范围：该技术适用于任何可以定义类型级谓词的场景（如正整数验证、短字符串格式验证）。
• 性能与复杂度权衡：虽然提升了构建速度，但类型级算法受限于 GHC 的归约深度（默认 20 步），不适合处理长字符串或复杂逻辑的类型级解析。

意义与影响

这项技术展示了 Haskell 类型系统在工程实践中的强大威力。它不仅是一个代码优化案例，更体现了“以类型驱动设计”的工程哲学。

1. 构建性能提升：对于数据密集型的大型 Haskell 项目，减少 Template Haskell 的使用可以显著缩短 CI/CD 流水线中的编译时间，提高开发迭代效率。
2. 代码安全性增强：通过将验证逻辑移至编译期，开发者可以确信代码中不存在违反业务规则的数据结构（如空的文本字段、非法的表名），从而减少运行时异常和测试用例的覆盖压力。
3. 技术栈演进：随着 GHC 9.10 等版本引入 RequiredTypeArguments 等新特性，Haskell 的类型级编程变得更加直观和强大。这种“类型级字符串处理”的模式为其他语言或未来的 GHC 版本提供了有价值的参考，展示了如何利用编译器特性来简化代码并提高可靠性。

总之，这是一种在保持代码简洁性的同时，利用编译器能力进行严格静态检查的高级 Haskell 编程技巧，特别适合对数据完整性和构建效率有高要求的企业级应用。