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

Question

考虑如下所示的递归数据结构：

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

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

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

Level
= Level1
| Level2
...
| LevelN

但N在哪里先验地不知道。在这种情况下，我将能够使节点的所有子节点都具有更高的级别。

例如

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

应该编译，而

tree = Node Level2
[ Node Level1 []
]

不应该。

有可能在哈斯克尔中模拟这样的事情吗？

Answer 1

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

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!"

这不是您可以对此执行的所有操作。当然还有扩展要做，但它能抓住重点，希望能为你指明正确的方向。

Answer 2

所以这个问题有很多困难。不过，皮亚诺数字是一个很好的起点：

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE ConstraintKinds           #-}
data Nat = Z | S Nat

接下来，我们需要某种方式来表示一个数字比另一个数字"大"。我们可以通过首先定义一个归纳类来做到这一点 "n 小于或等于 m">

class (n :: Nat) <= (m :: Nat)
instance Z <= n
instance n <= m => (S n <= S m)

然后，我们可以根据以下内容定义"小于"：

type n < m = S n <= m

最后，这里是树和关卡：

data Tree n where
Leaf :: String -> Tree n
Node :: n < z => Level z -> [Tree z] -> Tree n
data Level n where
Level0 :: Level Z
Level1 :: Level (S Z)
Level2 :: Level (S (S Z))
Level3 :: Level (S (S (S Z)))
Level4 :: Level (S (S (S (S Z))))

并且，根据需要，第一个示例编译：

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

虽然第二个没有：

tree = Node Level2
[ Node Level1 []
]

只是为了增加乐趣，我们现在可以添加一个"自定义类型错误"(这将需要UndecidableInstances：

import GHC.TypeLits (TypeError, ErrorMessage(Text))
instance TypeError (Text "Nodes must contain trees of a higher level") => S n < Z

所以当你写：

tree = Node Level2
[ Node Level1 []
]

您将获得以下内容：

• 节点必须包含更高级别的树

• 在表达式中：节点级别 1 []

在"节点">

的第二个参数中，即"[节点级别 1 []]">

在表达式中：节点级别 2 [节点级别 1 []]

如果你想使"level"更通用，你还需要几个扩展：

{-# LANGUAGE TypeApplications, RankNTypes, AllowAmbiguousTypes, TypeFamilies #-}
import qualified GHC.TypeLits as Lits
data Level n where
Level0 :: Level Z
LevelS :: !(Level n) -> Level (S n)

class HasLevel n where level :: Level n
instance HasLevel Z where level = Level0
instance HasLevel n => HasLevel (S n) where level = LevelS level

type family ToPeano (n :: Lits.Nat) :: Nat where
ToPeano 0 = Z
ToPeano n = S (ToPeano (n Lits.- 1))

node :: forall q z n m. (ToPeano q ~ z, HasLevel z, n < z) => [Tree z] -> Tree n
node = Node level

tree =
node @1
[ node @2 []
, node @3 []   
]