Mirror of forum.nim-lang.org

8795 :: Module typing, code reuse and separate compilation

• Sixte (orginal) [2022-01-12T01:08:27+01:00] view original

  I just recently stumbled over a paper from Karl Crary:

  https://www.cs.cmu.edu/%7Ecrary/papers/2020/exsig.pdf

  which aims to solve the “avoidance problem” aka “implicit abstraction” problem. Implicit abstractions occur, if a program does take advantage of a type that it doesn’t know about. The type can then be regarded as a hidden type parameter or an erased type. Type erasure allows for code reuse. With type erasure, programs can be combined freely – e.g. by using callback functions or a dynamic link library or by a “self” parameter. Dynamic solutions/applications aside, we can factorize every program into parts that have the type erasure property. If a program can be splitted into such parts, it then can take advantage of separate compilation. But the compiler should be able to sort it out, to derive it, to prove it. By doing this, the compiler has to derive existential signatures automatically. This is a very demanding task, especially when it is not clear by forehand where to set the splits. Quote:

  • “If we split a program at an arbitrary point, the corresponding interface must be expressible using the underlying signature calculus.”

  From where should we take such a signature? Assuming that we have an appropriate signature calculus to solve this, we can go further, quote:

  • In other words, however a software project might be broken into compilation units, there exist syntactic representations of the signatures needed to mediate the boundaries between units. To clarify this, we must distinguish between two forms of separate compilation :
  • In separate compilation per se, the programmer explicitly specifies an interface for unit A, and unit B depends on A via that interface. The code for A might not be available, or even written yet. In incremental recompilation, the code for unit A is compiled, automatically generating an interface, which unit B then depends on. When the code for B changes, it can be recompiled without recompiling A.
  • In separate compilation per se, the programmer(s) determine A’s interface and they can use strong sums in the interface instead of existential signatures. In incremental recompilation, on the other hand, the programmers wish to take A’s code as is and compile against it, perhaps for build efficiency or perhaps because A is upstream code provided only in binary. Either way, A itself determines the interface. This is the situation in which “fully syntactic” signatures are relevant.
  • But existential signatures are syntactic enough for incremental recompilation. When the compiler compiles A, it writes out an interface containing the signatures inferred for A, which may include existential signatures. Since the interface is generated, nothing is ever checked against it. The contents of A are made available to B according to that interface.

  The quote continues with a rather ominous phrase:

  • Recall that the context is required to be synthesis, not user

  because the compiler already has a synthetic view on the program (by using existentials), programmer’s interface gets added then, finally, the compiler will render a new synthesis. For the programmer roughly translated into:

  “I wish… so please do something with my wishes and tell me if my dreams come true”.

  The wishes – e.g. a library design enriched with independency (a constraint) will be respected as best as possible and the compiler will give a report about the result. If the constraints can’t be respected, it will still compile but the constraint(s) will be removed : “Please redesign your library” and the compiler might even tell what needs to be changed.

  The quote ends with:

  • In summary, code that cannot be altered need not be checked against a signature, one just compiles against it, thus fitting into an incremental recompilation scenario. And, even though existential signatures cannot appear within user code, they can appear within automatically generated interfaces, which makes them syntactic enough for incremental compilation purposes.

  Crary makes clear here that he doesn’t want to change the underlying language (ML). The compiler has to be at its own, a primary goal, no burden for the programmer. But for imperative languages, the “burden” (written as constraints) might be regarded as an extra improvement.

  These are steep claims aren’t they? And what do modern programming languages typically offer for that?

---

• ElegantBeef (orginal) [2022-01-12T01:39:52+01:00] view original

  Every time you make a post like this a little part of me hopes you've discovered plain english and code examples to explain the subject, but alas to my small mind you just come off as rambling technobabble. I do wish to understand the subject and point of these posts but as I'm not an academic I can only plea with you dumb down the subject matter when posting here so others can understand and contribute thoughts. Otherwise people just go "yep" and carry on.

---

• Sixte (orginal) [2022-01-12T02:34:40+01:00] view original

  I deeply apologize for the inconvenience. A bit of an irony here: I took the quotes entirely from section 6.3 , headline "practicum". They are the least technical part of the entire paper. I added some context about the motivation , side effects and relevance for imperative languages. If you want to read some code related to the issue, I'd like to mention the thread:

  https://forum.nim-lang.org/t/8728

  You can find some C++ code there. I had preferred to give some Nim code instead. But I couldn't. So I asked for a solution in Nim. If you want to contribute - it would be highly appreciated!

---