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.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
