What is the type system (or class of type systems) that that ensures all your tree Branches end in Leaves?

Question

I've come across this situation numerous times in the past few years where I have some classes like (pseudo-Java):

interface Node<T> { ... }

final class BranchNode<T> implements Node<T> {
    List<Node<T>> children;
}

final class LeafNode<T> implements Node<T> {
    List<T> elements;
}

If you know the height of a balanced tree in advance, you can make classes for each height of node instead of a single BranchNode class. I think Daniel Spiewak did this in his Scala PersistentVector implementation:

final class Height2Node<T> implements Node<T> {
    List<Height1Node<T>> children;
}
final class Height1Node<T> implements Node<T> {
    List<LeafNode<T>> children;
}

But if you don't know the height of the tree or need to support an arbitrary height, or only care whether a node is a Branch or a Leaf, is there a type system that can ensure that all your Branches end in Leaves?

I mean, you could walk the tree and use instanceof to find some leaf nodes and calculate the height of a given node from that and write code to ensure a balanced tree. But I'm wondering if a type system exists that can model this in such a way that it allows building a valid tree and prevents building an invalid one? If so, what is that type system, or class of type systems that can help solve this problem?

I've heard the words, "dependent types" and "higher kinded types" before. I could maybe even recognize simple examples of one or the other, but would have trouble explaining what they mean. So go easy on me, or provide links. Thanks in advance!

Answer 1

To be honest, I'm unsure about whether this is a CS question or a programming question. There is a strong programming part to it, yet encoding requirements in types requires reasoning on types which is more on the CS side. Anyway, here is an answer.

---

There are several options to encode that requirement into types.

Basically, we need to encode that each BranchNode has at least one child. This means that a leaf can only be a LeafNode.

A naive approach would be

final class BranchNode<T> implements Node<T> {
    Node<T> firstChild;
    List<Node<T>> otherChildren;
}

We can even keep only a (private) children list, and enforce that using a constructor.

// Make these private
private Node<T> firstChild;
private List<Node<T>> otherChildren;

// Make this to be the only public constructor of the class
BranchNode(Node<T> firstChild, List<Node<T>> otherChildren) {
    children = otherChildren.clone();
    children.add(firstChild);
}

Note the usual caveats, though. One can break this invariant using nulls, non termination, or by creating circular references, e.g. a BranchNode which is its own child (this is easy to achieve if the tree is mutable, for instance). Unwanted subclasses also can break the invariant.

---

Another option is to exploit the usual Church encoding of algebraic data types into polymorphic types. In theory, this is related to initial algebras and catamorphisms. In OOP practice, this is known as the "visitor pattern".

I'll pretend leaves contain a single int. One can generalize this using generics, as usual.

interface Visitor<R> {
   R visitNode(int data);
   R visitBranch(R firstChild, List<R> otherChildren);
}

interface Node {
   <R> R visit(Visitor<R> v);
}

Pseudo code follows, since Java is too heavy for writing this in a readable way, and I'm not completely familiar with its functional libraries.

class LeafNode implements Node {
  int data;
  visit(v) = v.visitNode(data);
}

class BranchNode implements Node {
  Node firstChild;
  List<Node> otherChildren;
  visit(v) = v.visitNode(firstChild.visit(v),
                         otherChildren.map(_.visit(v)));
}

The advantage of this approach is that the invariant can not really be broken by adding subclasses. One can create a new Leaf2Node subclass, but if that has the same visit(v), it will behave as LeafNode. The implementation of visit(v) in general will be limited by types, and running visit(v) will always (if terminating) end with calling v.visitNode(data) when a leaf is encountered.