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在调用编译器或解释器时，使用选项可以将此警告视为错误。）
此功能可提高编译器接受的程序的安全性和正确性。但是，它还有其他用途，例如可以在探索性编程中使用。从正常情况下简单的函数版本开始，并使用编译器提供的不匹配案例的示例来完善处理，将转换编写为普通形式非常有趣。