On Fri, Apr 3, 2015 at 8:29 PM Matt Oliveri <[email protected]> wrote:
> 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? > Yes. In my luddite set theory intuition: "type-level" is a fancy sounding synonym for compile time, and "type" is a compile time set of values. A specific boolean or natural is not a set of values, except in some pedantic set-theory-bootstrapping sense which doesn't matter.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
