Recursive type

Equirecursive types

Under equirecursive rules, a recursive type ${\displaystyle \mu \alpha .T}$ and its unrolling ${\displaystyle T[\mu \alpha .T/\alpha ]}$ are equal – that is, those two type expressions are understood to denote the same type. In fact, most theories of equirecursive types go further and essentially specify that any two type expressions with the same "infinite expansion" are equivalent. As a result of these rules, equirecursive types contribute significantly more complexity to a type system than isorecursive types do. Algorithmic problems such as type checking and type inference are more difficult for equirecursive types as well. Since direct comparison does not make sense on an equirecursive type, they can be converted into a canonical form in O(n log n) time, which can easily be compared.