[kazinator]

But what it's reasoning about coincides with the dynamic type which will exist at run time, so that means we cannot say the two have nothing to do with each other. It's the same knowledge, just known at different times, right?

Just because we have stuffed some knowledge into tags that exist at run time (and chosen suitable machine representations to make that possible) doesn't mean it's a different class of knowledge.

[chongli]

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

[kazinator]

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.

[chongli]

There can be propositions about that text.

Yes, however, those propositions are not types.

[kazinator]

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"?

[chongli]

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.

[kazinator]

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.