haskell - 对递归数据结构施加嵌套限制

Question

考虑如下的递归数据结构:

data Tree level
    = Leaf String
    | Node level [ Tree level ]

现在，如果level是 Ord 的一个实例，我想在类型级别对数据结构施加以下限制:节点必须仅包含 Tree s 具有更高的 level .

您可以放心地假设 level是一个简单的求和类型，例如

Level
= Level1
| Level2
...
| LevelN

但是在哪里N不是先验已知的。在这种情况下，我可以让一个节点的所有子节点都具有更高的级别。

例如

tree = Node Level1
    [ Node Level2 []
    , Node Level3 []   
    ]

应该编译，同时

tree = Node Level2
    [ Node Level1 []
    ]

不应该。

是否可以在 Haskell 中模拟这样的事情？

Answer 1

这是基本思想。像这样编码递归限制的最简单方法是使用 Peano numbers 。让我们定义这样一个类型。

data Number = Zero | Succ Number

一个数字要么为零，要么是另一个数字的后继。这是在这里定义数字的好方法，因为它将与我们的树递归很好地配合。现在，我们希望 Level 是一个类型，而不是一个值。如果它是一个值，我们就无法在类型级别限制它的值。因此，我们使用 GADT 来限制初始化事物的方式。

data Tree (lvl :: Number) where
    Leaf :: String -> Tree lvl
    Node :: [Tree lvl] -> Tree ('Succ lvl)

lvl 是深度。 Leaf 节点可以有任意深度，但是 Node 节点的深度受到限制，并且必须严格大于其子节点的深度(这里严格大于其子节点的深度，这可以工作)在大多数简单的情况下。一般来说，允许它严格更大需要一些更复杂的类型级别技巧，可能使用 -XTypeInType)。请注意，我们在类型级别使用 'Succ。这是一个升级类型，通过-XDataKinds启用。我们还需要 -XKindSignatures 来启用 ::Number 约束。

现在让我们编写一个函数。

f :: Tree ('Succ 'Zero) -> String
f _ = "It works!"

此函数仅采用最多一层深度的树。我们可以尝试调用它。

f (Leaf "A") -- It works!
f (Node [Leaf "A"]) -- It works!
f (Node [Node [Leaf "A"]]) -- Type error

所以如果深度太大，编译时会失败。

完整示例(包括编译器扩展):

{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}

data Number = Zero | Succ Number

data Tree (lvl :: Number) where
    Leaf :: String -> Tree lvl
    Node :: [Tree lvl] -> Tree ('Succ lvl)

f :: Tree ('Succ 'Zero) -> String
f _ = "It works!"

这并不是你能用它做的一切。当然还有一些扩展，但它传达了要点，并希望能为您指明正确的方向。