Hacker News new | ask | show | jobs
by chongli 4270 days ago
Types are propositions for which the text of your program is the proof. Type theory arose as an alternative to set theory in order to deal with Russell's paradox[0]. Types have been around for a lot longer than computers have. They have nothing at all to do with a running program.

[0] https://en.wikipedia.org/wiki/Russell%27s_paradox
1 comments
kazinator 4270 days ago
What is missing from the above articulation of a view is that the run-time state of the program is also text. (It's made up of the symbols "0" and "1", at one level.) There can be propositions about that text.
link
chongli 4269 days ago
There can be propositions about that text.

Yes, however, those propositions are not types.

link
kazinator 4269 days ago
Even those propositions, which are like, for example Ɐx: x -> x? (For all x, function from x to x)?

Who decides these things? Some "world type authority"?

link
chongli 4269 days ago
Such a proposition pertains to a mathematical function. A running computer program does not contain mathematical functions, merely representations of them.

It is akin the difference between the theory of gravity and a falling rock. You can describe the rock with all manner of equations but you will not find any equations inside the rock.

link
kazinator 4269 days ago
I think I almost understand your position now.

A running computer program does not contain mathematical functions, merely represenations of them.

A printed computer program text does contain mathematical functions, and not merely representations of them.

Because of this difference, logical propositions about structures in the program text are types, whereas those about structures in the running program are not.

Furthermore, this has something to do with gravity and rocks: the running program is analogous to a falling rock, but the non-running program is like ... something else.

Somehow, compilers are exempt: they are running programs, which work with types. The source of this exemption is that they operate on other programs; a proposition inside a compiler is a representation about the program being compiled, not about anything in the compiler. Running programs may not entertain propositions about their own typing, because typing is purely prior to run-time. Type does not exist at run-time, period. The propositions of run-time typing are not type, but some kind system of data representations that mimics type.

link