[bitc-dev] Retrospective: separate compilation and dynamic linking needs programmer knowledge?
guillaume.yziquel at citycable.ch
Mon Apr 9 14:21:05 PDT 2012
Le Monday 09 Apr 2012 à 13:44:23 (-0700), Jonathan S. Shapiro a écrit :
> However, this is only the tip of the iceberg. The entire space of
> typing/subtyping/parametrics/garbage-collection/JIT is all deeply
> inter-related. It isn't a situation where you "pick your language
> features" then "design your modular compilation system", some of these
> features are actually making it difficult if not impossible to support
> modular forward compatible separate compilation units.
I'd like to bring in the ATS language here in the picture: you
mentionned the space of
To me, ATS has an interesting and expressive type system (not perfect,
but still, quite good), has some support for subtyping and parametrics,
supports a region-based (de)allocation mechanism together with a
GC-based (de)allocation mechanism. But fails (yet) to address the JIT
end of the spectrum (which arguably is the most difficult part to
It currently is the most precise type system I've seen, and simplest AST
I've seen that addresses this spectrum. JIT is out of the picture for
multiple reasons, one of which is that it generates C code textually
(which is a reasonable design for its purposes). Which means that a lot
of info that seem to me necessary to implement JIT support are offloaded
to the C compiler. That's uncomfortable.
Still, I think ATS is a nice project on which to draw inspiration for a
"modular compilation system" skeleton:
[*] I'm not sure that the way it solves type-checking and type-inference
is the best possible (though it is indeed an achievement), but you could
likely implement a two-step "generation of constraints, solving of
constraints" solver to do the type-checking. There's lots of efforts here
to be done to write such a solver that could be specialised to
increasingly more complex and expressive type systems. And many type
system features are orthogonal to one another. So a "modular
type-checking / type-inferencing framework" does make sense to me. Would
be happy to be proved wrong.
[*] ATS type systems includes some form of subtyping and parametrics.
Not Scala-like for subtyping, and work to be done here, but research
seems to prove that it is doable (whether Scala subtyping, ML^F type
inference systems, and recent work on intersection types). Modularity
would be useful to cherry-pick features. Not only for the compiler
writer, but also as "pragmas" in the user source code, controlling what
features are useful or not at a given time.
[*] Garbage collection: ATS supports region-based (de)allocation via
linear logic, or Boehm-GC-based (de)allocation. Though not perfect (ATS
programmers tend to favor the GC-less approach) it has its merits.
Notably, it shows that it is possible to code stuff where multiple
allocation schemes do mingle. And it seems to leave room for making
multiple GCs cooperate, and even writing provably-safe GCs in ATS
itself (not yet doable I believe).
[*] As to JIT, I believe the big blocker here is generation of textual
representation of C code.
But in the end, I do not really see why, given ATS' effectiveness in
dealing with the first issues, JIT could not be handled. The difficulty
seems to me (aside from C code generation vs. typed assembly generation)
closing the loop and making the JIT runtime niceties cooperate nicely
with the type system. Linear logic and dependent types do look like they
would be darn useful here. I do not see low-level issues as being a
theoretical blocker here.
(OCa)ML dealt only with typing and garbage collection, leaving subtyping
and parametrics somewhat out of the picure. ATS closes the loop by
typing properly the garbage collection. Doesn't seem impossible to close
the loop and type properly JIT generation.
Not easy, granted. But I do not understand why a "modular compiler
framework" approach would get in the way.
More information about the bitc-dev