I don't think you really wrote anything I did not acknowledge. Yes, types are a form of complete test over the shape/type of data that they encode. If you can encode your data with the correct type, it will go a long way to making sure you don't have errors in the types.
However, I take issue with this statement: "For statically typed languages, the type check is a type of test that just so happens to be very succinct and easier to write than it is to skip. " For the simple cases, I agree with this. But when you see the type gymnastics that some programs go through to guarantee some traits, it is hard to agree with any claim of "easier to write." Consider a "true" quicksort in haskel[1].
My assertion was that the "hard part" of programming is often in the logic, not necessarily the shape/type of the data. When you see attempts at getting the logic of a program into the type system, things start to take a turn for the worse. Really worse when you find you have many types that all encode the same type of data. (Consider the metric system debate.)
My point about "having the right tests" is that sometimes you only care/have the knowledge to think about/whatever certain scenarios that are either likely or guaranteed to happen. Pushing everything in the type system implies that you had the energy to think of and consider everything. My assertion is often you don't have that time/energy.
So, sure, you will have the "right tests" in that scenario to an extent, since you will have all tests. However, I wonder if most programs couldn't work out with a much smaller subset of those tests.
A direct analogy for the point I am making is physics. Classical/Newtonian physics break down and don't work at a level. Worse, they rely on a lot of simplifications and actually describe what is happening moreso than how/why. Yet, for a large portion of calculations that people will do, they work. I grant that encoding all of the assumptions into the calculations will make them more accurate, but often you don't need that level of accuracy. And they definitely make them harder to understand.
The true quicksort example you linked has very little to do with Haskell's type system and everything to do with purity. The qsort version at the bottom of that page is also pretty close to the version used in any mutable language, just with a bit more noise in the syntax. A direct translation to Python might make the syntax easier to understand, though it should be stated that this is not supposed to be pretty Python code---it's literally just a syntactic swap.
def lscan(ary, p, h, i):
if (i < h):
if (p < ary[i]):
i
else:
lscan(ary, p, h, i+1)
else:
return i
def rscan(ary, p, l, i):
if (l < i):
if (ary[i] < p):
i
else:
rscan(ary, p, h, i-1)
else:
return i
def swap(ary, i, j):
ary[i], ary[j] = ary[j], ary[i]
def sloop(ary, p, l, h):
if (l < h):
l1 = lscan(ary, p, h, l)
h1 = rscan(ary, p, l1, h)
if (l1 < h1):
swap(ary, l1, h1)
sloop(ary, p, l1, h1)
else:
return l1
def myqsort(ary, lo, hi):
if (lo < hi):
piv = a[hi]
i = sloop piv lo hi
swap i hi
myqsort(ary, lo, i-1)
myqsort(ary, i+1, hi)
My point is pretty much about the "a bit more noise in the syntax." And qsort will only work on array types, something that is typically shunned by people trying to "do all of the work with the type system." Consider the types for "NonEmptyList" and such.
Is it neat when these work? Certainly. Do I think they pay obvious dividends in the effort increase? Not so much. I am open to the argument, but I have yet to see anything compelling. And with so much traction in other areas, I am doubtful that it is anything close to the silver bullet that advocates make it out to be.
Again, that noise is entirely an artifact of purity and syntactic choices, not the types.
I'm not sure exactly what you're arguing for here, but I can explain a use case of NEL—when you consume it you don't have to check the for emptiness. That means that you can eliminate an entire branch of code, either locally or in exception catching, or an entire failure mode.
Frequently people just throw those checks in and then assume, trusting their own eye or documentation to minimize the emptiness checking, but without expressing that into the type the compiler won't be able to help you not repeat that check. It's optimal to check it exactly once and people are liable to check it either 0 or many times.
My argument is that as you get more types that cover states or behavior of your program, one typically finds more code.
Is there an argument that these are beneficial? Of course there is. I just have not been privy to an example where it carried its weight.
Take the not-empty list. Typically the "cost of checking for empty" is so negligible that to push that thinking into the compiler just doesn't lead to any gains. Not even just marginal gains. It is nigh unmeasurable.
Compound this with similar types over the state of any other object, and you have an explosion of types that becomes unwieldy. Account, NotEmptyAccount, OverdrawnAccount, DrawingInterestAccount... It gets to be just crazy. Especially in areas where you don't care about any of those details, but now have to account for an inheritance tree.
And then you get into the fun of having to logic not just about how the actual program works, but how the interaction of various types works.
So, you keep saying the syntax I was referring to was due to purity. Which is kind of the point. These languages use syntax and types to help ensure purity. Which makes them more to handle for some algorithms. Less for others. And then just hard to really know the true computational cost for a lot.
Which is all to say that it is a design tradeoff. And should be undertaken as an informed decision. Not a "let the type system do the work" kind of one. More of one that "this is so important we need to make sure we can afford the cost of pushing it into the type system." Or, if you would prefer "this particular instance is so cheap to push to the type system, we should do so."
I agree completely that it's a tradeoff. I also only bring up purity to suggest that other strongly typed, impure languages could solve this with less trouble.
NEL is a particularly interesting point of compromise. I don't think it carries its weight very frequently at all, though I have used it very effectively in a few cases. I also think the burden of type hierarchies as you're describing isn't much felt in Haskell. You typically don't build large taxonomies, or taxonomies at all, in a language without subtyping.
The only place where I see taxonomies forming at all is in `lens` and there they are used to great effect.
Apologies for not seeing this. I really need to get better at following HN threads. (Or not, depending on your take.)
I think we are mostly in agreement. I just have not had the fortune to work in an area where these have panned out that well. Hopefully I get a chance to change that someday. (Though, I am currently under the song of the lisp sirens.)
However, I take issue with this statement: "For statically typed languages, the type check is a type of test that just so happens to be very succinct and easier to write than it is to skip. " For the simple cases, I agree with this. But when you see the type gymnastics that some programs go through to guarantee some traits, it is hard to agree with any claim of "easier to write." Consider a "true" quicksort in haskel[1].
My assertion was that the "hard part" of programming is often in the logic, not necessarily the shape/type of the data. When you see attempts at getting the logic of a program into the type system, things start to take a turn for the worse. Really worse when you find you have many types that all encode the same type of data. (Consider the metric system debate.)
My point about "having the right tests" is that sometimes you only care/have the knowledge to think about/whatever certain scenarios that are either likely or guaranteed to happen. Pushing everything in the type system implies that you had the energy to think of and consider everything. My assertion is often you don't have that time/energy.
So, sure, you will have the "right tests" in that scenario to an extent, since you will have all tests. However, I wonder if most programs couldn't work out with a much smaller subset of those tests.
A direct analogy for the point I am making is physics. Classical/Newtonian physics break down and don't work at a level. Worse, they rely on a lot of simplifications and actually describe what is happening moreso than how/why. Yet, for a large portion of calculations that people will do, they work. I grant that encoding all of the assumptions into the calculations will make them more accurate, but often you don't need that level of accuracy. And they definitely make them harder to understand.
[1] http://www.haskell.org/haskellwiki/Introduction/Direct_Trans...