[Well-Typed Blog] Explicit Level Imports awarded best paper at TFP 2025

Links
1

Thanks to @mpickering and @romes for all their hard work!

26 Likes
2

Congratulations! Very readable paper.

I have a question about section 5.2 “Module stages”.

If a module M splice imports module A, then compiling M@C requires compiling module A@C

I would expect it to be “requires compiling module A@R”. Shouldn’t the compilation of the example

import Control.Lens.TH (makeLenses)
import App (S)
data T = MkT { foo :: S }
$(makeLenses ′′T) -- generates foo :: Lens T S

require compiling Control.Lens.TH@R so that makeLenses may run?

1 Like
3

No. A@C means module A is compiled to be executed at the compile-time stage. In this example, makeLenses is executed at compile-time (and not at runtime), so we need Control.Lens.TH@C and not Control.Lens.TH@R.

2 Likes
4

Terrific!

By taking advantage of this extra information, the compiler can perform less work in certain situations.

However, I wonder: why do I as a user have to think about this? Why can’t the compiler figure it out? It doesn’t strike me as a fundamental way of expressing my thoughts. I don’t really care about stages when I program.

1 Like
5

Well, there are a couple of ways the compiler could figure it out:

  • The status quo, i.e. compile every module on the basis that it may be needed at any stage. This is what we want to get away from, because it’s both conceptually wrong (I expect makeLenses to run at compile time, I don’t want it linked into the final binary) and wastes compilation resources.
  • Start compiling a module before its dependencies are ready, dynamically figure out which dependencies are needed at which stages, suspend compilation, wait until the needed compile-time dependencies are available, then resume. This could work in principle but it’s very hard to implement and puts significant demands on the build system, because it breaks the assumption that the dependencies can be determined directly from the module header.

Given that neither of these approaches are really satisfactory, and adding the splice and quote annotations should make programs easier to understand, not just easier to compile, I think the extra annotation burden is worth it.

8 Likes