> And this post shows how you can do that in Haskell.
the actual critique of the first post wasn't really that Haskell can't do it in a literal sense, but that ignoring or reasoning about unknowns diminishes the advantages of static typing.
Sure, you can define an "unknown" type if you want and make your static language as permissive as possible, but then you lose the actual static guarantees, which is automating reasoning about the correctness and capacities of your program at compile time.
The question then is if you're already conceding that there are so many unknowns which better ought to be dealt with at runtime, what is there to be gained from making that explicit in your program other than just having to write more code?
> ignoring or reasoning about unknowns diminishes the advantages of static typing.
Ignoring the unknowns that are unnecessary to solve the problem at hand, is literally the essence of software abstraction. Why would you want to do more work than is necessary to solve a given problem?
> you can define an "unknown" type if you want and make your static language as permissive as possible
And 'unknown' type doesn't make the language permissive. Since the type is 'unknown' it doesn't permit any operations at at all on it. Hence, the opposite of permissive.
> you lose the actual static guarantees, which is automating reasoning about the correctness and capacities of your program at compile time.
You absolutely don't lose the actual static guarantees which are actually relevant to solving the problem your program wants to solve. If your program's job is to add a signature field to a JSON object, why would you want to parse and decode the entire JSON object into a strongly-typed value? You would just parse it into a reasonable Map data structure and add the signature as a key-value pair to the Map.
> you're already conceding that there are so many unknowns which better ought to be dealt with at runtime
That's exactly what we're not doing here, we're creating software abstractions which again, is an essential part of software development. Please see Liskov & Zilles, 'Programming with Abstract Data Types', 1974.
> what is there to be gained from making that explicit in your program
What you always gain from static typing–exposing the assumptions and invariants of your code as first-class parts of the code, making it easy for readers to understand at a glance what they are, making it easy to change the code with compiler assistance to ensure the invariants are honoured.
>What you always gain from static typing–exposing the assumptions and invariants of your code as first-class parts of the code, making it easy for readers to understand at a glance what they are
This is essentially what I was getting it. To me the static typing seems to be almost more about naming things that it is about verifying the correctness of your program in the face of unknown or interesting behaviour.
And there is a very obvious cost to this because not all code is 'your code'. That's the problem with a coupling that is mentioned in the first part of the article but not really addressed. With typing, it is very easily possible for someone to create bad abstractions that you have no control over, you simply inherit them. It breaks with the principle of leaving interpretation to the receiver of data who encapsulates it.
And this is a very practical problem in real static code, because people create bad abstractions all the time, so the type system rather than just making valuable claims about what we know produces all sort of entanglements you have no control over.
Here is where the dynamic and static typing distinction crosses over into the OO debate. Alan Kay pointed out that the 'late-binding of all things' is one of the key principles of object oriented programming. Static typing interferes with this in very strong ways by allowing developers to impose meaning on your program way too early.
> To me the static typing seems to be almost more about naming things that it is about verifying the correctness of your program in the face of unknown or interesting behaviour.
That's exactly backwards. The point is not naming things, the point is encoding behaviours and invariants in the type system so the compiler can help you check them.
> With typing, it is very easily possible for someone to create bad abstractions that you have no control over
It's possible for programs to be written badly in any typing discipline, static or dynamic. Neither saves you from the bad decisions of others. I've personally seen PHP code that no one could understand and everyone was afraid of touching because it heavily used reflection. I've heard of this for Ruby and Objective-C code too.
the actual critique of the first post wasn't really that Haskell can't do it in a literal sense, but that ignoring or reasoning about unknowns diminishes the advantages of static typing.
Sure, you can define an "unknown" type if you want and make your static language as permissive as possible, but then you lose the actual static guarantees, which is automating reasoning about the correctness and capacities of your program at compile time.
The question then is if you're already conceding that there are so many unknowns which better ought to be dealt with at runtime, what is there to be gained from making that explicit in your program other than just having to write more code?