> As the typed FP ecosystem is moving towards dependent typing (Agda, Idris, Lean), this becomes an issue, because you don't want the type checker to run indefinitely.
First of all, does ecosystem move to dependent types? I think the practical value of Hindley-Milner is exactly in the fact that there is a nice boundary between types and terms.
Second, why would type checking running indefinitely be a practical problem? If I can't prove a theorem, I can't use it. The program that doesn't typecheck in practical amount of time is in practice identical to non-type-checked program, i.e. no worse than a status quo.
No, the FP community at large is definitely not moving toward dependent types. However, much more of the FP research community is now focused on dependent types, but a good chunk of that research is concerned with questions like "How do we make X benefit of dependent types work in a more limited fashion for languages without a fully dependent type system?"
I think we'll continue to see lots of work in this direction and, subsequently, a lot of more mainstream FP languages will adopt features derived from dependent types research, but it's not like everybody's going to be writing Agda or Coq or Idris in 10 years instead of, like, OCaml and Haskell.
First of all, does ecosystem move to dependent types? I think the practical value of Hindley-Milner is exactly in the fact that there is a nice boundary between types and terms.
Second, why would type checking running indefinitely be a practical problem? If I can't prove a theorem, I can't use it. The program that doesn't typecheck in practical amount of time is in practice identical to non-type-checked program, i.e. no worse than a status quo.