On Tue, Jun 16, 2015 at 2:52 AM, Matt Rice <ratm...@gmail.com> wrote: > So, I was reading this paper about phase distinction (something I > haven't been sure what to call until now), > > and it occurred to me that a statically typed AST, with statically > typed sub-trees may require more interesting forms of phase separation > than is typically seen, in the form of an expression for producing the > type of the sub-tree
Which notion of "statically typed AST"? Shap's/mine, which can be done in simply-typed languages, or ASTs of (only) well-typed programs, which require fancier type systems? Either way, I don't actually see what it has to do with phase distinction. The type of an AST is compile-time, and the AST itself is runtime (or it can be either, with dependent types), no matter how complex the type is. Can you explain your reasoning? > http://lucacardelli.name/Papers/PhaseDistinctions.A4.pdf I started reading this, but it's hard to take seriously, since it's so old, and it starts by seeming to say that dependent type systems lack a phase distinction, and thus can't be compiled. Dependent types look impossible if you assume all code belongs to a certain (unique) phase. But the better way to think about it is that code in a dependent type system possibly belongs to both phases. To find out if it's actually needed at runtime, just do dead code elimination, starting from main (or whatever runtime entry points you consider your module to have). Ho hum. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
