对递归数据结构施加嵌套限制 [英] Impose nesting limits on recursive data structure

问题描述

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

Consider a recursive data structure like the following:

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

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

Now, if level is an instance of Ord, I would like to impose at the type level the following limitation on the data structure: a node must contain only Trees with a higher level.

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

You can safely assume that level is a simple sum type like

Level
= Level1
| Level2
...
| LevelN

，但是先验未知 N .在这种情况下，我将能够使节点的所有子节点具有更高的级别.

but where N is not known a priori. In this case I would be able to have that all the subnodes of a node have a higher level.

例如

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

应该编译，而

tree = Node Level2
    [ Node Level1 []
    ]

不应该.

是否可以在Haskell中为此类事物建模?

Is it possible to model such a thing in Haskell?

推荐答案

所以这个问题有很多困难.但是，Peano数字是一个不错的起点:

So there are a number of difficulties with this question. Peano numbers are a good place to start, though:

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE ConstraintKinds           #-}

data Nat = Z | S Nat

接下来，我们需要某种方式说一个数字是更大"的数字.比另一个.为此，我们可以先为"n小于或等于m"定义一个归纳类.

Next, we'll need some way of saying one number is "bigger" than another. We can do so by first defining an inductive class for "n is less than or equal to m"

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

然后我们可以定义小于".就此而言:

We can then define "less than" in terms of this:

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))))

然后，根据需要，第一个示例将进行编译:

And, as desired, the first example compiles:

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

第二个却没有:

tree = Node Level2
    [ Node Level1 []
    ]

仅出于额外的乐趣，我们现在可以在添加自定义类型错误"对话框中添加"(这将需要 UndecidableInstances :

Just for extra fun, we can now add a "custom type error" (this will need 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 []
    ]

您得到以下信息:

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

• Nodes must contain trees of a higher level

•在表达式中:节点Level1 []

• In the expression: Node Level1 []

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

In the second argument of ‘Node’, namely ‘[Node Level1 []]’

在表达式中:Node Level2 [Node Level1 []]

In the expression: Node Level2 [Node Level1 []]

如果您想进行级别"设置，更通用，您将需要更多扩展:

If you want to make "level" more generic, you'll need a couple more extensions:

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

这篇关于对递归数据结构施加嵌套限制的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！