Stream: general

Topic: simplifying composition in map

Bernd Losert (Dec 29 2021 at 21:31):

I have the following context:

h'' : r.converges (map g (map f ℱ)) (g (f x))
⊢ r.converges (map (g ∘ f) ℱ) ((g ∘ f) x)


I'm not sure how to turn h'' into the goal. I tried rw is_lawful_functor.comp_map, but that didn't help since comp_map uses <\$> and not map.

Adam Topaz (Dec 29 2021 at 21:49):

Try dsimp?

Adam Topaz (Dec 29 2021 at 21:50):

Or convert h''

Eric Wieser (Dec 30 2021 at 06:41):

Which map are you looking at? There is no docs#map

#mwe ?

Bernd Losert (Dec 30 2021 at 10:01):

Eric Wieser said:

Ah, filter.map_map worked. Thanks a lot.

Bernd Losert (Dec 30 2021 at 10:08):

convert h''

This also magically works.

Johan Commelin (Dec 30 2021 at 10:12):

"Lean doesn't do magic" -- Kenny Lau

Bernd Losert (Dec 30 2021 at 10:13):

"Any sufficiently advanced technology is indistinguishable from magic." -- Arthur C. Clarke

Bernd Losert (Dec 30 2021 at 10:16):

I've noticed that filter has certain theorems have are basically specializations of more general theorems (e.g. filter.map_map vs. is_lawful_functor.comp_map). I suppose the reason for this is because Lean can't figure out how to instantiate very general theorems in certain cases, so having a specific one is better.

Eric Wieser (Dec 30 2021 at 10:21):

docs#is_lawful_functor.comp_map isn't universe polymorphic

Eric Wieser (Dec 30 2021 at 10:22):

It requires α β γ : Type u

Eric Wieser (Dec 30 2021 at 10:23):

filter.map_map is, it requires {α : Type u} {β : Type v} {γ : Type w}

Bernd Losert (Dec 30 2021 at 10:24):

I thought the ? in Type ? means any universe. I didn't realize it was a name for a universe variable.

Eric Wieser (Dec 30 2021 at 10:30):

Have a look at src#is_lawful_functor

Yaël Dillies (Dec 30 2021 at 10:31):

Is there any reason why functors aren't universe-polymorphic btw? I can't find the source of the restriction.

Eric Wieser (Dec 30 2021 at 10:33):

Try writing the class to be polymorphic, it doesn't work

Yaël Dillies (Dec 30 2021 at 10:34):

Hmm... So that's a technical restriction, not a mathematical one?

Eric Wieser (Dec 30 2021 at 10:35):

The problem is that (f : Type u → Type v) is a quantification over types, and means that in the rest of the typeclass you can only talk about f α where α : Type u

Yaël Dillies (Dec 30 2021 at 10:35):

Yeah but this problem would go away if we did the refactor we talked about, right?

Eric Wieser (Dec 30 2021 at 10:35):

If you deal with f in the way I do in my thread about redesigning the functor typeclasses to use out_param, that problem goes away

Eric Wieser (Dec 30 2021 at 10:35):

If you deal with f in the way I do in my thread about redesigning the functor typeclasses to use out_param, that problem goes away

Yes

Ah yes!

Yaël Dillies (Dec 30 2021 at 10:36):

How's this refactor going? Do you need a helping hand?

Eric Wieser (Dec 30 2021 at 10:36):

But the functor typeclasses are hard-coded in the lean3 do notation parser

Yaël Dillies (Dec 30 2021 at 10:37):

Can Leo or Gabriel do anything about that?

Bernd Losert (Dec 30 2021 at 10:38):

What is that out_param thing? I see it every once-in-a-while in type classes.

Yaël Dillies (Dec 30 2021 at 10:38):

It's a way to stop Lean from trying to infer metavariables.

Bernd Losert (Dec 30 2021 at 10:39):

Is that similar/analogous to the {| |} stuff?

Eric Wieser (Dec 30 2021 at 10:39):

Leo could try this refactor in lean 4, if we could convince him that a) it works, and b) it's worthwhile.

Eric Wieser (Dec 30 2021 at 10:40):

docs#out_param has one line of docs I think

Yaël Dillies (Dec 30 2021 at 10:40):

The point is when you have an instance instance foo.to_bar [foo a b c] : bar a b where one variable that appears in the hypotheses does not appear in the goal. Because of the way TC inference works, when Lean looks for bar a b, it will find foo.to_bar and then look for foo a b ?c, and it will timeout trying to unify that metavariable.

Eric Wieser (Dec 30 2021 at 10:40):

Do you need a helping hand

Feel free to adopt my branch in the other thread. My goal there was simply to check that it's possible to state all the monad typeclasses in that style, not to actually replace all the old classes for new.

Yaël Dillies (Dec 30 2021 at 10:40):

So instead we make c an out_param to prevent Lean from trying to figure out what it is.

Bernd Losert (Dec 30 2021 at 10:42):

I get it. Interesting.

Mario Carneiro (Dec 30 2021 at 14:57):

Eric Wieser said:

But the functor typeclasses are hard-coded in the lean3 do notation parser

Actually I don't think this is true. It is hard-coded to make use of whatever bind resolves to, but not monads / functors specifically

Mario Carneiro (Dec 30 2021 at 15:01):

namespace foo
def bind (x : ℕ) (y : ℕ → ℕ) := y (2 * x)
def bar : ℕ := do a ← 1, 2 + a
end foo
#print foo.bar
-- def foo.bar : ℕ :=
-- foo.bind 1 (λ (a : ℕ), 2 + a)


Eric Wieser (Dec 31 2021 at 12:32):

I thought tactic mode begin end used more than just bind, but perhaps I'm mistaken

Last updated: Dec 20 2023 at 11:08 UTC