On Wednesday, July 2, 2014, Geoffrey Irving <[email protected]> wrote: > On Wed, Jul 2, 2014 at 12:19 PM, Geoffrey Irving <[email protected] > <javascript:;>> wrote: > > On Wed, Jul 2, 2014 at 11:04 AM, Jonathan S. Shapiro <[email protected] > <javascript:;>> 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. > > 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] <javascript:;> > http://www.coyotos.org/mailman/listinfo/bitc-dev >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
