Tell me more ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.
up vote 0 down vote favorite

My question could be simple but I haven't found an answer for it: could we define a type theory where the types are the natural numbers themselves (not the set of the natural numbers)?

Thanks.

share|improve this question
what exactly do you mean by type theory? – Ittay Weiss Jan 7 at 10:56
I mean an Intuitionistic type theory or constructive type theory. – Gibarian Jan 7 at 11:02
Do you mean something like the theory of simple types (TST)? – Zhen Lin Jan 7 at 11:26
Ah, yes, thanks. I hadn't any idea about it. – Gibarian Jan 7 at 11:53

1 Answer

up vote 0 down vote

Most type system will have 1 or True the type with a single unique in habitant.

And they will have disjunction types so you can define Bool or 2 = 1 + 1. which has two inhabitants..

In general you can have any sum 1 + 1 + 1 + 1 as a type and use 4 as a shorthand for it.

Therefore the natural numbers are already types in most systems.

share|improve this answer
A 0-tuple or record with no fields, i.e. an empty product type, are also common ways to describe the unit type. And of course an uninhabited type is 0. – camccann Jan 7 at 13:30

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.