Numbering matters
Nadji Gauthier, François Pottier · ACM SIGPLAN Notices · 2004
We study a type system equipped with universal types and equire-cursive types, which we refer to as F ͘ . We show that type equality may be decided in time O( n log n ), an improvement over the previous known bound of O( n 2 ). In fact, we show that two more general problems, namely entailment of type equations and type unification, may be decided in time O( n log n ), a new result. To achieve this bound, we associate, with every F ͘ type, a first-order canonical form , which may be computed in time O( n log n ). By exploiting this notion, we reduce all three problems to equality and unification of first-order recursive terms, for which efficient algorithms are known.