On Thu, Apr 2, 2015 at 10:27 AM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 15:15, Matt Oliveri <[email protected]> wrote: >> On Thu, Apr 2, 2015 at 9:58 AM, Keean Schupke <[email protected]> wrote: >> > Now, that seems unexpected. Why is it not a type? >> >> *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? >> >> The only thing I know of where natural numbers would be type-like, >> other than the encoding trick in Haskell, is set theory, where the >> number 4 is actually defined to be some set. (Usually {0,1,2,3}.) This >> is arguably another encoding trick. Most type theorists prefer for >> numbers to simply be numbers. >> >> If you're asking for the technical reason why 4 can't be used as a >> type in MLTT, it's simply that there's no way to derive the judgement >> that 4 is a type. > > So it can be a type.
In the sense that there are interpretations of MLTT in which it is, yes. > 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. > I suppose that makes me a constructivist :-) Naw. Pretty sure that's not what it means. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
