recursive uncurry

Stream: general

[Patrick Massot]

Given topological spaces X, Y and Z, and a function f : X→ Y→ Z, we can say that f is continuous if uncurry f is continuous, which avoids putting a topology on Y → Z (yes, I know we have the compact-open topology in mathlib, but I don't want to use it here). Is there any inductive predicate magic that would generate a unified definition handling an arbitrary finite number of variables?

[Gabriel Ebner]

One possible solution is to use type-classes:

class has_uncurry (α) (β : out_param Type*) (γ : out_param Type*) := (uncurry : α → (β → γ))
instance : has_uncurry α unit α := ⟨λ a _, a⟩ -- if you like this
instance : has_uncurry (α → β) α β := ⟨id⟩
instance [has_uncurry β γ δ] : has_uncurry (α → β) (α × γ) δ := ...

[Patrick Massot]

Thanks, I'll try that. Trying to continue using the instance skeleton hole command gives me a VSCode popup saying "unknown hole command '«Instance Stub»'". Dis this break recently?

[Gabriel Ebner]

This was indeed broken for a short time and should be fixed in the current 3.16.3 version. (EDIT: even I can't remember the current Lean version.)

[Patrick Massot]

Ok, I'll update soon.

[Patrick Massot]

It seems type class resolution is not smart enough for this trick:

variables {α β γ δ : Type*}

class has_uncurry (α : Type*) (β : out_param Type*) (γ : out_param Type*) := (uncurry : α → (β → γ))

local notation `U` := has_uncurry.uncurry

instance u : has_uncurry α unit α := ⟨λ a _, a⟩ -- if you like this

instance v : has_uncurry (α → β) α β := ⟨id⟩

instance w [has_uncurry β γ δ] : has_uncurry (α → β) (α × γ) δ :=
⟨λ f, λ p, U (f p.1) p.2⟩

example {α β γ δ : Type*} (f : α → β → γ) : (α × β) → γ :=
--has_uncurry.uncurry f -- fails
@has_uncurry.uncurry _ _ _ (@w _ _ _ _ (@v _ _)) f -- works

[Patrick Massot]

Oh, removing the out_param fixes it

[Gabriel Ebner]

The other (my preferred) option is to remove the u instance.

[Gabriel Ebner]

If you remove the out param, then you always need to specify the type of the curried function manually.

[Patrick Massot]

Ok. Will I regret using this trick? Or do you think this is actually a viable path?

[Gabriel Ebner]

How is this a trick? This seems like a reasonable use of type classes to me.

[Patrick Massot]

Great!

[Gabriel Ebner]

BTW, the reason it didn't work with the u instance is because it then inferred a different domain:

[class_instances] caching instance for has_uncurry (α → β → γ) (α × β × unit) γ
@w α (β → γ) (β × unit) γ (@w β γ unit γ (@u γ))

[Patrick Massot]

It really works super nicely because it is very easy to combine with bundled functions. Now I need to find a new tiny unicode upward pointing arrow.

[Patrick Massot]

Do we use "upleftharpoon": "↿", for anything?

[Yakov Pechersky]

(https://emojipedia.org/curry-rice/)

[Patrick Massot]

Nice try, but tradition dictates it should be some kind of upward pointing arrow.

[Kevin Buzzard]

This is really cool. Does it work for products of three things? I remember @Sebastien Gouezel running into this issue maybe a year ago?

[Gabriel Ebner]

It doesn't work for products of zero things. That extension is an advanced exercise.

[Patrick Massot]

#mwe for Kevin:

open function

variables {α β γ δ ε : Type*}

example (f : α → β → γ → δ) : (α × β) × γ → δ :=
(uncurry ∘ uncurry) f

/-- Records a way to turn an element of `α` into a function from `β` to `γ`. -/
class has_uncurry (α : Type*) (β : out_param Type*) (γ : out_param Type*) := (uncurry : α → (β → γ))

notation `↿` := has_uncurry.uncurry

instance has_uncurry_base : has_uncurry (α → β) α β := ⟨id⟩

instance has_uncurry_induction [has_uncurry β γ δ] : has_uncurry (α → β) (α × γ) δ :=
⟨λ f p, ↿(f p.1) p.2⟩

variables (f : α → β → γ) (g : α → β → γ → δ) (h : α → β → γ → δ → ε)

example (a : α) (b : β) :  ↿f (a, b)=  f a b := rfl

example (a : α) (b : β) (c : γ) :  ↿g (a, b, c)=  g a b c := rfl

example (a : α) (b : β) (c : γ) (d : δ):  ↿h (a, b, c, d)=  h a b c d := rfl

example :  ↿f = uncurry f := funext (λ _, rfl)

[Patrick Massot]

(and no, this is not missing imports).

[Kevin Buzzard]

You could use this with multilinear maps maybe

[Johan Commelin]

Right... can we beef this up so that it doesn't just work with functions, but also suitable bundled homs?

[Kevin Buzzard]

If not we can just change everything back to unbundled homs

[Eric Wieser]

Can this be used for partial uncurrying? Showing ↿g (a, b, c) = g a (b, c) perhaps via type ascriptions?

[Reid Barton]

I'm sort of confused by the discussion that petered out on the PR, but clearly there ought to be some priority attributes here, right?
If I reorder the two instances of has_uncurry, then Lean picks the other one. I don't think Lean makes any guarantees about which instance it picks among ones of the same priority, does it?

[Eric Wieser]

#3694, since I can't see the pr link above

[Patrick Massot]

You can add a priority if you want. I guess that if it doesn't break the couple of uses that are in mathlib then it won't break in the sphere eversion project either.

[Reid Barton]

I'd be happier if the priorities captured the intent of someone who knows how has_uncurry is intended to be used. For example, one could either lower the priority of has_uncurry_base or raise the priority of has_uncurry_induction.

[Reid Barton]

I'm guessing the former is more sensible than the latter, but I'm extrapolating from a small amount of data.