On Wed, Dec 31, 2014 at 6:15 PM, Geoffrey Irving <[email protected]> wrote: > A while back shap implied that there are issues with dependently typed > languages and separate compilation.
(I don't remember that.) > 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 I don't know the details of Idris, but both of the mechanisms you described seem fine to me. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
