Container (type theory)

[1] For lists, the shape type is the natural numbers (including zero).

Note that the natural numbers are isomorphic to lists of units.

One of the main motivations for introducing the notion of containers is to support generic programming in a dependently typed setting.

It takes a function g to This is equivalent to the familiar map g in the case of lists, and does something similar for other containers.

This programming language theory or type theory-related article is a stub.