> Types are there whether you want them to be or not<p>But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system.<p>There is also a minor thing that came to my mind. Types are most often associated with intuitionist logics, which are about constructive provability, as opposed to classical logics, which are about "truthyness" so the title of the post is a bit misleading :)
If you were building a sandcastle, a type system is like plastic forms in the shape of castle components (walls, towers, etc)... They help you create a better sandcastle...<p>This article was essentially saying: "You can remove the forms when you are done and your sandcastle will still stand."
Yes, type erasure is neat and a bit of thinking will make it obvious why proving static properties does not require run time checks if the transformations you perform on your program preserve those static properties. I disagree with the author's claim though that types are everywhere. Types in fact are extra structure that is hoisted onto programs. At the end of the day the machine knows nothing about the types and will shuttle bytes back and forth all day long. Furthermore, types restrict the universe of computation and there are examples of programs that are not well-typed but don't go wrong when evaluated.
Some food for thought from Rich Hickey:
"Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system."
<a href="http://www.reddit.com/r/programming/comments/lirke/simple_made_easy_by_rich_hickey_video/c2u1fgc" rel="nofollow">http://www.reddit.com/r/programming/comments/lirke/simple_ma...</a>
Isn't type erasure just a rather limited subclass of compiler optimization, and as such comes "for free" without having to explicitly code for it? The compiler frontend can leave in all type checks, having most of them can be removed by the optimizer, the same way you can remove any sort of redundant check (a default case in a switch statement over an enumeration, etc, etc)<p>That being said, general type erasure can have (massive) problems. Look at Java.
Personally, I wish that type systems allowed for arbitrary pure (as in "same input -> same output") code to define what is and isn't a valid instance of a type at compile time.<p>Being able to declare a function that is only valid for, say, power of two inputs (say: a hashmap's initial size, when the hashmap is using a bitwise and for wrapping) and having it actually enforced at compile time would be very useful.<p>I mean, even range types are useful.
The site is eerily similar to <a href="http://www.jonmsterling.com/index.html" rel="nofollow">http://www.jonmsterling.com/index.html</a><p>You two could hit it off or something.
"Whether your programming language "embraces" types or has a modern type system or not, these concepts are central to how programs execute, because they are a fundamental part of how computation works." - what are "modern" type systems?<p>Was something new invented in the last 15-20 years that I had missed?
The discussion of types here is all over the place. This is because they are handled so differently in various programming languages. Pascal included array bounds in the type annotation for arrays and subscripting was enforced (at runtime) to be withing bounds. In C (and C++) arrays are almost equivalent to pointers (the full answer is complicated see [1]) and there is a real danger of buffer overflows. Python doesn't include type annotations, but the run-time enforces strong typing, lists carry their type information and will throw an exception if subjected to a non-list operation. The type system in Haskell is perhaps the best example of a really expressive and really effective system for ensuring that the compiler can catch as many error as possible at compile time.<p>Haskell programmers sometimes say that if a program compiles it almost always works. This is interesting, but unfortunately, types and type annotations in use today don't fully capture the formal specification needed to guarantee program correctness.<p>Just writing down specification in preparation for a proof of correctness can be difficult. The specifications have to be expressed in a formal system, for example some form of mathematical logic like predicate calculus. Working with anything less than a formal specification is like trying to solve a mathematical set of equations without using math symbols. Natural language is just inadequate to the task. See [2].<p>Getting the specifications right isn't easy. I remember my first attempt at proving the correctness of a sorting program. I understood that I needed to insure that A[i] <= A[i+1] for all elements in the array, but I forgot that the final result had to include all and only the original elements (i.e. that it had to be a strict permutation of the input elements). I don't believe that type systems are currently useful for these kind of specifications and verifications of program correctness.<p>Real programs interact with the outside world (e.g. GUI's are hard to describe mathematically). Real programs often have distributed or concurrent execution for which new logics (like Temporal Logic) may have to be employed. Proving that a program will terminate or make progress or not deadlock or not livelock or will meet some real-time constraints are all exceptionally hard.<p>Many years ago (in the 1980's) I worked on this research area at University. I had the hope that eventually, programming would be more like an interactive exploration with a sophisticated program prover. I thought that the programmer and software-prover would work together to produce a correct program. Today, we are still programming in pretty much the same old ways as back then. The languages are much better, but it's a harder problem than I thought it was going to be.<p>[1] <a href="http://stackoverflow.com/questions/3959705/arrays-are-pointers" rel="nofollow">http://stackoverflow.com/questions/3959705/arrays-are-pointe...</a>
[2] <a href="https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD667.html" rel="nofollow">https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/E...</a>