具有递归依赖元素的反向异构 gadt 列表

Question

看过这个关于依赖于前面元素类型的列表元素的答案，其中问题通过以下列表定义解决了：

 type ('a,'b) mlist =
  | MNil : ('a,'a) mlist
  | MCons : ('a, 'b) element * ('b,'c) mlist -> ('a,'c) mlist

其中“元素”是：

module Tag = struct
  type root = Root
  type fruit = Fruit
  (* ... *)
end
type (_,_) element=
  | Fruit : (Tag.root, Tag.fruit) element
  | Veggie : (Tag.root, Tag.veggie) element
  (* ... and so on *)

我发现它对于创建一个列表非常有用，在该列表中您想要对元素的顺序有一些规则。例如，在神经网络中创建层列表时......

我现在想要反转这个列表。所以我定义了一个新的反转列表类型，如下所示：

 type ('a,'b) rev_list =
  | RNil : ('a,'a) rev_list
  | RCons : ('b, 'c) element * ('a,'b) rev_list -> ('a,'c) rev_list

最后一个元素的类型取决于前一个元素。

但是我在反向功能上遇到了麻烦：

let rec rev : type a b c. (a, c) mac_list ->
                    (b, a) rev_list ->
                    (c, b) rev_list =
  fun lst acc -> 
  match lst with
  | MNil -> acc (* <- error *)
  | MCons (h, t) ->
     revp t (RCons (h, acc))

显然，Ocaml 抱怨返回类型与累加器的类型不匹配： 类型 (b, a) 与类型 (c, b) 不兼容 ...

但是，如果我将

(b, a) rec_list

写为返回类型，我会在最后一行（在递归函数调用时）收到错误，因为显然，

acc

中前一个列表元素的类型与下一个列表元素的类型不同我现在添加。

我认为我不能在这里使用任何存在包装器，因为（据我所知）我会丢失有关列表元素的类型信息......

虽然代码是在 Ocaml 中，但如果您有 Haskell 中的解决方案或至少有一些建议我可以在哪里搜索它，我会很高兴..

如果您知道如何限制列表或其他数据结构中元素的顺序，并且知道我还需要向后迭代它，我将不胜感激。

编辑：
看来我把问题过于简单化了，所以把它贴在这里，我的错。
但如果原来的问题是这样的呢：
我实际上已经定义了

mlist

和

rev_list

 ，如下所示：

type ('a,'b) mac_list =
  | MNil : ('a,'a) mlist
  | MCons : ('a, 'b) element * (('b,'c) element, _) mlist -> 
            (('a,'c) element, 'e) mlist

type ('a,'b) rev_list =
  | RNil : ('a,'a) rev_list
  | RCons : ('b, 'c) element * (('a,'b) element, _) rev_list ->
            (('a,'c) element, 'e) rev_list

我不确定这些定义是否有意义，但我确实需要有关“元素”内部类型的信息来迭代列表，因为我想将当前元素的“水果”或“蔬菜”传递给下一次迭代。

我的迭代代码工作正常，直到我想反转列表：

(* ... *)
type (_,_) element=
  | Fruit : Tag.root -> (Tag.root, Tag.fruit) element
 (* ... *)

let rec iter : type a b c. ((a, b) element, c) mlist -> a 
               -> unit =
  fun list input ->
  match list with
  | MNil -> ()
  | MCons (element, tail) ->
     (match element with
      | Fruit root ->
         (* processing the input *)
         let fruit : Tag.fruit = (* to fruit *) root + input in 
         iter tail fruit
     (* ... *) )

rev

功能现在如下：

let rec rev : type a b c d. ((b, c) element, d) mlist ->
                    ((a, b) element, _) rev_list ->
                    ((a, c) element, _) rev_list =
  fun lst acc -> 
  match lst with
  | MNil -> acc 
  | MCons (h, t) ->
     rev t (RCons (h, acc))

在这种情况下，无论类型的顺序如何，我在返回累加器时都会遇到错误...

Answer 1

您距离解决方案仅差一个错字， 让我们首先用更明确的类型重写

rev

函数的类型：

let rec rev : type bottom current top.
  (current, top) mlist ->
  (bottom, current) rev_list ->
  (top, bottom) rev_list =
  fun lst acc ->
  match lst with
  | MNil -> acc (* <- error *)
  | MCons (h, t) ->
     rev t (RCons (h, acc))

如果仔细观察这两个

rev_list

的类型，它们的参数顺序会有些奇怪：中间列表是

(bottom, current) rev_list

，因此在类型系统中保留了

bottom -> top

的顺序，而结果是一个

(top, bottom) rev_list

，它颠倒了类型参数的顺序。

这里存在不一致，这并不奇怪，因为这两个选择在

rev_list

的定义函数中是有效的。就您而言，您有：

type ('a,'b) rev_list =
  | RNil : ('a,'a) rev_list
  | RCons : ('b, 'c) element * ('a,'b) rev_list -> ('a,'c) rev_list

而另一个选择是

type ('a,'b) rpath =
  | RPNil : ('a,'a) rpath
  | RPCons : ('b, 'a) element * ('b,'c) rpath -> ('a,'c) rpath

请注意，您的选择保留了列表元素的方向，而第二个选择则相反。

因此，您一开始就选择了

('a,'b) mlist

的反转将是 ('a,'b) rev_list

and not

('b,'a) rev_list`。

换句话说，要修复你的函数，我们只需要一致地记住这个选择，并将返回类型设置为

(bottom,top) rev_list

而不是

(top,bottom) rev_list

：

let rec rev : type bottom current top.
  (current, top) mlist ->
  (bottom, current) rev_list ->
  (bottom, top) rev_list =
  fun lst acc ->
  match lst with
  | MNil -> acc
  | MCons (h, t) ->
     rev t (RCons (h, acc))