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 ex...