What are strings: objects or types?

Once upon a time, there were two mathematicians named Haskell Curry and William Alvin Howard. They invented the proposition that types are really propositions and values are really proofs. That means, e.g. in Ada, propositions like:

type Integer

are really the logical proposition

There exists an integer,

and strong typing like

42 : Integer

are really lemmas along the lines of 

Theorem. There exists an integer.

Proof. 42. ∎

And the dependent types like 

subtype Small_Int is Integer range 1 .. 10

are really the logical proposition along the lines of

There exists an integer x such that 0 ≤ x ≤ 255

and strong typing like

42 : Small_Int

are really lemmas along the lines of 

Theorem. 42 is a Small_Int.

Proof. 42. See that 0 ≤ 42 and that 42 ≤ 255. ∎

Now what are strings, such as "42", in relation to type theory? They are not values, but rather specific facts, and as such are the singleton type. That means the string

"42"

is really the declaration

The value is exactly the string "42",

and these follow the singleton design pattern, which is object-oriented programming. They really shouldn't be represented as types, because that's lazy thinking.