On Thu, Apr 2, 2015 at 10:34 PM, Matt Oliveri <[email protected]> wrote: > On Thu, Apr 2, 2015 at 5:32 PM, Jonathan S. Shapiro <[email protected]> wrote: >> 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.
This thread got sidetracked by an unfruitful argument between Keean and me. Does everyone aside from Keean agree that "type-level" and "type" are different, and that Nats and Bools are only type-level? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
