无依赖类型的条件表达式
摘要
本文展示了一种技巧，使用Haskell中的Church编码和可重绑定语法来实现无依赖类型的条件表达式，并通过简单类型推断证明其可行性。
<p><a href="https://lobste.rs/s/yomxcl/dependent_if_expressions_without">评论</a></p>
查看缓存全文
缓存时间: 2026/09/02 17:56
# 无依赖类型的条件依赖表达式
来源：https://haskellforall.com/2026/09/dependent-if-expressions
本文介绍一种在不实际使用依赖类型的情况下实现看似需要依赖类型代码的民间技巧。事实上，该技巧适用于任何支持简单 Hindley-Milner 类型推断的语言。为证明这一点，本文结尾将展示如何让以下 Haskell 代码通过类型检查并正常运行：
```haskell
example bool = if bool then 5 else "hi!"
main = do
print (example false) -- "hi!"
print (example true ) -- 5
print (example (false && true)) -- "hi!"
print (example (false || true)) -- 5
print (example (not true)) -- "hi!"
```
...且仅需启用一个语言扩展：`RebindableSyntax`。
我从研究多个 Haskell 包中掌握了这一技巧，尤其值得注意的是 `formatting` 包（https://hackage.haskell.org/package/formatting）。此处我将该技巧调整为对依赖式 `if` 表达式的建模——即根据输入返回不同类型的条件表达式。我将分两步展开：首先解释相关技巧（丘奇编码布尔值），然后将其推广以实现依赖式 `if` 表达式。
### 丘奇编码
"丘奇编码"是一种仅使用纯函数（不借助其他手段）对数据结构及其操作进行编码的技术。例如，我们可以将布尔值丘奇编码为接受两个参数并返回其中之一的函数：
```haskell
{-# LANGUAGE RankNTypes #-}
import Prelude hiding (Bool(..), not, (&&), (||))
type Bool = forall a . a -> a -> a
true :: Bool
true thenBranch elseBranch = thenBranch
false :: Bool
false thenBranch elseBranch = elseBranch
```
我将函数参数命名为 `thenBranch` 和 `elseBranch`，是因为你可以将这些丘奇编码的布尔值视为"预构的 if 表达式"——两个函数参数分别代表 `if` 表达式的 `then` 和 `else` 分支，而布尔值决定返回哪个分支作为结果。实际上，我们可以定义一个 `ifThenElse` 函数，其行为与 `if` 表达式相同，只是期望条件为丘奇编码布尔值：
```haskell
ifThenElse :: Bool -> a -> a -> a
ifThenElse condition thenBranch elseBranch = condition thenBranch elseBranch
```
...其工作方式与 `if` 表达式完全一致：
```haskell
>>> ifThenElse true "then branch" "else branch"
"then branch"
>>> ifThenElse false "then branch" "else branch"
"else branch"
```
> **注意：** 若想跟随操作或运行示例，完整代码见附录。
要理解其工作原理，让我们推演对 `true` 调用 `ifThenElse` 时发生的情况：
```haskell
ifThenElse true thenBranch elseBranch
-- 根据 `ifThenElse` 定义：
= true thenBranch elseBranch
-- 根据 `true` 定义：
= thenBranch
```
上述表达式返回 `thenBranch`，正如传统 `if` 表达式在条件为 `true` 时的行为。类似地，若对 `false` 调用 `ifThenElse`，则得到 `elseBranch`：
```haskell
ifThenElse false thenBranch elseBranch
= false thenBranch elseBranch
= elseBranch
```
实际上，我们可以更进一步修改 Haskell 的 `if`/`then`/`else` 语法以使用上述 `ifThenElse` 函数。启用 `RebindableSyntax` 语言扩展后，所有形如 `if condition then thenBranch else elseBranch` 的表达式将被解构为 `ifThenElse condition thenBranch elseBranch`，使用当前作用域内的任意 `ifThenElse` 函数：
```haskell
{-# LANGUAGE RebindableSyntax #-}
toString :: Bool -> String
toString bool = if bool then "true" else "false"
main :: IO ()
main = do
print (toString false) -- "false"
print (toString true ) -- "true"
```
我们可以按相同逻辑推导其工作原理：
```haskell
toString false
-- 根据 `toString` 定义：
= if false then "true" else "false"
-- `if`/`then`/`else` 解构为 `ifThenElse`：
= ifThenElse false "true" "false"
-- 根据 `ifThenElse` 定义：
= false "true" "false"
-- 根据 `false` 定义：
= "false"
```
我们可以继续实现所有常规布尔运算，使其适用于这些丘奇编码的布尔值：
```haskell
not :: Bool -> Bool
not bool thenBranch elseBranch = bool elseBranch thenBranch
(&&) :: Bool -> Bool -> Bool
(x && y) thenBranch elseBranch = x (y thenBranch elseBranch) elseBranch
(||) :: Bool -> Bool -> Bool
(x || y) thenBranch elseBranch = x thenBranch (y thenBranch elseBranch)
```
...其行为完全符合预期：
```haskell
main :: IO ()
main = do
...
print (toString (not true)) -- "false"
print (toString (false && true)) -- "false"
print (toString (false || true)) -- "true"
```
...我们可以按如下方式推导最后一个示例：
```haskell
toString (false || true)
= if false || true then "true" else "false"
= ifThenElse (false || true) "true" "false"
= (false || true) "true" "false"
= false "true" (true "true" "false")
= true "true" "false"
= "true"
```
然而，最初设想的 `example` 函数在使用丘奇编码布尔值时仍无法通过类型检查。尝试类型检查会得到：
```haskell
ghci> example bool = if bool then 5 else "hi!"
<interactive>:2:29: error:
• No instance for ‘Num String’ arising from the literal ‘5’
• In the expression: 5
In the expression: if bool then 5 else "hi!"
In an equation for ‘example’:
example bool = if bool then 5 else "hi!"
```
那么我们该如何实现呢？
### 技巧
目前我们启用了两个语言扩展使丘奇编码布尔值生效：
- `RankNTypes`
- `RebindableSyntax`
但前文提到，我们将仅用一个扩展 `RebindableSyntax` 实现依赖式 `if` 表达式。这是否意味着我们要用更少的语言扩展使丘奇编码布尔值**更强大**？没错！实际上，我们只需**删除**所有类型声明、类型签名及 `RankNTypes` 扩展，如下：
```haskell
{-# LANGUAGE RebindableSyntax #-}
import Prelude hiding (Bool(..), not, (&&), (||))
true thenBranch elseBranch = thenBranch
false thenBranch elseBranch = elseBranch
ifThenElse condition thenBranch elseBranch = condition thenBranch elseBranch
not bool thenBranch elseBranch = bool elseBranch thenBranch
(x && y) thenBranch elseBranch = x (y thenBranch elseBranch) elseBranch
(x || y) thenBranch elseBranch = x thenBranch (y thenBranch elseBranch)
toString bool = if bool then "true" else "false"
main = do
print (toString false) -- "false"
print (toString true ) -- "true"
print (toString (false && true)) -- "false"
print (toString (false || true)) -- "true"
print (toString (not true)) -- "false"
```
...不仅代码仍能通过类型检查，现在还支持依赖式 `if` 表达式！前文展示的代码直接生效：
```haskell
example bool = if bool then 5 else "hi!"
main = do
print (example false) -- "hi!"
print (example true ) -- 5
print (example (false && true)) -- "hi!"
print (example (false || true)) -- 5
print (example (not true)) -- "hi!"
```
很神奇吧？这究竟是如何工作的？
### 解释
若保留原有的类型签名，`example` 函数将无法通过类型检查，因为那些签名实际上**过于严格**。删除类型签名后，编译器会为相同代码推断出更通用的类型。为说明这一点，我将加回编译器推断的类型，从 `true` 和 `false` 的类型开始：
```haskell
true :: a -> b -> a
true thenBranch elseBranch = thenBranch
false :: a -> b -> b
false thenBranch elseBranch = elseBranch
```
`true` 最通用的类型是接受两个参数（可以是不同类型 `a` 和 `b`）且返回第一个参数类型的函数。类似地，`false` 也接受不同类型的参数，但返回第二个参数类型。为避免使用 `a` 和 `b` 这样的类型变量名，我将其重命名为 `thenBranch` 和 `elseBranch`：
```haskell
true :: thenBranch -> elseBranch -> thenBranch
true thenBranch elseBranch = thenBranch
false :: thenBranch -> elseBranch -> elseBranch
false thenBranch elseBranch = elseBranch
```
我还将引入并使用新的 `Bool` 类型，它本质上是双参数函数的别名：
```haskell
type Bool thenBranch elseBranch result = thenBranch -> elseBranch -> result
true :: Bool thenBranch elseBranch thenBranch
true thenBranch elseBranch = thenBranch
false :: Bool thenBranch elseBranch elseBranch
false thenBranch elseBranch = elseBranch
```
新的 `Bool` 类型与旧版本共享一个特征：它们都是双参数函数：
```haskell
type Bool = forall a . a -> a -> a
```
但现在两个函数参数和返回结果可以拥有不同类型。现在我们可以标注 `ifThenElse` 的类型：
```haskell
ifThenElse :: Bool thenBranch elseBranch result -> thenBranch -> elseBranch -> result
ifThenElse condition thenBranch elseBranch = condition thenBranch elseBranch
```
新类型签名保留了更多信息，表明 `result` 类型会随传入的 `Bool` 值而变化。要理解其工作原理，假设将 `true` 作为第一个参数传入 `ifThenElse`。类型检查器会对齐第一个参数与 `true` 的类型：
```haskell
ifThenElse :: Bool thenBranch elseBranch result -> ... -> ...
↕↕↕↕↕↕↕↕
true :: Bool thenBranch elseBranch thenBranch
```
...然后类型检查器会推断出 `result` 类型变量必须匹配 `thenBranch` 类型变量。接着类型检查器会修复 `ifThenElse` 类型中的不匹配，将每个 `thenBranch` 替换为 `result`：
```haskell
ifThenElse :: Bool result elseBranch result -> result -> elseBranch -> result
```
...这意味着对 `true` 应用 `ifThenElse` 会得到此类型：
```haskell
ifThenElse true :: result -> elseBranch -> result
```
...现在从类型可以看出它将返回第一个参数并忽略第二个参数。我们也可以通过 REPL 推断类型来确认正确性：
```haskell
ghci> :type ifThenElse true
ifThenElse true :: result -> elseBranch -> result
```
反之，若传入 `false`，则类型检查器会将 `result` 类型变量与 `elseBranch` 类型变量统一，得到此类型：
```haskell
ghci> :type ifThenElse false
ifThenElse false :: thenBranch -> result -> result
```
...因此，根据传入的第一个参数（哪个 `Bool`），我们会得到不同的类型！这一切之所以可行，是因为新的 `Bool` 类型在类型层面追踪了信息流。例如，明确写出 `not` 函数的通用类型：
```haskell
not :: Bool thenBranch elseBranch result -> Bool elseBranch thenBranch result
not bool thenBranch elseBranch = bool elseBranch thenBranch
```
...类型签名现在表明 `not` 交换了 "then" 和 "else" 分支。之前我们通过查看 `not` 函数的实现可以知道这一点，但现在同样的信息在类型层面被追踪。然而，泛化逻辑运算符的类型可能更难理解：
```haskell
(&&) :: Bool intermediateResult elseBranch result -> Bool thenBranch elseBranch intermediateResult -> Bool thenBranch elseBranch result
(x && y) thenBranch elseBranch = x (y thenBranch elseBranch) elseBranch
(||) :: Bool thenBranch intermediateResult result -> Bool thenBranch elseBranch intermediateResult -> Bool thenBranch elseBranch result
(x || y) thenBranch elseBranch = x thenBranch (y thenBranch elseBranch)
```
...但（在我看来）如果你略微重构实现以更贴近推断类型，它们会更合理：
```haskell
(&&) :: Bool intermediateResult elseBranch result -> Bool thenBranch elseBranch intermediateResult -> Bool thenBranch elseBranch result
(x && y) thenBranch elseBranch = x intermediateResult elseBranch
where
intermediateResult = y thenBranch elseBranch
(||) :: Bool thenBranch intermediateResult result -> Bool thenBranch elseBranch intermediateResult -> Bool thenBranch elseBranch result
(x || y) thenBranch elseBranch = x thenBranch intermediateResult
where
intermediateResult = y thenBranch elseBranch
```
经过此轻微重构，类型层面的信息流与实现层面的信息流完全对应：
- `thenBranch` 类型追踪 `thenBranch` 变量的数据流
- `elseBranch` 类型追踪 `elseBranch` 变量的数据流
- `intermediateResult` 类型追踪 `intermediateResult` 变量的数据流
最后，让我们查看布尔函数的泛化类型：
```haskell
toString :: Bool String String result -> result
toString bool = if bool then "true" else "false"
example :: Bool Int String result -> result
example bool = if bool then 5 else "hi!"
```
这些函数现在在类型中记录了根据提供的 `Bool` 值将返回的类型。在依赖类型语言中，类型会是类似：
```haskell
example :: (bool :: Bool) -> if bool then Int else String
```
...但我们可以通过向 `Bool` 类型添加更多类型参数来表达类似效果。这一切仅需约 20 行普通函数式代码，利用标准类型系统特性即可实现。
### 混合布尔值
这种方法的另一个巧妙特性是：若混合 `true` 和 `false`，推断类型会平滑降级为"未精化"的布尔类型。例如，若将 `true` 和 `false` 放入列表，推断类型为：
```haskell
bools :: [Bool result result result]
bools = [true, false]
```
...这意味着处理列表的任何函数（或 `if` 表达式）必须为 `thenBranch` 和 `elseBranch` 返回相同类型。因此，若对列表调用 `toString`，编译器不会报错，因为 `toString` 对两个分支返回相同结果类型：
```haskell
ghci> map toString [true, false]
["true","false"]
```
...但若对相同列表调用依赖式 `example` 函数，会出现类型错误，因为我们无法混合两个不同类型的分支：
```haskell
ghci> map example [true, false]
<interactive>:3:21: error:
• Couldn't match type ‘[Char]’ with ‘Int’
Expected: Bool Int String Int
Actual: Bool Int String String
• In the expression: false
In the second argument of ‘map’, namely ‘[true, false]’
In the expression: map example [true, false]
```
## 断言
若愿意启用更多扩展，你甚至可以对布尔表达式实现基本断言，强制其必须为真：
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Kind (Constraint)
import GHC.TypeLits (TypeError, ErrorMessage(..))
data AssertionFailed = AssertionFailed
type family Successful result :: Constraint where
Successful AssertionFailed = Unsatisfiable ('Text "Assertion failed")
Successful _ = ()
assert :: Successful result => Bool result AssertionFailed result -> result -> result
assert condition expression = if condition then expression else AssertionFailed
```
若 `condition` 为 `true`，`assert` 仅返回第二个参数：
```haskell
ghci> assert true 1
1
ghci> assert (true || false) 1
1
ghci> [ assert b 1 | b <- [true, true] ]
[1,1]
```
...但若为 `false`，则会出现类型错误：
```haskell
ghci> assert false 1
<interactive>:1:1: error:
• Assertion failed
• In the expression: assert false 1
In an equation for ‘it’: it = assert false 1
ghci> assert (true && false) 1
<interactive>:2:1: error:
• Assertion failed
• In the expression: assert (true && false) 1
In an equation for ‘it’: it = assert (true && false) 1
ghci> [ assert b 1 | b <- [true, false] ]
<interactive>:3:3: error:
• Assertion failed
• In the expression: assert false 1
In the second argument of ‘map’, namely ‘[true, false]’
In the expression: map (assert b) [true, false]
```
注意：此断言机制利用了 `AssertionFailed` 作为类型的特殊构造，通过类型族 `Successful` 检查类型是否有效。当 `condition` 为 `false` 时，`AssertionFailed` 不满足约束，导致编译时错误。
相似文章
记录类型推断入门指南
本文解释了静态类型语言中匿名记录类型推断的基础知识，使用了类型理论符号并以Haskell作为实现语言。
受控的存在类型
一篇技术文章，提出了一种使用线性函数和unsafeCoerce在Haskell中编码存在类型的方法，实现了无需GADT包装器的“裸”存在类型，并通过透镜组合子unsafePartsOf的安全变体进行了演示。
类型推断（第一部分）
关于类型推断的教程，涵盖Damas-Hindley-Milner类型系统、合一及相关概念，并附有OCaml代码示例。
Serokell 对 GHC 的工作：依值类型，第5部分
本文详细介绍了 Haskell 的 GHC 编译器在依值类型方面的最新进展，包括 GADTs 中的可见 forall、命名空间指定导入以及其他编译器改进。
记录拼接的机械化类型推断
本文对Mitchell Wand在1991年提出的偏记录拼接类型推断算法进行了机械化，提供了声明式与算法式语义，并给出了Haskell参考实现，以推动Nix及其他语言的类型检查进展。