On Thu, Apr 2, 2015 at 11:09 AM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 15:57, Matt Oliveri <[email protected]> wrote: >> >> > If mathematics is founded on type-theory, and everything in mathematics >> > can >> > be constructed from it, then of course numbers are types. >> >> If you insist on thinking of everything as a type, you're not going to >> get into any contradictions, but the fact remains that most languages >> do not consider everything to be a type, so you won't get much use out >> of your point of view. >> >> You still have not provided any reason why BitC should allow True and >> False (the elements of the Bool kind, and the y and n for arrows) to >> be used as types. > > They are types, but they can't be used as _Types. > > because instead of: > > (->) : * -> * -> * > > we have: > > (->) : _Bool -> _Type -> _Type -> _Type
OK, so they're not types in any useful sense. > Where _Type (a universe 1 type) contains (universe 0 types: Int, Float, > etc...). > > and _Bool (a universe 1 type) contains (universe 0 types: True, False). I think you're still using the term "universe" wrong. A universe is a type whose elements are types. (If you think of everything as a type, then everything is also a universe. How silly.) So _Type is a universe, for example. If _Type contains Int, then Int's universe is _Type. But you are referring to "universe 1" and "universe 0". Why? What is their role? > You would not infer True or False from any values, and if the user did > explicitly use them: > > type X = True > > The are just creating an alias. Because True and False cannot be the domain of a function, (from the kind of (->)) why should we treat them as types in this way? I don't mind you privately thinking of everything as a type, but please don't let that be a reason to recommend useless quirks like this. >> > I suppose that makes me a constructivist :-) >> >> Naw. Pretty sure that's not what it means. > > http://en.wikipedia.org/wiki/Constructivism_%28mathematics%29 Being a constructivist isn't about preferring constructions of concepts (e.g. starting from MLTT) to axiomatizations. It's about requiring a construction of something to prove that it exists, as the article says. We haven't talked about existence at all, so whether you're a constructivist or not would not be evident from anything you've said so far. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
