7 ms·
A PL theorist would note that most of the time when people talk about ‘types’, that they really mean ‘classes’, and that all of those things your mentioned woul
by noblethrasher 10y ago
A PL theorist would note that most of the time when people talk about ‘types’, that they really mean ‘classes’, and that all of those things your mentioned would be considered to be the latter. Types are rather the elements of your program that correspond directly to logical propositions (which your program proves to be true).
- kazinator 10y agoIn software engineering, programs are usually not constructed to prove anything; this claim is just the consequence of an equivalence between logic and static typing (Curry-Howard). Programming languages do not make very good logic systems in spite of the isomorphism. They are not designed to be expressive that way. The logic system exhibited by the type system is geared toward proving trivialities about the program: mainly that its run-time translation won't misuse data. Plus it supports certain devices like polymporphism and pattern matching and whatnot. Now instead of writing a useful program, we can exploit the type system for doing logic in a separate domain, detached from the program. The proof occurs as a byproduct when we compile the program. Somehow we encode, for instance, the "all men are mortal; Socrates is a man; therefore Socrates is mortal" argument into types and write the corresponding code. Then when the code compiles, it verifies: yes, the argument is valid. At that point, we throw the program away. What (if anything) that program does is irrelevant; its types have proven the modus ponens as it passed through the compiler, thus quod erat demonstrandum. That is supposedly what type is all about in a very narrow, myopic branch of computer science.