コンテナ（型理論）

数理論理学の一分野である型理論において、コンテナはリストやツリーなどのさまざまな「コレクション型」を統一された方法で表現することを可能にする抽象概念である。(単項)コンテナは、形状の型Sと、Sでインデックス付けされた位置の型ファミリPによって定義される。コンテナの拡張は、形状(型S)とその形状の位置から要素型までの関数で構成される従属ペアのファミリである。コンテナは、コレクション型の標準形式と見なすことができる。^[1]

リストの場合、シェイプ型は自然数（ゼロを含む）です。対応する位置型は、シェイプごとに、シェイプより小さい自然数の型です。

ツリーの場合、シェイプ タイプはユニットのツリーのタイプです (つまり、情報がなく、構造のみのツリー)。対応する位置タイプは、各シェイプのルートからシェイプ上の特定のノードまでの有効なパスのタイプと同型です。

自然数はユニットのリストと同型であることに注意してください。一般に、シェイプ タイプは、ユニットに適用された元の非ジェネリック コンテナー タイプ ファミリ (リスト、ツリーなど) と常に同型になります。

コンテナの概念を導入する主な動機の1つは、依存型の設定で汎用プログラミングをサポートすることです。^[1]

コンテナの拡張はエンドファンクタです。これは関数gを取り、

${\displaystyle \lambda (s,f).(s,g\circ f)}$

これはリストの場合のよく知られたものと同等でありmap g、他のコンテナーに対しても同様のことを行います。

インデックス付きコンテナ（従属多項式関数とも呼ばれる）はコンテナの一般化であり、ベクター（サイズ付きリスト）などのより広いクラスの型を表すことができます。^[2]

要素型 (入力型と呼ばれる) は形状と位置によってインデックス付けされるため、形状と位置によって変化する可能性があり、拡張子 (出力型と呼ばれる) も形状によってインデックス付けされます。

• コンテナ（抽象データ型）
• 多項式関数（型理論）

• コンテナタイプブログ