On Wed, Jul 2, 2014 at 12:19 PM, Geoffrey Irving <[email protected]> wrote:
> > 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. > Understood. But note that "'a[n+1]" can be expressed as a type-level construction "'a[S(n)]", where by S, I mean "successor", and "n" is required to have Nat kind. We can then introduce the '+' sugar as needed using kind classes as in Habit. I'm not even worried about Sqr, except to the extent that computing this crap in the type system raises some unfortunate compile speed issues, and the type inference engine is already being pushed really hard. > The worst thing that C++ got wrong initially was using a different > syntax for compile time metaprogramming and runtime programming... Syntactically that would have been very hard to resolve. I've played with it both ways at various points in BitC. It's *very* tricky. Though I have to say that the competition for "worst thing C++ got wrong" seems to be ruthless, vicious, and on-going. :-) > C++ has now solved this to some extent with constexpr, but a constexpr > can't return a tuple. More generally, C++ lost something by not introducing a tuple type. Though if I only get to make one change to C++, I want it them to introduce a tagged union as an alternative to untagged unions. Because that would give us a migration path away from one of the big problems for automatic code conversion. > 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. > It's a bit more complicated than that if you add the requirement that type computation must terminate... > 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. > Yes. And *that* is why a fully dependent type system is not the right path for a systems programming language. Very nicely put, Geoffrey! Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
