如何定义类型安全的约束玫瑰树

Question

我正在尝试定义具有这些特征的数据结构：

这是一棵玫瑰树
树中的节点是可变排序的
节点种类之间的唯一区别是对它们可能占用的 children 数量的限制
完整的约束集是：None；仅一个;只有两个；最后一个;至少两个
我希望相关约束可以类型检查和检查。（例如，在构建或编辑树时，尝试向 IamJustOne :: OneOnly 添加第二个 child 是错误的）

我很难开始定义这个结构（尤其是第 3-5 点）。

网上有关于定义玫瑰树所需步骤的信息。
Data.Tree.Rose 中的信息足以创建具有可变节点的玫瑰树。（虽然我仍然不清楚该模块中 Knuth 树和 Knuth 森林之间的区别。）
关于异构容器的研究水平论文远远超过我的理解等级

我最初的方法是尝试创建 MyRose 的子类型（不是工作代码）：

data MyRose sub = MyRose {label :: String, subtype :: sub, children :: [MyRose sub]}
type AtLeastOne a = snoc a [a]
type AtLeastTwo a = snoc a ( snoc a [a] )
...
instance MyRose AtLeastOne where children = AtLeastOne MyRose -- instances to provide defaults
...
instance None STree where children = Nothing

我尝试了各种使用数据、新类型、class、类型的方法，现在正在研究类型族和数据族。 None 我的方法很有成效。

您能否建议定义此数据结构的指针。婴儿的第一步将非常有用 - 很难低估我在这个主题上的知识水平。

Answer 1

就算能定义，这种树好像也很难用。树的类型必须反映它的整个结构，客户端必须随身携带该类型，因为树上的所有操作都需要知道该类型才能执行任何操作。他们不能只拥有 Rose String 之类的东西，他们需要知道确切的形状。

假设您已经成功实现了目标。然后，您可能有一些示例树 t:

t :: OnlyTwo (AtLeastOne None)

表示顶层有2个节点，每个节点至少有一个child，每个都是空的。 insert t "hello" 的类型究竟应该是什么？ deleteMin t？如果删除单个节点，您无法真正知道树的哪一层可能需要折叠，或者如果插入一个节点，树的哪一层可能需要增长。

也许您对这些问题有答案，并且在一些模糊的用例中这是最佳解决方案。但是既然你要求宝宝的第一个解决方案：我想如果我是你，我会退后一步问问为什么我真的想要这个。您希望通过这种级别的类型细节实现什么？您希望客户端代码在使用或构建这样一棵树时看起来像什么？这些问题的答案将使问题更加清晰。

Answer 2

在你走疯狂的高级路线之前，我建议确保简单的路线不够好。简单的路线如下所示：

data Tree = Node { label :: String, children :: Children }
data Children
    = Zero
    | One Tree
    | Two Tree Tree
    | Positive Tree [Tree]
    | Many Tree Tree [Tree]

这是您的标准：

是一棵玫瑰树——呃，我猜？
树中的节点是可变排序的 -- 检查，五个 Children 构造函数表示排序，每个 Node 可以选择不同的构造函数
排序之间的唯一区别是对排序次数的限制 children -- check
完整的约束集 -- 检查
相关约束是类型可检查和检查的——检查，例如应用程序 One child1 child2 没有类型检查

如何定义类型安全的约束玫瑰树

How to define Type safe constrained rose trees

tree

haskell