Believing that any technology has no cost is poor engineering IMO. There are costs to that rigidity, and they're rather self-evident.

No one is saying there is no cost. The cost of using static types is (1) you have to think about type info when writing the code and (2) you have to fix compile-time type errors while you are developing. The poster is claiming that, over time, as code bases tend to grow large, this small investment yields increasing (not diminishing) returns; a claim I would agree with.

If you believe there are no diminishing returns, I'm interested to hear your reply to the author's question about why we don't all use Agda or Idris.

Well, the easy answer is that dependently-typed languages like Agda and Idris aren't very mature yet. They're still missing many commonly-needed libraries, compile times are slow, the tooling isn't great, etc etc.

Getting a language to the point where it's workable for serious projects is a lot of work. Rust is getting there with the backing of Mozilla, Haskell has made some decent strides too (but still has a way to go, and I think has some pretty fundamental flaws entirely apart from the type system). It'll be probably another decade at least before we see any dependently-typed languages getting a serious foothold, but I do think they're going to become a lot more common eventually.

It isn't just a matter of tooling. There exist hard limits on how much can be inferred about unannotated programs, and when you go past those limits, the price you have to pay is to embed (partial) proofs of correctness in your own code. For example, think about why GADTs don't play nicely with type inference.

IMO, machine assistance is useful to the extent it relieves us humans from work. In particular, types are useful to the extent they can be inferred. Beyond that, you still need to prove the correctness of your programs on your own, so there is no point to the ceremony of writing down those proofs in a machine-checkable format.

> Well, the easy answer is that dependently-typed languages like Agda and Idris aren't very mature yet.

It's also self-evidently wrong. Agda was first released in 1999, ten years before Go. If you use a wallclock interpretation of "maturity", Agda is twice as old as Go and Idris is roughly as old as Go. Both are used significantly less (by several orders of magnitude), though. Despite them having a far stronger type-system.

If you, on the other hand, you are using a "developers' time" interpretation of maturity, on the other hand, you are making a circular argument, i.e. "Agda is seeing less use, because it has been used less", as resources invested in a language ecosystem tend to be strongly correlated with it's usage.

Have you used them? Switching to a language like Agda or Idris is entering the realm of formal verification because the types are so expressive. It's completely different to what most programmers are used to.

Essentially the types being used as so complex the type checker cannot automate the decision about two types being compatible so you have to write maths proofs to help. The types used in mainstream languages are simple enough that the type checker never needs help like that.

The cost of formal verification right now is immense but the benefit is close to bug free code. Mainstream strong statically languages require nowhere near the same amount of effort and give clear benefits over dynamic types.

Defining types is easy and enhances code readability until you go too far. Some type declarations in Haskell or highly templated C++ are hard to read.

While this is a valid point, it's also worth remembering that if you have a data structure of sufficient complexity that writing out its type is cumbersome, then your data is still in that structure whether you choose to be explicit about it or not. Any code reading or modifying some element within that data still needs to correctly find that element, and if writing out the types is a burden then probably finding the correct location every time is also difficult. So if anything, when you have more complicated data structures flying around, and particularly if you work with several similar but different complicated structures, that could make having the types explicit much more useful for ensuring correctness and maintainability.

Absolutely. Sometimes the type is too complex not to be explicit about it.

Highly templated C++ is the highway to hell. If you haven't heard C++ templates are turing complete and so can also have the halting problem.

I really don't think it does that. Most refactoring is not like that. It is about changing things at a deeper level than just the type.

I don't think they enhance code readability - I think they make it worse. I never look at the type when I am reading code, it just gets in the way.

Semi-automatic refactoring tools is just one part of what a type system enables. A much bigger benefit in my opinion is that it immediately highlights issues in your code while you are refactoring. Basically answer "What do I still need to change to finish the refactoring?". Unit testing also gives you some of this, but is typically much slower - both in execution time, and the additional time it takes to figure out where the issue is.

When using languages with static typing amount of refactoring of that type is disproportionately large, so people notice how much the ide helps, without noticing that most of the help wouldn't be even necessary without the complexity added by static types.