OCaml 否定范式：深度模式匹配

示例

模式匹配允许解构复杂的值，并且绝不限于值表示的“最外部”级别。为了说明这一点，我们实现了将布尔表达式转换为布尔表达式的函数，其中所有否定都仅存在于原子上，即所谓的否定范式和谓词可识别这种形式的表达式：

我们定义布尔表达式的类型，其原子由字符串标识为

type expr =
| Atom of string
| Not of expr
| And of expr * expr
| Or of expr * expr

让我们首先定义一个谓词，它以否定正态形式识别表达式：

let rec is_nnf = function
| (Atom(_) | Not(Atom(_))) -> true
| Not(_) -> false
| (And(expr1, expr2) | Or(expr1, expr2)) -> is_nnf expr1 && is_nnf expr2

如您所见，可以与嵌套模式匹配。现在，我们实现一个函数，将一个布尔表达式映射为一个否定正态形式的等效布尔表达式：Not(Atom(_))

let rec nnf = function
| (Atom(_) | Not(Atom(_))) as expr -> expr
| Not(And(expr1, expr2)) -> Or(nnf(Not(expr1)),nnf(Not(expr2)))
| Not(Or(expr1, expr2)) -> And(nnf(Not(expr1)),nnf(Not(expr2)))
| And(expr1, expr2) -> And(nnf expr1, nnf expr2)
| Or(expr1, expr2) -> Or(nnf expr1, nnf expr2)
| Not(Not(expr)) -> nnf expr

第二个功能更多地使用了嵌套模式。最终，我们可以在隐含否定的条件下在顶层测试我们的代码：

# let impl a b =
Or(Not(a), b);;
  val impl : expr -> expr -> expr = <fun>
# let expr = Not(impl (Atom "A") (Atom "B"));;
val expr : expr = Not (Or (Not (Atom "A"), Atom "B"))
# nnf expr;;
- : expr = And (Atom "A", Not (Atom "B"))
# is_nnf (nnf expr);;
- : bool = true

OCaml类型的系统能够验证模式匹配的穷尽性。例如，如果我们Not(Or(expr1, expr2))在nnf函数中省略大小写，则编译器会发出警告：

# let rec non_exhaustive_nnf = function
| (Atom(_) | Not(Atom(_))) as expr -> expr
| Not(And(expr1, expr2)) -> Or(nnf(Not(expr1)),nnf(Not(expr2)))
| And(expr1, expr2) -> And(nnf expr1, nnf expr2)
| Or(expr1, expr2) -> Or(nnf expr1, nnf expr2)
| Not(Not(expr)) -> nnf expr;;
          Characters 14-254:
  ..............function
  | (Atom(_) | Not(Atom(_))) as expr -> expr
  | Not(And(expr1, expr2)) -> Or(nnf(Not(expr1)),nnf(Not(expr2)))
  | And(expr1, expr2) -> And(nnf expr1, nnf expr2)
  | Or(expr1, expr2) -> Or(nnf expr1, nnf expr2)
  | Not(Not(expr)) -> nnf expr..
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Not (Or (_, _))
val non_exhaustive_nnf : expr -> expr = <fun>

（-w @8在调用编译器或解释器时，使用选项可以将此警告视为错误。）

此功能可提高编译器接受的程序的安全性和正确性。但是，它还有其他用途，例如可以在探索性编程中使用。从正常情况下简单的函数版本开始，并使用编译器提供的不匹配案例的示例来完善处理，将转换编写为普通形式非常有趣。