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

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数字.让我们定义这样一种类型.

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

所以这个问题有很多困难.尽管如此,Peano数字是一个很好的起点:

{-# 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 []

在'Node'的第二个参数中,即'[Node Level1 []]'

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

如果你想让"级别"更通用,你需要更多的扩展:

{-# 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 []   
      ]