deconstruct sigma types

Stream: general

[Kevin Buzzard]

-- works fine
example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ (x : (Σ (a : α), f a)), x.1

-- doesn't work
example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ (⟨s,t⟩ : (Σ (a : α), f a)), s
-- invalid binder, identifier expected
-- and other errors

Can't I take a sigma type apart like this? Isn't a sigma type just a structure? I suspect I'm missing a trick?

[Kenny Lau]

nooooo

[Kenny Lau]

don’t deconstruct things in definitions

[Kevin Buzzard]

-- works
example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ (x : (Σ (a : α), f a)), let ⟨s,t⟩ := x in s

[Kevin Buzzard]

Is this better Kenny?

[Kevin Buzzard]

Or still bad?

[Mario Carneiro]

drop the type ascription

[Kevin Buzzard]

Heh, why would this help?

[Mario Carneiro]

the syntax for lambda match is λ ⟨s,t⟩, ... with no type ascriptions permitted

[Kevin Buzzard]

Oh!

[Mario Carneiro]

the ⟨s,t⟩ is not actually a pair even though it looks like one

[Mario Carneiro]

it's just syntax

[Kevin Buzzard]

Kenny says it's a bad idea -- is the let thing OK or is it a bad idea for the same reason?

[Mario Carneiro]

it's the same

[Kevin Buzzard]

-- works
example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ ⟨s,t⟩, s

[Mario Carneiro]

The simpler way is just to pattern match right from the start

[Mario Carneiro]

example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α
| ⟨s,t⟩ := s

[Mario Carneiro]

I think the reason Kenny doesn't like those definitions is because it creates an auxiliary, and it doesn't unfold unless it's an explicit pair

[Mario Carneiro]

as opposed to

example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ p, p.1

[Johan Commelin]

It would be nice if what Kevin wants would just be syntactic sugar for the p, p.1 version...

[Johan Commelin]

But I guess syntactic sugar will only take you so far...

[Mario Carneiro]

this is a thing: they are called lazy pattern matches in haskell, and they've been discussed on this chat before

[Patrick Massot]

Yeah, this is a very common fantasy on this chat

[Kevin Buzzard]

Reality: set.image (λ x, let (⟨⟨⟨j,k⟩,f⟩,r⟩ : (Σ y : (Σ x : J × J, (R x.1) → (R x.2)), R y.1.1)) := x in (X ⟨j,r⟩ - X ⟨k,f r⟩)) {x | x.1 ∈ F})

[Kevin Buzzard]

well, that's actually just a small piece of the reality

[Kevin Buzzard]

We're making colimits in the category of commutative rings!

[Kevin Buzzard]

Without it, it will be x.1.1.1 everywhere