I love Bob Harper's view that something like Type Theory will eventually become the one-true-language. His arguments arise from a POV pretty different from the standard argument here—it's not that some particular implementation will win, but instead that the entire design space of languages we will eventually gravitate to type theory because it's just right.
I think type theory is supremely interesting, and I'm curious to see how far you can take it. I worry a little that at some point your type system needs its own type system, and then we've just moved the argument about typing one level of abstraction deeper.
I'm not willing to concede that strong static typing is a universal truth though. Too many people much smarter than me seem to disagree.
At the end of the day who wants dependently typed bash?
It's a great intellectual position for happy hour at the campus pub. Yet from a practical standpoint, it's hard to see how programming languages requiring more attention to type system will facilitate banging out code for ordinary problems more quickly.
There are times when it is really important to be able to prove code is correct and times when it is enough to just provide a plausible answer. The market for ML on Rails remains without validation.
With something like Haskell (very good type inference) the types will only bother you if you're writing wrong code (or writing particularly complex expressions, I'm not necessarily against compilers complaining about things that are complicated).
The Haskell compiler will complain if I am writing wrong Haskell code, or more generally when the types are indeterminate and can't be inferred.
This not the same as 'wrong code' in the abstract. The code will run fine if I don't pass in mismatched data, or more generally bad data. And if I am passing in bad data, static typing doesn't give me good answers, it just keeps the program from crashing. Don't get me wrong, there are times when crashing is bad. But there are times when the cost of a runtime error is nominal and the value of flexible code is high.
Static typing trades one type of cognitive overhead for another. The Java program of 500 classes is its manifestation.
What is the cognitive overhead Haskell is introducing? Types? Because as far as I can tell we use types in all OOP, they're just implicit and not checked.
Static type checking, regardless of language, requires thinking about programs in a particular way because one possible mode of failure is prioritized over all other modes. It does so regardless of whether absolute type safety deserves to be prioritized given the purpose of a particular program and it does so regardless of whether absolute type safety is an appropriate concern at a particular stage of the program's development.
Static typing can make "how do I get this to compile?" a design criterion Consider year 2038 problem. In MySQL, various date types are coerced to the timestamp type by design. Otherwise the program would not compile. Compilation takes precedence over problem solving.
I've personally found that static typing is an aid to comprehension and thought. I spend more time fiddling with untyped code than typed code. I also disagree that static typing prioritizes a particular mode of failure—the notion of failing to typecheck is a rather general one.
There are two contexts in which one can think about data types. The first choosing among or constructing data types as abstractions. The data type as metaphor is useful regardless of language. An important property of this context is it's not just useful externally via an automobile class in a used car lot application but internally with ports and pipes for I/O and threads and locks and semaphores for processes and so on.
But the other context in which we select and choose and construct data types is because a language insists upon it. Here our choices are not based on how to best represent the world, but by how to package our metaphor into a pre-existing schema. The very first time we compile our code, we have been forced by the compiler to crystallize our code based on an early guess.
When a flat roofed building uses scuppers to provide emergency overflow drainage, it is good if water passing through them makes a mess of the plantings below and perhaps stains the facade. It indicates that the primary drains are clogged before the roof collapses. Likewise, runtime type errors might be preferable to zeros silently inserted into a database.
Static and dynamic typing each catch some types of errors at runtime at the expense of masking other types of errors at runtime.
I think runtime errors are a fine way of detecting such failings. I don't understand why typing is at odds with that.
I think types make us write out the why next to the what. That why might be a domain model justification, or something much more trivial. It's also completely possible to encode an untyped regime in a type system. You're always crystallizing your design, you just can either provide good information to understand its failings and be more prepared to fix them. Or not and chase logic errors throughout an undocumented, dynamic system.
The holy grail of type theory is to write propositions as types and have proofs fall out of those propositions naturally. Those proofs comprise your program. So-called dynamic typing throws that all out the window and just says "I'll permit any program you want to write and bail out at the first opportunity". It's a proposition that is trivially true and thus it's not useful at all.
Who says it has to feel much at all like DTLs of today? I probably do want to be at least warned when the compiler can't be sure my bash is terminating.
And I'd love Bash embedded in a DT. Even if I never write the DT components being able to nicely map Bash -> DT is powerful.
Pretty much every program humanity has produced is grossly defective. Certainly there's nothing I use heavily that hasn't failed. IMHO shipping more garbage more quickly is not a problem worth solving.
