= Recursive type
{title2=$\mu\alpha.\tau$}
A <recursive type> explicitly names a type in terms of itself. Notation $\mu\alpha.\tau$ binds $\alpha$ within $\tau$. A <programming language> must specify whether unfolding gives type equality or requires explicit operations; this is outside the finite <simple type> grammar used here. See Benjamin C. Pierce's treatment of <recursive types> in chapters 20–21. https://www.cis.upenn.edu/~bcpierce/tapl/contents.pdf[Pierce, Types and Programming Languages (2002), author-hosted contents, chapters 20–21]{ref}
Back to article page
