7
$\begingroup$

I am trying to understand the concept of dependent sum types ($\Sigma$ types) using concrete examples. The example given in Theorem Proving in Lean 4 seems to be a degenerate case rendering the regular Cartesian product (if I understand it correctly):

universe u v

def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
  ⟨a, b⟩

def h1 (x : Nat) : Nat :=
  (f Type (fun α => α) Nat x).2

Searching around, I found some interesting Agda examples that the $\Sigma$ type can be used to express:

  • disjoint unions
  • subsets, and
  • existential quantification.

I don't know Agda and cannot understand the examples there.

Can someone help explain the $\Sigma$ types in those examples in Lean 4?

$\endgroup$
1
  • $\begingroup$ Note that the example is only degenerate in the sense that it introduces a pair and then immediately projects out of it. It is, nonetheless, a dependent pair, of type (t : Type) × t. You can read that as “a pair of a type t together with a value of type t”. $\endgroup$
    – James Wood
    Feb 21, 2022 at 23:41

2 Answers 2

4
$\begingroup$

I would like to warn you that dependent product type is usually used for the dependent function type, while the dependent version of the product type is referred to as the dependent sum type. Personally, I would try my best to avoid confusions, so I use the names "Pi types" and "Sigma types".

I wrote this answer to learn some Lean4, as I've never used Lean4 before. I appreciate nitpicks on my code.

Disjoint union

This is a disjoint union of the type A and B, represented using a Sigma type:

def DisjointUnion (A B : Type) : Bool → Type
| true => A
| false => B

def disjoint_union (A B : Type) :=
  (b : Bool) × DisjointUnion A B b

To pattern match on a disjoint union defined above, we use Bool as the "type tag" of usual disjoint unions:

def use_disjoint_union : (disjoint_union Bool Nat) → Nat
| ⟨true, true⟩ => 0
| ⟨true, false⟩ => 1
| ⟨false, n⟩ => n -- `n` is of type `Nat`, so this checks

Note how the second component of the sigma type vary by the first component's value.

Subsets

Here's a subset of Nat that only have numbers less than or equal to 3:

def Subset := (a : Nat) ×' (a ≤ 3)
def subset_instance : Subset := ⟨2, Nat.le_step (Nat.le_refl 2)⟩

In other words, when you construct an instance of Subset, you need to show a natural number and prove it to be less than or equal to 3. This is, in my understanding, similar to defining a subset using an injective map.

This is also an existential quantification: that there exists natural numbers less than or equal to 3. You may replace the right hand side of × with any proposition about a to make your own favorite existential quantification.

Here's a minor addition: if you want to understand the sigma types in the Agda code, for example Σ ℕ (λ x → x < n) this expression, you split it into three parts with the Σ symbol ignored: , λ x →, and x < n; and then you reform it as (x : ℕ) × (x < n).

$\endgroup$
6
  • $\begingroup$ Thanks. Could you explain the b variable in def disjoint_union (A B : Type) := (b : Bool) × DisjointUnion A B b a little bit? It's not defined prior, and does not seem to be a parameter of a function. $\endgroup$
    – tinlyx
    Feb 21, 2022 at 23:02
  • $\begingroup$ Also, I tried #check (⟨false, 1⟩ : disjoint_union Bool Nat) and got an error failed to synthesize instance OfNat (DisjointUnion Bool Nat false) 1Lean 4 $\endgroup$
    – tinlyx
    Feb 21, 2022 at 23:03
  • $\begingroup$ @tinlyx (x : A) × B binds x in the expression B. So, in that example, the first occurrence of b is a binding occurrence (standing for the Boolean value the first component of the pair may have), and the second occurrence refers back to this binding. It would make sense for an explanation like this to make its way into the answer, in the right place. $\endgroup$
    – James Wood
    Feb 21, 2022 at 23:42
  • $\begingroup$ @mudri Thanks. So, is (x: a) \x B some kind of lambda abstraction? $\endgroup$
    – tinlyx
    Feb 21, 2022 at 23:45
  • $\begingroup$ @tinlyx it's a binding, but definitely not a lambda abstraction. In Agda, they use lambda abstraction to represent the latter expression, but in Lean, there's a special syntax. Beware that this is a type, and lambda abstraction is a way to make a term. $\endgroup$
    – ice1000
    Feb 22, 2022 at 0:01
1
$\begingroup$

Here an example from group theory:

Consider a family of groups Π (i : ι), G i (which is using the Pi-type to say that for every index i of some index type ι we have a group G i, and you want to work with words built from the elements of all the groups.

A good data type to for words is of course list …, but what is the type of the elements? list (G i) would be words with elements from just G i, for some fixed i.

This is where the Sigma-type comes into play: It allows us to say “an element of G i of some i“, and we end up with list (Σ (i : ι), G i) as the type of words with elements from all the groups.

(Of course, in this example I didn’t actually use that the G i are groups, and this could be phrased as “words over an alphabet”, but maybe with groups it is a bit more intuitively useful.)

$\endgroup$
1

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.