Σ

Σ は、依存ペア(dependent pair)型を表します。

たとえば、[(Nat, 1), (String, "hello"), (Bool, true)] というようなリストを考えてみます。 このリストに正しく型を付けるにはどうすればいいでしょうか？ 通常の直積型では、「右の要素の型が左の要素の型に依存する」ことが許されないので、型を付けることができません。

#check_failure [(Nat, 1), (String, "hello"), (Bool, true)]

しかし、依存ペア型を使うことで解決できます。 この場合、リストの中身の型は Σ (α : Type), α になります。 これは、(α : Type) × α と同じ意味です。

example : (Σ (α : Type), α) = ((α : Type) × α) := by rfl

これを使うと、次のようにリストに型を付けることができます。

def sample : List ((α : Type) × α) :=
  [⟨Nat, 1⟩, ⟨String, "hello"⟩, ⟨Bool, true⟩]