A Logic Your Typechecker Can Count On: Unordered Tree Types in Practice

Type systems featuring counting constraints are often stud- ied, but seldom implemented. We describe an efficient im- plementation of a type system for unordered, edge-labeled trees based on Presburger arithmetic constraints. We begin with a type system for unordered trees and give a compilation into counting automata. We then describe an optimized implementation that provides the fundamental operations of membership and emptiness testing. Although each operation has worst-case exponential complexity, we show how to achieve reasonable performance in practice using a combination of techniques, including syntactic translations, lazy automata unfolding, hash-consing, memoization, and incremental tree processing implemented using partial evaluation. These techniques avoid constructing and examining large structures in many cases and amortize the costs of expensive operations across many computations. To demonstrate the effectiveness of these optimizations, we present experimental data from executions on realistically sized examples drawn from the Harmony data synchronizer.