Option-Trees

In ML (and Coq, and Haskell by another name) there is a type operator called option; an option X is either the special value None or else a value of type X. It's the strongly-typed language version of a value that might be the null-pointer.

A (tree (option X)) is a tree whose leaves are option X's.

Given an option-tree, you can get back the unique list X consisting of its leaves, in order. In the reverse direction the mapping is not unique.

If there is one thing I've suffered greatly in order to learn about dependently-typed programming, it is that one should never attempt to concatenate lists. If you find yourself doing this, you probably ought to be using option-trees instead.

I don't know for sure why this advice is so useful, but here are three clues:

  1. The theory of lists undecidable because it is the same as the theory of monoids (one binary operator, an axiom making it associative, one constant, and axioms making it neutral). Even the theory of semigroups (take away the constant) is still undecidable. But the theory of trees is the same as the theory of magmas (one binary operator, no axioms) and of option-trees (one binary operator, one constant, no axioms)

    Why worry about this? Typechecking must be decidable. If your types are able to interpret an undecidable theory, you will necessarily encounter valid terms which the type-checker cannot accept in the absence of some human-provided proof about equality between types. Equality between types (rather than values) is, at the moment, a very poorly-understood (and poorly developed) part of type theory.

  2. Strict monoidal categories are evil. Option-trees are to lists what monoidal categories are to strict monoidal categories.

  3. (Most vague:) redundant representations are a very powerful tool in computer science. Observe that decrementing an n-bit counter takes O(log n) time using the usual binary representation; there is a way to get O(1)-time decrements by allowing three possible values for each bit (but remaining at radix-2). The multiple redundant option-tree representations for a particular list seem to add just the right amount of flexibility in the same way.



rendered from WIX