我可以禁止在另一个内部的一个特定数据构造函数，而两者都给出相同的类型

Question

我想在haskell中制作 T的类型

[Leaf 1, Rooted (Leaf 2), Branch (Leaf 3) (Branch (Leaf 4) (Leaf 5))]

但不是

[Leaf 1, Rooted (Leaf 2), Branch (Rooted (Leaf 3)) (Branch (Leaf 4) (Leaf 5))]

即。除Rooted外，所有T的构造函数都可以出现在Branch的第一个或第二个参数中（完整代码具有更多的构造函数）。

我尝试了

之类的事情

{-# LANGUAGE GADTs #-}
data T (x::Bool) where
  Leaf :: Int -> T True
  Rooted :: T True -> T False
  Branch :: T True -> T True -> T True

确保我们不能执行Branch (Rooted …) …，但也意味着我们不能进行[Rooted …, One …]，因为那将是不同类型的列表（[T True, T False]）。

我研究了datakinds，希望我可以做

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
data T where
  Leaf :: Int -> T
  Rooted :: T -> T
  Branch :: UnRooted a => a -> a -> T
class UnRooted a
instance UnRooted Leaf
instance UnRooted Branch

但是GHC（7.10.3）给出Data constructor ‘Leaf’ comes from an un-promotable type ‘T’。

有没有办法在Haskell中做到这一点？

Answer 1

如果将所有内容包装在隐藏布尔值的构造函数中，则可以使用第一个解决方案：

{-# LANGUAGE GADTs, DataKinds, KindSignatures, RankNTypes #-}
data T (x::Bool) where
  Leaf :: Int -> T True
  Rooted :: T True -> T False
  Branch :: T True -> T True -> T True
data TWrap = forall (x :: Bool). TWrap (T x)
[TWrap $ Leaf 1, TWrap $ Rooted (Leaf 2), TWrap $ Branch (Leaf 3) (Branch (Leaf 4) (Leaf 5))]

但是，如果我们必须包裹这种类型，那么最好选择更直接的解决方案来拆分类型：

data T = Leaf Int | Branch T T
data TWrap = Unrooted T | Rooted T
[Unrooted $ Leaf 1, Rooted $ Leaf 2, Unrooted $ Branch (Leaf 3) (Branch (Leaf 4) (Leaf 5))]

---

您的要求基本上是依赖类型，Haskell尚未（尚未）。