On Thu, Jul 3, 2014 at 1:03 PM, Jonathan S. Shapiro <[email protected]> wrote: >> I would advise that you do some hacking in at least one existing >> dependently-typed language before trying to design your own. > > 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?
My gut feeling is to say give up, don't bother. Unless you know now what you'll want to add, and make sure now that you don't do anything else to screw it up, who knows what'll happen? Dependent type systems is still an active research area. And I haven't seen anyone who has tried to combine dependent typing with unboxed types yet, other than to go all the way to formal verification (using propositions as types). >> 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. I meant immutable variables. Assuming variables are mutable by default is rather confusing for dependent typing. To make sure we're on the same page, with dependent typing, terms are programs. If you have a separate compile-time-only language for terms, then it isn't really dependent typing, it's just type-level computation. So function objects are values, for example, and you'd need a theory of equality for functions represented by their programs. The full theory for pure functions is undecidable, so that's one of the areas where dependent typing adds new design decisions. For "functions" with side effects, there _is_ no theory of equality in general. (Or rather, you have a fake theory where you pessimistically say practically nothing's equal.) You can only reason about a program running in its implicit environment, unless strong measures are taken to ensure modularity. So what I meant by literals and variables was to say maybe you could handle literals as well as immutable variables for sufficiently simple types. But it looks like you're effectively planning to do this with Nat kind. (Which falls in the category of type-level computation that isn't really dependent types.) > If we restrict ourselves to constructions over literals and types, we get a > structural theory of equality more or less for free... > > The Habit report is quite an astonishing document, because they managed to > get so much out using kinding without quite going to dependent type. Right, it sure sounds like what you want is some _other_ notion of type level computation than dependent typing. It's too bad type-level functional programming somehow got equated with dependent type systems, which are just one particularly powerful but theoretical way to do it. I blame Dependent ML (which wasn't really dependently typed). > My intuition is that [something like Habit] 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. Right. I completely agree. In fact, it seems like you really meant to be talking about type-level computation the whole time. Or that I was supposed to know that that's what you meant. :) I like Geoffrey's idea of having a strictly separate, pure copy of BitC for compile time. Like he suggests, that copy could be safely extended with dependent types (now or later) provided care is taken with the syntax. But the combination as a whole is still not dependently typed in my book, since there's no type dependency on the full language. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
