3 ms·

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.

Arcsech 9y ago
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.
- catnaroek 9y ago
  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.
- Merovius 9y ago
  > 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.
seanwilson 9y ago
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.

Arcsech 9y ago

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.

catnaroek 9y ago
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.
Merovius 9y ago
> 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.

seanwilson 9y ago

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.