Zulip Chat Archive

Stream: general

Topic: functor.map_const


Johan Commelin (May 29 2019 at 09:13):

I don't understand lawless functors. What is functor.map_const supposed to mean? Does every "maths" functor satisfy this?

Mario Carneiro (May 29 2019 at 09:15):

map_const is another operation available as part of functor data, which should always be the same as map ∘ const

Mario Carneiro (May 29 2019 at 09:16):

but the function slot is provided in case there is an easier or faster implementation of this composition

Mario Carneiro (May 29 2019 at 09:17):

In functor it is only a default value, but in is_lawful_functor it is required that they coincide

Mario Carneiro (May 29 2019 at 09:20):

For example, the functor (λ b, X -> b) has an efficient implementation map_const (a : A) (f : X -> B) : X -> A := λ x, a which does not have to evaluate the function f, while map (const a) f x := const a (f x) will end up evaluating f before discarding the result

Johan Commelin (May 29 2019 at 09:22):

bfhwrgg... I'm still confused.

Johan Commelin (May 29 2019 at 09:23):

Why does a maths functor always have a default value?

Johan Commelin (May 29 2019 at 09:23):

I'm missing something about endo-functors of Type, I guess.

Johan Commelin (May 29 2019 at 09:25):

Whatever, I entered some constant thing, and Lean is happy.

Keeley Hoek (May 29 2019 at 10:41):

I don't think const is saying anything about having a default value; const is just the core lean name for a constant function and functor remembers a special way to map the constant function for some reason (and this is ok because the corresponding "maths" functor is Type -> Type, and in Type for each A B : Type and b : B there is a distinguished morphism const b : A -> B)


Last updated: Dec 20 2023 at 11:08 UTC