On Thu, Jul 3, 2014 at 12:42 PM, Matt Oliveri <[email protected]> wrote:
> On Thu, Jul 3, 2014 at 1:03 PM, Jonathan S. Shapiro <[email protected]> > wrote:> 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. > Perhaps. But I don't think the grammar is where the research is. And the truth is that "constructions over literals" pushes you pretty far in the direction of unifying the expression and type grammars, because literals can appear any place that a type name can appear. And then also expressions over those. So you could easily see something like List (1+2) as a **type name**, meaning the (contrived) "List of elements of type 3 : Nat". And the other thing is that you cannot entirely avoid dependence on values. Because if the type of fixed length arrays is: 'a['i : Nat] then the type of *indices* for fixed-length arrays is either "'index < 'i" or " 'index : [ 0 .. 'i :Nat ]". The latter would mean that all array indices are range types as far as the type system is concerned, which is mildly interesting. But in either case, at *some* point you need to be able to take a variable /ndx/ and index into an array /ar/: ar[v] and note that because /v/ is a variable, the types don't agree. There are a couple of ways to resolve this. One of them is to resolve this by introducing a new set of overloads for the indexing operator that invoke the range check explicitly, passing the literal type as a *type parameter* to the range check procedure. This is implemented in the runtime, and can therefore do dispatches on type that ordinary code may or may not be able to do. The point is that even within this (seemingly) limited "computation by kind classes" sort of approach, there remain places at the bottom where we need to cross the line between types and values. Eventually these are going to "leak out" into the rest of the language in the form of constraints or some such thing. I guess what I'm saying is: it doesn't feel to me like we are going to get away with "giving up" on this in the grammar, even if we don't do full dependent types. Since we can't give up, it would be nice not to shoot ourselves in the grammar in some way that might preclude going to dependent types later. > 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). > I actually don't see that as much of an issue. Propositions as types doesn't do it either, since as long as the data structure is pure you can't tell the difference between value copy semantics and reference copy semantics. > 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. Right. And if I'm understanding things right, that's what Habit is doing. But if the type-level computation language and the term-level computation language are related closely enough, it seems likely that you end up with similar grammar issues, and maybe even a lot of the same feel. I'm going to be looking for a type-level/term-level pun as much as possible. 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.) > Yes. Though I'm using "Nat" as an example for discussion. There are a bunch of other useful kinds for this sort of thing. > 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. You know, that's a very insightful way to state it. I like Geoffrey's idea of having a strictly separate, pure copy of > BitC for compile time... I do too, but we're already committed to that. Because I'm interested in complex deep-constant initializations, I need to know the subset of the language that comprises pure computation. Think of this as "constexpr" done right (assuming we *can*). It's a surprisingly tricky thing to define, because it appears to require parametric effect types. I like effect types a lot, but they have a way of introducing one hell of a lot of textual clutter. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
