Impose nesting limits on recursive data structure

Question

Consider a recursive data structure like the following:

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

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.

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

Level
= Level1
| Level2
...
| LevelN

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.

For example

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

should compile, while

tree = Node Level2
    [ Node Level1 []
    ]

should not.

Is it possible to model such a thing in Haskell?

Answer 1

Here's the basic idea. The easiest way to encode recursion limits like this is to use Peano numbers. Let's define such a type.

data Number = Zero | Succ Number

A number is either zero or the successor of another number. This is a nice way to define numbers here, as it will get along nicely with our tree recursion. Now, we want the Level to be a type, not a value. If it's a value, we can't limit its value at the type level. So we use GADTs to restrict the way we can initialize things.

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

lvl is the depth. A Leaf node can have any depth, but a Node node is restricted in its depth and must be strictly greater than that of its children (here, strictly one greater, which works in most simple cases. Allowing it to be strictly greater in general would require some more complicated type-level tricks, possibly with -XTypeInType). Notice that we use 'Succ at the type level. This is a promoted type, enabled with -XDataKinds. We also need -XKindSignatures to enable the :: Number constraint.

Now let's write a function.

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

This function only takes trees that go at most one level deep. We can try to call it.

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

So it will fail at compile-time if the depth is too much.

Complete example (including compiler extensions):

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

This isn't everything you can do with this. There's certainly expansions to be made, but it gets the point across and will hopefully point you in the right direction.