## Stream: general

### Topic: recursive uncurry

#### Patrick Massot (Jun 22 2020 at 13:45):

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 (Jun 22 2020 at 14:00):

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 (Jun 22 2020 at 14:13):

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 (Jun 22 2020 at 14:14):

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 (Jun 22 2020 at 14:14):

Ok, I'll update soon.

#### Patrick Massot (Jun 22 2020 at 14:28):

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 (Jun 22 2020 at 14:29):

Oh, removing the out_param fixes it

#### Gabriel Ebner (Jun 22 2020 at 14:31):

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

#### Gabriel Ebner (Jun 22 2020 at 14:32):

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

#### Patrick Massot (Jun 22 2020 at 14:32):

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

#### Gabriel Ebner (Jun 22 2020 at 14:32):

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

Great!

#### Gabriel Ebner (Jun 22 2020 at 14:34):

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 (Jun 22 2020 at 14:51):

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 (Jun 22 2020 at 14:53):

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

#### Patrick Massot (Jun 22 2020 at 14:57):

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

#### Kevin Buzzard (Jun 22 2020 at 15:00):

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 (Jun 22 2020 at 15:01):

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

#### Patrick Massot (Jun 22 2020 at 15:03):

#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 (Jun 22 2020 at 15:04):

(and no, this is not missing imports).

#### Kevin Buzzard (Jun 22 2020 at 15:04):

You could use this with multilinear maps maybe

#### Johan Commelin (Jun 22 2020 at 15:05):

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

#### Kevin Buzzard (Jun 22 2020 at 15:06):

If not we can just change everything back to unbundled homs

#### Eric Wieser (Aug 05 2020 at 15:02):

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

#### Reid Barton (Sep 27 2020 at 14:23):

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 (Sep 27 2020 at 15:03):

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

#### Patrick Massot (Sep 27 2020 at 15:10):

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 (Sep 27 2020 at 15:19):

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 (Sep 27 2020 at 15:22):

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

Last updated: May 14 2021 at 02:15 UTC