haskell - 具有 'can contain' 约束的模型嵌套数据结构

Question

给定一组 A、B、C、D...，其中 A 包含 As、Bs、Cs、... 的有序列表，而 Bs 具有 Bs、Cs 的列表， Ds...等等，这样任何给定的元素都不能包含任何“更高”类型的实例，您将如何对此建模？

data Hier a = A [a] | B [a] | C [a] | D [a] 

允许这种嵌套，但不会阻止将 A 放入 B。

data A = A [ACont]
data B = B [BCont]
data C = C [CCont]
data D = D

data ACont = AA A | AB B | AC C | AD D
data BCont =        BB B | BC C | BD D
data CCont =               CC C | CD D

pattern PatAA x <- AA (A x) where
   PatAA x = AA (A x)

正确嵌套但是......糟糕。七种类型，一堆构造函数，没有明显的仿函数实例，然后一般地遍历这个结构不会很有趣。您可以使用一些模式同义词(一个节目)来稍微减轻痛苦，但不是很多。

这是可以做到的最好的吗？

Answer 1

(类似问题有答案 here )

您可以使用一些类型级别的约束来做到这一点:

data Nat = Z | S Nat

class (<=) (n :: Nat) (m :: Nat) where isLte :: n <=! m
  
instance Z <= n where isLte = LTEZ
instance n <= m => S n <= S m where isLte = LTES isLte

data (<=!) (n :: Nat) (m :: Nat) where
  LTEZ :: Z <=! n
  LTES :: n <=! m -> S n <=! S m

此代码为彼此小于或等于的(peano)数字创建了一个类，以及一个表示该事实证明的类型。

下面是你如何使用它来制作你的构造函数:

newtype Root (n :: Nat) = Root { getRoot :: [Branch n] }

data Branch (n :: Nat) where
  Branch :: m <= n => Root m -> Branch n
  
type A = Root (S (S (S Z)))
type B = Root (S (S Z))
type C = Root (S Z)
type D = Root Z

a :: [Branch (S (S (S Z)))] -> A
a = Root

b :: [Branch (S (S Z))] -> B
b = Root

c :: [Branch (S Z)] -> C
c = Root

d :: [Branch Z] -> D
d = Root

您可以看到这为您提供了正确的约束，即:

c [Branch (d [])] -- Passes
c [Branch (c [])] -- Passes
c [Branch (b [])] -- Fails typechecker