Meaning of `specialize`

Stream: mathlib4

[Eric Wieser]

Yaël Dillies said:

Is that a problem? We already have docs4#Nat.repeat

Tangential, but: what does @[specialize #[]] mean there?

[Mario Carneiro]

looks like a doc-gen bug

[Mario Carneiro]

the source only has @[specialize]

[Notification Bot]

A message was moved here from #mathlib4 > Data.Fin.Tuple.Basic mathlib4#1516 by Eric Wieser.

[Eric Wieser]

Ugh, the mobile app doesn't move replies too, sorry @Mario Carneiro

[Eric Wieser]

Mario Carneiro said:

the source only has @[specialize]

And what does that mean?

[Mario Carneiro]

if you are asking about what the @[specialize] attribute itself does, it is an instruction to the compiler to prefer to specialize this declaration for different functions passed to it, similar to what monomorphization gives you in languages like C++/Rust

[Mario Carneiro]

lean already does this by default for arguments passed in typeclasses

[Mario Carneiro]

the library-writer's advice is to put this attribute on functions that take an explicit higher order (function) argument which would benefit from monomorphization