异构列表的元素是否可能取决于前面元素的类型？

Question

语境

我想对 Web 应用程序的路由进行建模，使其满足以下要求：

1. 可以强制执行完整的定义
2. 可以创建不完整的定义
3. 可以检查不完整的定义是否“匹配”（即包含在）完整的定义。

作为使用的示例：

type root =
  | Fruit of fruit
  | Veggie of veggie
  
and fruit =
  | Apple of apple
  | Banana of banana
  
and veggie =
  | Carrot of carrot
  
and apple = { diameter: int; cultivar: string; }
and banana = { length: int }
and carrot = { length: int; color: [`Orange | `Purple] }

有了这个，我们可以轻松创建和执行完整的定义：

let complete = Fruit (Apple { diameter = 8; cultivar = "Golden Delicious" })

但无法创建不完整的定义

let incomplete = Fruit Apple

                       ^^^^^
Error: The constructor Apple expects 1 argument(s),
       but is applied here to 0 argument(s)

因此也无法匹配不完整和完整的定义，但我们至少可以详细地实现一个忽略参数的部分相等函数：

let equal a b = match a, b with
  | Fruit (Apple _), Fruit (Apple _ ) -> true
  | Fruit (Apple _), _ -> false
  | Fruit (Banana _), Fruit (Banana _ ) -> true
  | Fruit (Banana _), _ -> false
  | Veggie (Carrot _) , Veggie (Carrot _) -> true
  | Veggie (Carrot _) , _ -> false

对可能的解决方案的模糊想法

因此，我想到了使用 GADT 树和异构列表，通过将路由定义为列表来使定义更加灵活，例如：

let route = [Fruit; Apple; { diameter = 6; cultivar = "Granny Smith" }]

然后可以将它们与模式匹配和递归一起使用，以更轻松地解构和比较它们。

不幸的是，实现这一点并不那么容易。这是我到目前为止所拥有的：

type _ root =
  | Fruit : _ fruit root
  | Veggie : _ veggie root

and _ fruit =
  | Apple : apple fruit
  | Banana : banana fruit

and _ veggie =
  | Carrot : carrot veggie

and apple = { diameter: int; cultivar: string; }
and banana = { length: int }
and carrot = { length: int; color: [`Orange | `Purple] }

type 'a t =
  | [] : _ root t
  | ( :: ) : 'b * 'a t -> 'b t

我在这里看到两个问题：

1. 'b不受 约束'a，因此任何内容都可以放入列表中，只要它以 a 开头root t，并且可能也没有办法恢复元素的类型。我认为这需要更高种类的类型，但也许有办法解决这个问题？
2. 即使我能够解决这个问题，我也不知道如何才能终止它。也许参数也可以制作成 GADT，并以 结尾unit。

Answer 1

可能存在异构列表，其中每个元素的类型取决于前一个元素并对后续类型施加约束。核心思想是要意识到每个元素需要定义它被允许在哪个上下文中以及哪个上下文中，然后就是链接匹配上下文的问题：

 type ('a,'b) t =
  | [] : ('a,'a) t
  | ( :: ) : ('a, 'b) element * ('b,'c) t -> ('a,'c) t

这里的类型('a,'b) t描述了一个异构列表，它从上下文类型开始'a，到上下文类型结束'b。它的类型定义('a,'b) element决定了允许哪些转换。

在您的情况下，元素类型可以定义为类似

module Tag = struct
  type final = Done
  type root = Root
  type fruit = Fruit
  type veggie = Veggie
end
type (_,_) element=
  | Fruit : (Tag.root, Tag.fruit) element
  | Veggie : (Tag.root, Tag.veggie) element
  | Apple : (Tag.fruit, apple) element
  | Banana : (Tag.fruit, banana) element
  | Carrot: (Tag.veggie, carrot) element
  | End: 'a -> ('a, Tag.final) element

值得注意的是，该模块Tag仅提供不与任何值关联的类型级别标记（索引）。

有了这个定义：

let fruit = [Fruit]

is a (Tag.root,Tag.fruit) element：该元素仅允许位于顶部，并且要求上下文中允许以下元素Tag.fruit。有效的下一个元素将是

module Tag = struct
  type final = Done
  type root = Root
  type fruit = Fruit
  type veggie = Veggie
end
type (_,_) element=
  | Fruit : (Tag.root, Tag.fruit) element
  | Veggie : (Tag.root, Tag.veggie) element
  | Apple : (Tag.fruit, apple) element
  | Banana : (Tag.fruit, banana) element
  | Carrot: (Tag.veggie, carrot) element
  | End: 'a -> ('a, Tag.final) element

这是一条(Tag.root,Tag.apple) t路径。End最后，一旦我们处于映射到具体类型的上下文中，就可以使用构造函数关闭路径：

let fruit = [Fruit]

而且这种构造仍然足够静态，通常可以恢复足够的类型信息来处理部分路径，但代价是一些冗余：

let rec prefix: type a b c d. (a,b) t -> (c,d) t -> bool = fun pre x ->
  match pre, x with
  | [], _ -> true
  | Fruit :: q, Fruit :: r -> prefix q r
  | Veggie :: q, Veggie :: r -> prefix q r
  | [Apple], Apple :: r -> true
  | [Banana], Banana :: r -> true
  | [Carrot], Carrot :: r -> true
  | [Apple; End x], [Apple; End y] -> x = y
  | [Banana; End x], [Banana; End y] -> x = y 
  | [Carrot; End x], [Carrot; End y] -> x = y
  | _ -> false