`(a,b)` 与 `(a*b)` 在 ocaml 中

问题描述

似乎只有a * b可以适应_，只有(a,b)可以适应(a,_)。

我可以想象 a*b 是具有组件 a 和 b 的内部乘积的正确类型，而 (a,b) 是 a 类型的外部乘积并输入 b（只是猜测）

但是有区分两者的例子吗？

type zero = Z : zero
type 'a succ = S : 'a succ

type _ ptree1 =
  | Leaf : 'a -> ('a * zero) ptree1
  | Node : (('a * 'n) ptree1 * ('a * 'n) ptree1) -> ('a * 'n succ) ptree1

type (_,_) ptree =
  | Leaf : 'a -> ('a,zero) ptree
  | Node : (('a,'n) ptree * ('a,'n) ptree) -> ('a,'n succ) ptree

(* bad
type ('a * _) ptree =
  | Leaf : 'a -> ('a,'n succ) ptree
 *)

let rec last1 : type n a. (a * n) ptree1 -> a = function
  | Leaf x      -> x
  | Node (_,t) -> last1 t

let rec last : type n a. (a,n) ptree -> a = function
  | Leaf x      -> x
  | Node (_,t) -> last t

解决方法

类型构造函数在 OCaml 中有一个元数。例如，在

type ('a,'b) either =
 | Left of 'a
 | Right of 'b

类型构造函数 either 的元数为 2。而 ('a,'b) either 表示应用于两个参数 either 和 'a 的类型构造函数 'b。形式 ('a,'b) 在该语言中不存在。

但是，可以将具有 n 元数的类型构造函数编码为 1 元数的类型构造函数，并且仅限于将 n 元组类型作为参数。通常，这意味着将 either 重写为

type 'p either2 =
 | Left2 of 'a
 | Right2 of 'b
constraint 'p = 'a * 'b

let translation: type a b. (a*b) either2 -> (a,b) either = function
| Left2 x -> Left x
| Right2 x -> Right x

这里，either2 是 arity one 的类型构造函数，但参数必须是 2 元组类型。

这相当于在类型级别将 'a -> 'b -> 'c 类型的函数转换为 'a * 'b -> 'c 类型的函数。另一种观点是，类型级应用程序的编写方式类似于函数应用程序('a,'b) either 将编写为either 'a 'b，而('a * 'b) either2 将变为either2 ('a * 'b)。

如果没有 GADT，这种编码需要使用显式 constraint，因此它们不会那么频繁。对于 GADT，由于 GADT 的定义可以自由地构建自己的类型索引，因此这种选择更加明显。例如，可以将 either 的古怪版本定义为

type (_,_,_) either3 =
| Left3: 'a -> ('a list -> _,'a * unit,_) either3
| Right3: 'a -> ( _ -> 'a array,unit * 'a) either3

let translate: type a b. (a list -> b array,a * unit,unit * b) either3 -> (a,b) either =
function
| Left3 x -> Left x
| Right3 x -> Right x

这里，either3 是 arity 3 的类型构造函数，它将左右类型存储在其 3 个参数之间的所有位置。

ml ocaml ocaml