functor.map_const

Stream: general

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

bfhwrgg... I'm still confused.

[Johan Commelin]

Why does a maths functor always have a default value?

[Johan Commelin]

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

[Johan Commelin]

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

[Keeley Hoek]

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)