容器（类型理论）

在类型理论中，容器是一种抽象，它允许各种集合类型，如列表和树，以统一的方式表示。容器的扩展是由一个形状（S型）和一个位置（P型）组成的依赖对家族，其中包括一个形状（S型）和一个从该形状的位置到元素类型的函数。容器可以被看作是集合类型的典范形式。对于列表，形状类型是自然数（包括零）。相应的位置类型是小于形状的自然数的类型，对于每个形状。对于树，形状类型是单位的树的类型（也就是没有信息的树，只有结构）。对应的位置类型与每个形状的从根到形状上的特定节点的有效路径类型是同构的。请注意，自然数与单位列表是同构的。一般来说，形状类型将总是与应用于单元的原始非通用容器类型系列（列表、树等）同构。引入容器概念的主要动机之一是在依赖类型的环境中支持通用编程。

容器的扩展是一个endofunctor。它把一个函数g带到在列表的情况下，这相当于我们熟悉的映射g，对其他容器也有类似的作用。

索引型容器（也被称为依赖多项式向量）是容器的一种概括，它可以表示更广泛的类型，比如向量（大小的列表）。元素类型（称为输入类型）是由形状和位置来索引的，所以它可以因形状和位置而变化，而扩展（称为输出类型）也是由形状来索引的。