Zulip Chat Archive

Stream: general

Topic: recursive uncurry


view this post on Zulip 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?

view this post on Zulip 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 (α  β) (α × γ) δ := ...

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip Patrick Massot (Jun 22 2020 at 14:14):

Ok, I'll update soon.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 22 2020 at 14:29):

Oh, removing the out_param fixes it

view this post on Zulip Gabriel Ebner (Jun 22 2020 at 14:31):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Jun 22 2020 at 14:32):

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

view this post on Zulip Patrick Massot (Jun 22 2020 at 14:33):

Great!

view this post on Zulip 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 γ))

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 22 2020 at 14:53):

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

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 14:56):

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

view this post on Zulip Patrick Massot (Jun 22 2020 at 14:57):

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

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Jun 22 2020 at 15:01):

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

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Jun 22 2020 at 15:04):

(and no, this is not missing imports).

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 15:04):

You could use this with multilinear maps maybe

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 15:06):

If not we can just change everything back to unbundled homs

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Sep 27 2020 at 15:03):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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