Numbering matters: first-order canonical forms for second-order recursive types

We study a type system equipped with universal types and equirecursive 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(n2 ). 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.

• Type: Conference
• Year: 2004
• Where: ICFP
• Authors: François Pottier, Nadji Gauthier
• Keywords: ICFP 2004, O(n Log N, Programming Languages, Time O(n Log, Type Unification