I am trying to define a data structure with these characteristics:

1. It is a rose tree
2. The nodes in the tree are of variable sort
3. The only difference between the sorts of node is a constraint on the number of children they may take
4. The complete set of constraints is: None; OneOnly; TwoOnly; AtLeastOne; AtLeastTwo
5. I want the relevant constraint to be type checkable and checked. (Eg when building, or editing the tree, trying to add a second child to IamJustOne :: OneOnly is an error)

I am having difficulty getting started defining this structure (especially points 3-5).

1. There is information on the web on the steps needed to define a rose tree.
2. There is information in Data.Tree.Rose sufficient to create a rose tree with variable nodes. (Though I am still not clear on the distinction in that module between Knuth trees, and Knuth forests.)
3. There are research level papers on heterogeneous containers well above my comprehension grade

My initial approach was to attempt to create subtypes of MyRose (not working code) as:

data MyRose sub = MyRose {label :: String, subtype :: sub, children :: [MyRose sub]}
type AtLeastOne a = snoc a [a]
type AtLeastTwo a = snoc a ( snoc a [a] )
...
instance MyRose AtLeastOne where children = AtLeastOne MyRose -- instances to provide defaults
...
instance None STree where children = Nothing

I have tried various approaches using data, newtype, class, type, and am now investigating type family and data family. None of my approaches have been productive.

Could you suggest pointers to defining this data structure. Babies first steps would be perfectly useful - it is difficult to underestimate my level of knowledge on this topic.

CodePudding user response：

Before you go the crazy advanced route, I recommend making sure that the simple route isn't Good Enough. The simple route looks like this:

data Tree = Node { label :: String, children :: Children }
data Children
    = None
    | One Tree
    | Two Tree Tree
    | Positive Tree [Tree]
    | Many Tree Tree [Tree]

Here's your criteria:

1. Is a rose tree -- uh, I guess?
2. Nodes in the tree are of variable sort -- check, the five Children constructors indicate the sort, and each Node may make a different choice of constructor
3. The only difference between sorts is a constraint on the number of children they may take -- check
4. The complete set of constraints -- check
5. Relevant constraint is type checkable and checked -- check, the application One child1 child2 does not typecheck

CodePudding user response：

Even if you could define it, a tree of this sort seems very difficult to use. The type of the tree will have to reflect its entire structure, and a client will have to carry that type around everywhere, since all operations on the tree will need to know this type in order to do anything. They won't be able to just have a Rose String or something, they will need to know the exact shape.

Let's imagine you've succeeded in your goal. Then, you may have some example tree t:

t :: OnlyTwo (AtLeastOne None)

indicating a top level with 2 nodes, each of whom has at least one child, each of which is empty. What on Earth should be the type of insert t "hello"? Of deleteMin t? You can't really know which levels of the tree may need to collapse if you delete a single node, or where you may need to grow a level if you insert one.

Maybe you have answers to these questions, and some obscure use case where this is the best solution. But since you ask for baby's first solution: I think if I were you, I would step back and ask why I really want this. What do you hope to achieve with this level of type detail? What do you want client code to look like when it consumes or builds such a tree? Answers to these questions would make for a much clearer problem.