haskell - 递归类型是haskell，它不重复相同的构造函数

Question

我想在 Haskell 中用不同的节点标签制作一棵树。一般情况如下所示:

data Tree a
    = Leaf a
    | Node1 [Tree a]
    | Node2 [Tree a]
    ...
    | NodeN [Tree a]

现在我想告诉编译器每个特定的节点都不会重复。我使用 GADT 和总和类型实现了这一点

data Tree t a where
  Leaf  :: a -> Tree t a
  Node1 :: [Either (Tree 2 a) (Tree 3 a)] -> Tree 1 a
  Node2 :: [Either (Tree 1 a) (Tree 3 a)] -> Tree 2 a
  Node3 :: [Either (Tree 1 a) (Tree 2 a)] -> Tree 3 a

但出于多种原因，我不喜欢我的解决方案。

• 实例没有明确定义，因为您可以将 Leaf 放入 Left 或 Right 中。
• 添加另一个节点会更改所有其他构造函数的类型。
• 从外部使用这棵树会带来痛苦，因为特定树的类型取决于其根。

有更好的解决办法吗？我可以说“我想要每种类型 Tree t a 但不是 Tree 1 a”吗？

更新 1 根据 chi 的回答我做了这个

data Tag = L | A | B | C

data Tree (a :: Tag) v where
    Leaf :: l -> Tree L v
    N1 :: NotEqual a A => [Tree a v] -> Tree A v
    N2 :: NotEqual a B => [Tree a v] -> Tree B v
    N3 :: NotEqual a C => [Tree a v] -> Tree C v

type family NotEqual (a :: Tag) (b :: Tag) :: Constraint where
  NotEqual x x = TypeError (Text "forbidden Case")
  NotEqual _ _ = ()

我工作得很好，但我无法用它创建 N1 [N2 [Leaf 1], N3 [Leaf 3] ]。

Answer 1

您可能想在此处使用自定义约束，并利用 DataKinds。

下面，我只展示一个未经测试的草图。

我们首先定义标签的类型。

data Tag = T1 | T2 | ...

然后我们用禁止标签列表来注释树，即那些不能在树中使用的标签。每次我们使用构造函数时都会检查此列表。

data Tree (forbidden :: [Tag]) a where
  Leaf  :: a -> Tree forbidden a
  Node1 :: NotIn 'T1 forbidden => [Tree ('T1 ': forbidden) a] -> Tree forbidden a
  Node2 :: NotIn 'T2 forbidden => [Tree ('T2 ': forbidden) a] -> Tree forbidden a
  ...

现在我们需要定义约束。我们可以通过“禁止标签列表”进行归纳。

type family NotIn (x :: Tag) (xs :: [Tag]) :: Constraint where
   NotIn _ '[]       = ()
   NotIn x '(x :  _) = TypeError "forbidden case"
   NotIn x '(_ : xs) = NotIn x xs

这种方法的主要缺点是我们无法编写 O(1) 弱化，如

weakening :: Tree '(t : f) a -> Tree f a

为此，我们需要使用 O(N) 时间遍历整个树。