Attribute specialize

Stream: lean4

[François G. Dorais]

What does the new attribute @[specialize] do?

[Simon Hudon]

It is an instruction to the compiler. If you write a function def foo {m a} [Monad m] : Int -> m a, the straightforward way to generate code is to make it a higher-order function that takes bind and pure as parameter. Invoking parameters is typically slow and foo can be made more efficient if new code is generated by the compiler for every monad with which foo is being called.

[Simon Hudon]

This is useful in general when taking type class instances as parameter but also when simply taking functions as parameters.

[Andrew Ashworth]

Interesting! How do I find out what specializations the compiler has generated? Will it inline small functions? What happens to functions when I provide a second function with a more specific type signature? (I am just now starting to read about the details of Lean 4...)

[Simon Hudon]

There are options you can set (something like set_option compiler.ir true, I don't remember the exact name of the option) that causes the output of various stages of the compiler to be printed out

[Simon Hudon]

It is extremely useful when you want to make sure that large data structures are actually used in a linear manner (and that destructive updates are enabled)

[Simon Hudon]

What do you mean by "when I provide a second function"? What does the second function do?

[Andrew Ashworth]

ahh, I am thinking in terms of C++, like how the compiler chooses the correct template specialization

[Reid Barton]

I guess as a 1st order approximation you can take https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pragmas.html#specialize-pragma as the documentation

[Andrew Ashworth]

I realize it came out yesterday so if the answer is: read the source code, that is OK

[Simon Hudon]

Ah! I see! This is not like template specialization. With template specialization, the user provides different "versions" of the same declaration. Here, the compiler see your definition of mmap (for instance), sees that you use it with the state monad and generates code for mmap that specifically uses your state monad. That is to say that calls to bind and pure are statically bound instead of dynamically bound.

[Simon Hudon]

Actually, in the case of mmap f, you can specialize further and bind statically the exact function f being passed as a parameter. That function is often a lambda abstraction and the specialization also saves us from allocating a thunk at run time

[François G. Dorais]

Thank you Simon, this is very helpful!