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

Question

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

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

现在我想告诉编译器每个特定节点都不会重复。我使用 GADTs 和 sum 类型做到了这一点

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) 时间遍历整棵树。