如何在类型级为递归树形数据结构施加嵌套层级限制？

Got it, let's work through this problem. You need a tree structure where every Node can only hold child trees with a strictly higher level than itself, and your level type is an open sum type (like Level1 | Level2 | ... | LevelN) with an unknown number of constructors that implements Ord. Here's a type-safe way to pull this off in Haskell using GADTs and type-level constraints:

We'll use GADTs (Generalized Algebraic Data Types) to enforce the level constraint at compile time, paired with a custom type class that formalizes "one level is higher than another". This way, the compiler will reject any tree that violates the parent-child level rule before your code even runs.

Step 1: Enable Required Haskell Extensions #

First, turn on the extensions we need at the top of your file:

{-# LANGUAGE GADTs, FlexibleInstances, ConstraintKinds #-}

Step 2: Define Your Level Sum Type #

Define your level type as a simple sum type, making sure to derive Ord with the correct hierarchy (e.g., Level1 < Level2 < Level3). You can add more constructors later as needed:

data Level = Level1 | Level2 | Level3 deriving (Eq, Ord, Show)

Step 3: Define a "Higher Than" Type Constraint #

Create a type class that acts as a proof that one level is strictly higher than another. We don't need any methods—this is just a compile-time constraint:

class HigherThan l l' where
  -- No methods needed; this exists purely to enforce level hierarchy

Now add instances for every valid parent-child level pair. For our example Level type:

instance HigherThan Level1 Level2
instance HigherThan Level1 Level3
instance HigherThan Level2 Level3

Step 4: Define the Tree GADT #

Rewrite your Tree type as a GADT, adding the HigherThan constraint to the Node constructor to ensure all children have a higher level than the parent:

data Tree l where
  -- Leaf: Can hold a string, tied to a specific level l
  Leaf :: l -> String -> Tree l
  -- Node: Holds a level l, and a list of children with level l' (proven to be higher than l)
  Node :: HigherThan l l' => l -> [Tree l'] -> Tree l

If you prefer leaves to be unbound to a specific level (i.e., a leaf can be treated as any level), you can simplify the Leaf constructor to:

Leaf :: String -> Tree l

Example Usage #

Valid Tree (Compiles Successfully) #

This tree follows the rules: a Level1 node has Level2 children, which in turn have Level3 children:

validTree :: Tree Level1
validTree = Node Level1
  [ Leaf Level2 "First child"
  , Node Level2 
      [ Leaf Level3 "Grandchild 1"
      , Node Level3 [Leaf Level3 "Great-grandchild 1"]
      ]
  ]

Invalid Tree (Fails to Compile) #

This tree tries to put a Level1 child under a Level2 node—compiler will throw an error because there's no HigherThan Level2 Level1 instance:

-- This will NOT compile!
invalidTree :: Tree Level2
invalidTree = Node Level2 [Leaf Level1 "Invalid child"]

Extending the Level Type #

When you add a new level constructor (e.g., Level4), you just need to:

1. Add it to the Level sum type:

   data Level = Level1 | Level2 | Level3 | Level4 deriving (Eq, Ord, Show)
   

2. Add new HigherThan instances for all valid pairs:

   instance HigherThan Level1 Level4
   instance HigherThan Level2 Level4
   instance HigherThan Level3 Level4
   

This keeps the system flexible even with an unknown number of levels upfront.

内容的提问来源于stack exchange，提问作者marcosh