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

Question

看过this answer about the elements of a List that depend on the type of preceding elements ，问题已通过以下列表定义解决:

 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 而不是 (' b,'a) rev_list`。

换句话说，要修复您的函数，我们只需要一致地记住此选择并将返回类型设置为 (bottom,top) rev_list 而不是 (顶部，底部)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))