On Thu, Apr 2, 2015 at 5:32 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Thu, Apr 2, 2015 at 7:15 AM, Matt Oliveri <[email protected]> wrote: >> *Sigh* >> I wonder how Shap will feel about this tangent. This really has >> nothing to do with BitC anymore. >> >> Really, "Why is it not a type?" is an odd question. When you learned >> to count, did you think numbers were types? Why should the natural >> numbers be types? > > Well, I'd sort of like this to move to a different subject heading damned > fast so that we can find the discussion later, but the discussion itself is > no problem.
Done. > As I've already mentioned, BitC is going to adopt a Nat kind. One reason we > want natural numbers to be able to be interpreted as types is that it gives > us more sensible constructions for array and vector types that allow us to > check and elide bounds checks for many implementations of library-level > collection types. Saying elements of the Nat kind can be used in types is not the same thing as saying they _are_ types. Types are things such that we can ask whether something is an element of a type. We do not want to care about elements of 4, for example, so 4 shouldn't be a type. We should be able to use 4 as an argument to a type constructor though, so it is type-level. "Type-level" and "type" are different! In most dependent type systems, anything can be used as an argument to a type constructor, so the term "type-level" is misleading and vacuous. But still, not everything is a type. 4 is not a type in any dependent type system I've seen. You can't talk about elements of 4. > And anybody who has looked at the performance of Java or C# collections will > understand that eliminating those bounds checks actually matters! To real > systems programmers, even. I'm all for Nat kinds and even fancier things to avoid bounds checks. One of the motivating philosophies of my project is that you should be able to avoid any dynamic check that you provably statically know will succeed. It may not be worthwhile to actually eliminate all unnecessary checks, but the machinery needed to be _able_ to eliminate all of them them versus to actually eliminate the expensive ones seems to be the same. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
