4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I'm not really sure what you're asking, here, but it feels more like a question about linguistics than about computer science. Could you clarify what the CS content of the question is, please? (Grammatically, by the way, numbers are determiners.) $\endgroup$ – David Richerby Aug 6 '16 at 18:53
8
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you very much for your quick and detailed response! I've got your point. However, I'm wondering can we think about numbers as something abstract. For example, when we encode numbers using Church encoding, we say that 2 means f(f x). So, here we can see very concrete meaning of a number - how many times f was applied. When we say 2 smth we mean smth, smth. There's pattern: number + noun. Like Maybe a. a : Maybe doesn't make sense, whereas a : Maybe Book does. In the same vein a : One no sense, but a : One Book is a book. Of course One and Maybe are different things $\endgroup$ – Ivan Demchenko Aug 6 '16 at 18:03
  • $\begingroup$ You can attach meaning to a number, but the number itself isn't a type, it's a function. Church numerals have the type $\forall n \ldotp (n \to n) \to n \to n$. $\endgroup$ – jmite Aug 6 '16 at 18:33
  • $\begingroup$ Also, you're confusing values and types. Maybe is a type constructor: you apply it to a type, and it gives you a type back. Church numberals are values: you give them values, and they give you values back. In some systems, types and values are combined, so you could apply church-numerals to types, but they themselves are values (functions), not types. It just so happens that we write type application Maybe Int with the same notation as function application f x $\endgroup$ – jmite Aug 6 '16 at 18:36
  • $\begingroup$ Oh, I see! Your ideas make perfect sense for me. thanks a lot! $\endgroup$ – Ivan Demchenko Aug 6 '16 at 18:43
  • $\begingroup$ It's possible you could have type constructors like One a = a, Two a = (a, a), Three a = (a, a, a), etc. but in this case the numbers themselves aren't type constructors, it's just that you happened to use the name of them. $\endgroup$ – porglezomp Aug 6 '16 at 19:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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