# Natural numbers as types.

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.

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

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.

-
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 '13 at 13:30