类型检查的非空字符串

# Haskell 公案：类型检查的非空字符串 来源：https://exploring-better-ways.bellroy.com/haskell-koan-type-checked-non-empty-strings.html 这篇帖子是一则 Haskell 公案。我们会先讲背景和动机，但重点是分享我们采用并乐在其中一项小巧而不常见的技术——绝佳的博客素材。 简单来说，我们编写了一个类型检查的非空字符串构造器，替换了数千个等价的 `TemplateHaskell` 调用，在一个数据量庞大的大型包中实现了约 10% 的构建时间提升。 ``` before, after, invalidBefore, invalidAfter :: NonEmptyText before = $$(NonEmptyText.make "hello") after = NonEmptyText.make "hello" invalidBefore = $$(NonEmptyText.make "") -- ⇝ 展开时出错…… invalidAfter = NonEmptyText.make "" -- ⇝ 类型错误：期望非空字符串 ``` 让 **无效状态不可表示** 是 Bellroy 软件设计的核心目标。基于此，我们经常用于文本数据（我们有很多文本数据）的一个类型是 `NonEmptyText`。顾名思义：这个类型的值是一个至少包含一个字符的字符串。 这项技术是过去十五年左右 GHC 特性汇聚的结果。特别是 `RequiredTypeArguments`（在 GHC 9.10 中引入，https://downloads.haskell.org/ghc/9.10.1/docs/users_guide/9.10.1-notes.html），它允许我们把类型层面的字符串字面量像值一样传递给函数。如果我们（在类型层面）看到空字符串，我们可以抛出自定义类型错误消息，例如 `"Expected a non-empty string"`，如下所示： ``` type family IsNonEmptySymbol symbol :: Constraint where IsNonEmptySymbol "" = Unsatisfiable (Text "Expected a non-empty string") IsNonEmptySymbol _ = (()::Constraint) -- 空约束始终满足 -- 注意之前没有 RequiredTypeArguments 的语法： -- make :: forall symbol. IsNonEmptySymbol symbol => NonEmptyText -- 使用时类似 `make @"hello!"` make :: forall symbol -> (IsNonEmptySymbol symbol) => NonEmptyText make symbol = NonEmptyText (fromString (symbolVal (Proxy :: Proxy symbol))) test :: NonEmptyText test = make "hello!" ``` 结合正确的 `LANGUAGE` 魔法，这确实有效。这需要 `UndecidableInstances` 才能工作，它本身无害，但确实为出错的可能性打开了大门¹ (https://exploring-better-ways.bellroy.com/haskell-koan-type-checked-non-empty-strings.html#fn1)。 此外，由于 `IsNonEmptySymbol` 是一个类型族，它不能直接像普通类型类约束那样使用——例如，它不能打包到 `Dict` 中，也不能与 `Data.SOP.hcfoldMap` 等函数一起使用；它不是那种你可以像普通类型类一样“请求其实例”的东西，尽管它返回一个类似 `Constraint` 的东西。 这个技巧的最后一步是将 `IsNonEmptySymbol` 写成类型类： ``` class IsNonEmptySymbol symbol instance {-# OVERLAPPING #-} Unsatisfiable (Text "Expected a non-empty string") => IsNonEmptySymbol "" instance IsNonEmptySymbol a -- make: 同上 make :: forall symbol -> (IsNonEmptySymbol symbol) => NonEmptyText make symbol = NonEmptyText (fromString (symbolVal (Proxy :: Proxy symbol))) ``` 当 GHC 解析 `IsNonEmptySymbol` 约束并给定一个空字符串时，它同时找到实例：`\ _ => instance IsNonEmptySymbol ""` 和 `instance IsNonEmptySymbol a`。如果我们省略 `OVERLAPPING` 编译指示，GHC 就会报错；它不知道该选择哪个实例，并会抱怨存在重叠的可能性——这没问题，因为唯一存在重叠实例的情况正是我们想要禁止的情况，即输入为 `""`。 所以这里 `OVERLAPPING` 编译指示的效果是，GHC 确实选择了我们“想要”的实例；那个带有自定义类型错误的实例。然后该实例会抛出自定义错误消息，告知用户期望一个非空字符串。 ## 影响 我们内部的 `bellroy-data` 包——包含诸如已知货运和运输提供商信息、会计系统、产品数据、税务代码等数据——有数千个 TH 拼接，如 `$$(NonEmptyText.makeTH _)`。迁移到 `RequiredTypeArgument` 方法为这个包减少了大约 10% 的编译时间。 ## 类似我们可运用该技巧的场景 我们可以（几乎）完全相同的代码来验证给定的 `Natural` 是正数，以构造一个类型检查的 `Positive` 构造器。一般来说，我们可以将此技术用于任何我们可以定义类型层面谓词的类型。 从这里你或许可以想象，例如，类型层面的字符串解析来定义类型安全的结构化语法以构造 URI：这会有效，但你很快就会遇到 GHC 默认的 20 步归约限制；一个对长度为 n 的字符串进行 O(n) 类型层面验证的函数有 20 步“归约”（即解析）的硬上限，因此解析不能超过 20 个字符——这还假设解析步骤本身不计数在内。 一般来说，非平凡的算法也很难用类型族表达；例如，你无法编写 `let` 绑定，或使用类似 `case` 的语法进行模式匹配：如果需要这些，必须通过额外的类型参数和辅助类型族来表达。这也需要一些管道工作才能像我们上面创建的 `IsNonEmptySymbol` 类那样作为类型类工作。 尽管如此，如果你读到这里，你可能对实际样子感兴趣：看好了🪄，用于 DynamoDB 表名的类型层面解析： ``` {-# LANGUAGE DataKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RequiredTypeArguments #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} import Data.Proxy import Data.String (fromString) import Data.Text (Text) import Data.Type.Bool qualified as Bool import GHC.TypeError import GHC.TypeLits -- | 有效的 DynamoDB 表名必须匹配正则 /^[a-zA-Z_.-]{3,255}$/ newtype TableName = TableName Text deriving (Show) make :: forall name -> (IsValidTableName name) => TableName make name = TableName (fromString (symbolVal (Proxy :: Proxy name))) ``` 到目前为止，一切顺利。但枚举每个无效字符串需要时间；我们需要一种算法方法，而不是上面 `IsNonEmptySymbol` 的工作方式。如上所述，我们更希望将其封装成一种 kind 为 `Type -> Constraint` 的类型类。我在这里使用的方法是，用一个类型族来指导内部类型类的解析。因此这种方法既可以作为一元类型类（理想）工作，又能向程序员展示自定义类型错误消息（优秀）。 ``` class (KnownSymbol a) => IsValidTableName a instance (KnownSymbol a, IsValidTableName_ validity a) => IsValidTableName a -- | 包装类，产生友好的错误消息 -- -- `wasValid` 参数由 `IsValidTableName__` 类型族计算。 -- 然后我们可以引导 GHC 进入无操作实例（成功）， -- 或抛出一些信息的错误实例。 class (IsValidTableName__ a ~ wasValid) => IsValidTableName_ (wasValid :: Bool) a instance (IsValidTableName__ a ~ 'True) => IsValidTableName_ 'True a instance (Unsatisfiable ('Text "Encountered invalid TableName")) => IsValidTableName_ 'False a ``` 现在我们需要实际实现这个 `IsValidTableName__` 类型族，它看起来像 `IsValidTableName__ (input :: Symbol) :: Bool`。 ``` type IsValidTableName__ text = IsValidTableName_go 0 'Nothing (UnconsSymbol text) -- IsValidTableName__ 的内部循环 type family IsValidTableName_go (len :: Nat) (invalidLastChar :: Maybe Char) (unconsResult :: Maybe (Char, Symbol)) :: Bool where IsValidTableName_go len 'Nothing ('Just '(x, xs)) = IsValidTableName_go (len + 1) (InvalidTableChar x) (UnconsSymbol xs) IsValidTableName_go len 'Nothing _ = (3 <=? len) Bool.&& (len <=? 255) IsValidTableName_go len ('Just invalidChar) _ = 'False -- 检查单个字符是否有效 type family InvalidTableChar (ch :: Char) :: Maybe Char where InvalidTableChar ch = Bool.If (IsValidTableChar ch) 'Nothing ('Just ch) type family IsValidTableChar (ch :: Char) :: Bool where IsValidTableChar '-' = 'True IsValidTableChar '_' = 'True IsValidTableChar '.' = 'True IsValidTableChar ch = ('a' <=? ch Bool.&& ch <=? 'z') Bool.|| ('A' <=? ch Bool.&& ch <=? 'Z') Bool.|| ('0' <=? ch Bool.&& ch <=? '9') ``` 最后，我们确实可以使用它： ``` valid, invalid, invalid2 :: TableName valid = make "hello-bellroy123" invalid = make "no" -- 错误！"Encountered invalid TableName" invalid2 = make "tablename!!" -- 错误！"Encountered invalid TableName" ``` 这里可以使用 `singletons-th` 包来推广实际的值层面函数，比如 `IsValidTableName` 函数，但这里的一个要点是演示它在底层是如何工作的。 依赖类型 Haskell 的进程不可阻挡 (https://ghc.serokell.io/dh)，它随着每个主要 GHC 版本缓慢但坚定地接近现实。像 Idris 和 Lean 这样的语言今天已经拥有它，但无论好坏，Haskell 是这个领域采用率和惯性最大的语言。GHC 开发者们：请继续！🙂 --- 1. Dennis Gosnell (https://functor.tokyo/blog/2017-04-07-undecidable-instances) 有一篇很棒的博文详细介绍了 `UndecidableInstances`，并阐述了它在一个用例中相当危险的情况。↩︎ (https://exploring-better-ways.bellroy.com/haskell-koan-type-checked-non-empty-strings.html#fnref1)