GADT定义

Question

这只是一个测试，所以我不太关心，但我有以下定义：

type z
type _ s
type (_, _, _) balance =
  | Less : (*∀'a.*) ('a, 'a s, 'a s) balance
  | Same : (*∀'b.*) ('b, 'b, 'b) balance
  | More : (*∀'a.*) ('a s, 'a, 'a s) balance
type _ aVL =
  | Leaf : z aVL
  | Node : (*∀'a, 'b, 'c.*)('a, 'b, 'c) balance * 'a aVL * int * 'b aVL ->
    ('c s) aVL

我得到了"type _ aVL =“的错误：

Error: In this definition, a type variable cannot be deduced
       from the type parameters.

该怎么办呢？

Answer 1

H/T给加布里埃尔·舍勒在卡米尔-名单上回答。

不要使用这种抽象类型定义。使用(并导出)具体定义(即使您没有将它们的构造函数用于任何事情)

type 'a s = S of 'a

(或者仅仅是type 'a s = S) 它们具有“较好”的内射性。我们在邮件列表中提到过几次，这也是雅克·加里格在9月OCaml研讨会上的“轻松的一课”。

真可惜我没在谷歌搜索这个问题。这里解决了确切的问题：GADTs :无法推导类型变量