On Tue, Jun 16, 2015 at 1:04 AM, Matt Oliveri <atma...@gmail.com> wrote: > 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?
ASTs for a well typed compiler so the latter, > 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? My reasoning is its complicated to talk about this primarily because something can be interpreted any of these ways, and frustratingly set up so that you cannot speak about type's return value, or specify some return values future type existentially, when we limit ourselves to one side of the type checking equation, yet the tools work on both, and ownership of type in the resulting language becomes underspecified, and when type class "returns" a new type class associated with a type, who owns the resulting type class, and that you can go down a class of order, but cannot go back up one... the theory is that we should be interpreting sequences of provably true theories and forcing everything, language primitives included to admit to returning a value, which can be thrown away if you really don't want it, and letting type be a regular value which just looks like the identity function on some future well defined type. its easy to fall under the spell of omniscient type values, rather than isolating phases from one another, and reusing the language. >> 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. Indeed, i mainly intended for it to use for relating to its definitions but it's "type system, which will serve as a utopic goal;" seems a good reference point, since it does not differentiate between compile-time and run-time values, so not so much the argument the paper is making, but the generic environment in which it presents its arguments. > 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. right, or to restate it, you can decide via some pure function whether you work with a runtime value or a compile time value _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
