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