On Wed, Jul 2, 2014 at 12:57 PM, Matt Oliveri <[email protected]> wrote:
> The defining characteristic of dependent type systems is not types as > terms, but type checking depending on the execution of terms. Clearly > literal types avoids both, but even true dependent type systems do not > need to be able to use types as terms. That's a consequence of > universe types. > Thanks for the distinction, and that's an *excellent* way of stating what a dependent type system is. > I would advise that you do some hacking in at least one existing > dependently-typed language before trying to design your own. There's a > surprising pile of new subtleties once you take dependent types > seriously. > Yes. I had come to that conclusion as well. But it leaves me hesitant, because it would be nice to be able to evolve in the direction of dependent type later, so I'd like to keep the current BitC grammar open to it as a future expansion. Any thoughts on how to accomplish that? > What I'm coming to, here, is that I think at this stage I should stick to > > what I know, which is the literal types part of all this. That's pretty > > powerfully expressive already, and within the realm of what can be > > explained. > > Literally just literals though? What about variables? Basically the > trouble only comes in once you start needing a theory of equality for > values. (To get a theory of equality for dependent types.) You said two very different things there, so let's draw them out. Variables are mutable; they are not merely bindings (which are terms). A theory of equality for *terms* is comparatively tractable. A theory of equality for *variables* is quite another thing. If we restrict ourselves to constructions over literals and types, we get a structural theory of equality more or less for free. We can even define type-level operators that perform constructions and deconstructions (inspections?), so long as they converge in certain ways. For example we can do three-function type-level arithmetic on integer literals (excluding divide). The key to it is that we restrict ourselves to link-time computable type expressions, and further restrict ourselves to type expressions whose link-time computability can be witnessed at unit-of-compilation compile time. The Habit report is quite an astonishing document, because they managed to get so much out using kinding *without* quite going to dependent type. If it isn't fresh in your mind, it's worth a look: http://hasp.cs.pdx.edu/habit-report-Nov2010.pdf My intuition is that this is the right kind of balance point to seek initially for BitC. Disclosure: Marc Jones and I had some long talks about what kinds of things OS people need to be able to express. The way that the HASP team put those and other ideas into Habit astonishes, delights, and surprises me. Getting back to your point above, no, I do *not* want to step over the line into depending on variables. I think we want to set the line - at least for now - at terms derived by construction and (possibly) by compile-time type-level computation. I'm treading a very deliberate line here in that I am *not* allowing variables generally to appear in types. I think there is a complexity cliff there, both for the user and for the compiler, that is potentially insurmountable. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
