A while back shap implied that there are issues with dependently typed languages and separate compilation. Given that bitc intends to exist before our field makes major advantages in proof automation, it seems unlikely that bitc will be dependently typed. That said, is it not-too-offtopic if I occasionally start threads about dependent types, and in particular how they interact with systems languages and high performance languages? If not, where should such questions go?
------------------------------------------- In any case, the first question is: what are the said issues with separate compilation? It seems that Idris has this solved already, at the language level if not in the actual implementation, via its three notions of symbol export: 1. private: Invisible externally 2. abstract: Only the type is visible externally 3. public: Both type and implementation are visible externally Before writing this sentence, I was fairly confident that if compilation unit A depended on only abstract exports of compilation unit B, A could be compiled once the type declarations of B are known but before B is compiled. After writing the previous sentence, I am less sure, since the compilation of A entails arbitrary execution of code whose safety may depend on whether said types in B are inhabited. However, there seems to be an easy fix: treat everything as a module, or in other words a dependently typed struct. If module A wants to be compiled in parallel with module B, generate a interface type BT such that B : BT and compile A as A : BT => AT This enforces that the compilation of A can't access anything in BT, any more than the compilation of a function can access an actual value of its argument type. Are there any issues that I'm missing? Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
