The general term for this is an indexed type. Specifically what is shown here is indexed codata. Indexed data is more commonly known as generalized algebraic da

The general term for this is an indexed type. Specifically what is shown here is indexed codata. Indexed data is more commonly known as generalized algebraic data types (GADTs), which encode equality constraints at construction. GADTs are well established in FP, but codata in general is not[^1]. As far as I can tell this is partly historical and partly cultural. (Codata is basically OO. Recent FP languages, like Idris, have explicit support for codata.) More in my book: https://functionalprogrammingstrategies.com/ https://functionalprogrammingstrategies.com/ ^[1]: The degenerate form of codata is the function, which FP languages do tend to support very well.