Zulip Chat Archive

Stream: lean4

Topic: Attribute specialize


view this post on Zulip François G. Dorais (Jan 06 2021 at 17:41):

What does the new attribute @[specialize] do?

view this post on Zulip Simon Hudon (Jan 06 2021 at 18:23):

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.

view this post on Zulip Simon Hudon (Jan 06 2021 at 18:24):

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

view this post on Zulip Andrew Ashworth (Jan 06 2021 at 18:45):

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...)

view this post on Zulip Simon Hudon (Jan 06 2021 at 18:49):

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

view this post on Zulip Simon Hudon (Jan 06 2021 at 18:50):

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)

view this post on Zulip Simon Hudon (Jan 06 2021 at 18:50):

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

view this post on Zulip Andrew Ashworth (Jan 06 2021 at 18:52):

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

view this post on Zulip Reid Barton (Jan 06 2021 at 18:54):

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

view this post on Zulip Andrew Ashworth (Jan 06 2021 at 18:54):

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

view this post on Zulip Simon Hudon (Jan 06 2021 at 18:55):

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.

view this post on Zulip Simon Hudon (Jan 06 2021 at 19:06):

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

view this post on Zulip François G. Dorais (Jan 08 2021 at 09:40):

Thank you Simon, this is very helpful!


Last updated: May 18 2021 at 23:14 UTC