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: > > On 2 April 2015 at 14:57, Matt Oliveri <[email protected]> wrote: > >> On Thu, Apr 2, 2015 at 9:50 AM, Keean Schupke <[email protected]> wrote: > >> > On 2 April 2015 at 14:25, Matt Oliveri <[email protected]> wrote: > >> >> You seem to be under the hilarious misimpression that everything in > >> >> MLTT is a type. It ain't so! Ask any proof assistant: "fun (x : 4) => > >> >> x" is nonsense. > >> > > >> > There is nothing fundamentally wrong with that statement, I could > write; > >> > > >> > fun (x : succ (succ (succ (succ zero)))) => x > >> > > >> > So I could allow "4" so be a shorthand for succ (succ (succ (succ > >> > zero))) > >> > and then hide the succ/zero types inside a module. > >> > >> No no no. 4 _is_ a shorthand for that. (Modulo constructor names.) > >> (succ (succ (succ (succ zero)))) isn't a type. > > > > 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. If mathematics is founded on type-theory, and everything in mathematics can be constructed from it, then of course numbers are types. I suppose that makes me a constructivist :-) Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
