On Fri, Jul 4, 2014 at 3:04 AM, Gabriel Dos Reis <[email protected]> wrote: > > > On Wednesday, July 2, 2014, Geoffrey Irving <[email protected]> wrote: >> >> On Wed, Jul 2, 2014 at 12:19 PM, Geoffrey Irving <[email protected]> wrote: >> > On Wed, Jul 2, 2014 at 11:04 AM, Jonathan S. Shapiro <[email protected]> >> > wrote: >> >> Thanks, William. The pointer to Idris is really helpful. Their tutorial >> >> is >> >> kind of interesting, since the sections on dependent types don't >> >> actually >> >> use dependent types! >> >> >> >> I have to say that I'm waffling here, for three reasons. >> >> >> >> First, most of the simple use-cases turn out to involve literals, and >> >> we >> >> simply don't need dependent type for that. Admitting literals into >> >> types >> >> goes right up to the edge of true dependent types, but it does not step >> >> over >> >> the line of turning types into terms. I think it's very clear what the >> >> benefit of "literal types" (there's a proper term, but that's what I've >> >> been >> >> calling them here) into BitC. I also think that's a step that is small >> >> enough to be readily explained to programmers - it doesn't require >> >> taking a >> >> leap into types as terms that will be really jolting to most >> >> programmers. >> >> >> >> The second is probably just my ignorance, but it's not always bad to >> >> worry >> >> about how what you don't know will bite you. :-) The issue is this: in >> >> BitC, >> >> types define the shapes of data structures even as they describe the >> >> nature >> >> of the inhabiting values. I don't know how that relationship really >> >> works in >> >> dependent type systems. It seems obvious to me that a language with >> >> dependent types must ultimately arrive at shapes for all of the values >> >> it >> >> manipulates, but I'm ignorantly nervous about that part. >> >> >> >> The third issue is that I have no personal experience with dependent >> >> type. >> >> While designing a language to support them actually is a really good >> >> way to >> >> learn them, I'm not so sure that learning language should then be >> >> published. >> >> :-) >> >> >> >> 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. >> > >> > Assuming you mean literals literally, I don't think they quite cover >> > the cases one wants. For example, if you have a static size array >> > type parameterized by a size, say Vec n a for n copies of type a, you >> > very quickly want to say Vec (n+1) a, and then after that you very >> > quickly want to say Vec (sqr n) a, and so. C++ has already gone >> > through a lot of evolution on this front, so it'd be good for bitc to >> > skip to the end. >> > >> > The worst thing that C++ got wrong initially was using a different >> > syntax for compile time metaprogramming and runtime programming, so >> > that we ended up with Vec (mpl::sqr<n>::value) a. If (1) bitc does >> > not allow Vec (sqr n) a, and (2) there is *any* way to do >> > mpl::sqr<n>::value, people will start to do it, and you live in syntax >> > hell for the rest of the lifetime of the language. >> > >> > C++ has now solved this to some extent with constexpr, but a constexpr >> > can't return a tuple. This means that if you want Vec n0 (Vec n1 a), >> > and you want the same code to split out both n0 and n1, there's no >> > clean way to do it. Bitc could conceivably solve this if you had >> > something like constexpr for all purely functional code, but I suspect >> > you are (somewhat justifiably) afraid of going this far (though I >> > would love it if you did :)). I don't think it is particularly >> > difficult to implement: all it requires is knowing which code is >> > functional and which isn't, and being able to run an interpreter for >> > the functional part at compile time. Certainly it has been done >> > before (tik-c does a lot more, for instance). >> >> Self-correction: C++11 constexprs can return tuples and other structs, >> but the structs they return must be declared completely separately >> from the normal structs (which I only just now learned): >> >> http://en.cppreference.com/w/cpp/concept/LiteralType >> > > I don't understand what you mean by "completely separately from the normal > structs" but > 1) structs (as known in C) are literal types > 2) literal types are normal types, just like any other types, and can be > (and often) used to define traditional runtime values > 3) constexpr functions are be called for both compile time and runtime > computations > 4) classes that are literal types need at least one constexpr > constructor, but are normal classes in every other aspect > > Note that C++14 relaxed many of the C++11 syntactic restrictions. > >> I don't really know the reason for this separation, unless it was to >> satisfy FUD. The compiler already has to check that constexprs >> satisfy constraints, so you could just as easily let normal functions >> be used as constexprs as long as they satisfy those same constraints >> without forcing the user to annotate. > > > constant expression functions as I originally designed them did not require > a keyword, and very much used the fact that the compiler already has what it > needed. A keyword was demanded by implementors, for various reasons - > including the fact that there are far more variations in C++ implementation > strategies than meet the eyes. One thing that convinced me was concerns > over early diagnostics.
Thanks for the clarifications! I happily withdraw several of my concerns, especially now that I see that std::tuple is littered with constexpr. It's too bad the keyword is necessary, but very nice that the standard library has it in the appropriate places. Geoffrey >> > In terms of your worry about shapes, the issue with dependent typing >> > is that there is no "now compile time is done" point in a fully >> > dependent typed language where you know what n is in Vec n a. That >> > is, there is no hard striation between compile time and runtime. >> > There is a hard striation between type checking and running, but type >> > checking does not tell you what n is, just that whatever it is at >> > runtime will be safe. I think a compile vs. runtime striation is >> > reasonable for bitc, and don't think it is particularly hard to >> > implement. >> > >> > Geoffrey >> _______________________________________________ >> bitc-dev mailing list >> [email protected] >> http://www.coyotos.org/mailman/listinfo/bitc-dev > > > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev > _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
