[Solved]: Are numbers types and what is "Number"?

Problem Detail: 

I was pondering about what are the numbers. It seems like a number is data type. I mean, like Maybe in Haskell. Because, for instance, one on its own means nothing for me. However, one apple tells me about how many apples does one talking about. Thus, numbers are quite abstract. If somebody asks you "how is it going" you can't answer "10". 10 what? But you could say 10 out of 10. But this is another abstraction. So, what I want to say is that a number is an abstraction. It can only be used to quantify other things. Thus, very often people say that "Number" is a type or set or category, etc. But then if a concrete number is an abstraction what is Number?

I hope you've got my idea and question and sorry if I used some terms incorrectly. I'm trying to study CS on my own and do make lots of mistakes.

Asked By : Ivan Demchenko

Answered By : jmite

So, you have to be very careful to distinguish values, and the types of those values.

We say $v : T$ when $v$ is a value with type $T$.

The type Number

When people say "Number" is a type, usually they're referring to the type of natural numbers. But each number isn't a type, it's a value, and $Number$ is their type. So we can say $1 : Number$, $2 : Number$, etc.

Notation isn't always consistent. Sometimes people will refer to $Number$ as a type class that contains $Nat, Int, Float$ etc. But that's more complicated.

Now, as for each number being a type, in a language like Haskell (or any Hindley-Milner lanugage), this isn't the case, because numbers are values, and types and values are separate.

But there are a few ways we can look at this

Numbers as singletons

But using dependent-types or GADTs, in a Haskell, Agda, Idris, or other languages with advanced types, you can form a type like this (using Agda-like pseudocode):

data TypeNat : Nat -> Set where    TZero : TypeNat Zero   TSucc : {n : Nat} -> TypeNat n -> TypeNat (Succ n) 

For any number n, TypeNat n is a type, containing exactly one value, the TypeNat representation of n.

So here, the number isn't the type, but there's a 1:1 correspondence between the numbers and the types.

Numbers to Quantify other things

We can use numbers to quantify things, but in a dependent-type system, usually this is done by indexing types.

So you can have a type like Vec a n, which is the type of Vectors containing exactly n elements of type a. So here, our types are indexed by numbers, but the number itself is not a type.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/62352

 Ask a Question

 Download Related Notes/Documents