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 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). 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. > I suppose that makes me a constructivist :-) > > Naw. Pretty sure that's not what it means. > http://en.wikipedia.org/wiki/Constructivism_%28mathematics%29 Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
