Recursive subtyping revealed - Functional pearl

Algorithms for checking subtyping between recursive types lie at the core o f many programming language implementations. But the fundamental theory of these algorithms and hom they relate to simpler declarative specifications is not widely understood, due in part to the difficulty of the available in troductions to the area. This tutorial paper offers an "end-to-end" introdu ction to recursive types and subtyping algorithms, from basic theory to eff icient implementation, set in the unifying mathematical framework of coindu ction.