Container (type Theory) - Indexed Containers

Indexed containers (also known as dependent polynomial functors) are a generalisation of containers, which can represent a wider class of types, such as vectors (sized lists).

The element type (called the input type) is indexed by shape and position, so it can vary by shape and position, and the extension (called the output type) is also indexed by shape.

Read more about this topic:  Container (type Theory)