用户定义的变量不会识别它自己的类型列表是类型

Question

由于某种原因，我收到错误消息，声称 distribute((AndC t),p) 是 cnf 而不是 cnf list... 除了 cnf list 是 cnf 的类型。为什么 OCaml 不承认这最终会提供一个列表？

问题点在第 11-12 行。

type cnf
  = AtomC of signed_atom
  | AndC of cnf list    
  | OrC of cnf * cnf

let rec distribute : cnf * cnf -> cnf = 

  let rec aux = function
    | AndC [], _
    | _, AndC [] -> AndC []
    | AndC (h::t), p -> AndC( distribute(h,p) :: distribute((AndC t),p) )
    | p, AndC (h::t) -> AndC( distribute(p,h) :: distribute(p,(AndC t)) )
    | p, q -> OrC(p, q)
  in aux

Answer 1

AndC xxx 形式的值不是列表。这是一个cnf 类型的值，它包含一个列表。但它本身并不是一个列表。

像您这样的声明定义了一个新类型cnf，以及三个新的值构造函数，AtomC、AndC、OrC。值构造函数（如名称）用于构造值。它们不是类型。

cnf 类型的每个值都将由三个构造函数之一构造。所以cnf 值的列表不是cnf 值本身。 AndC 是必需的。

更新

如果你定义了这个函数：

let mycons cnf andc =
    match andc with
    | AndC cnfs -> cnf :: cnfs
    | _ -> [cnf] (* Not possible *)

您可以像这样将:: 替换为mycons：

AndC( mycons (distribute (h,p)) (distribute ((AndC t), p)) )

（我没有对此进行测试，但我认为这个想法还可以。声称第二次调用distribute 保证返回AndC 值。）

更新 2

你可以像这样直接定义distribute而不用aux：

let rec distribute : cnf * cnf -> cnf = function
| AndC [], _
| _, AndC [] -> AndC []
(* Rewrite these ...
| AndC (h::t), p -> AndC( distribute(h,p) :: distribute((AndC t),p) )
| p, AndC (h::t) -> AndC( distribute(p,h) :: distribute(p,(AndC t)) )
 ... *)
| p, q -> OrC(p, q)