3 ms·
> 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 indefi
by js8 2y ago
> 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.
- DonaldPShimoda 2y agoNo, 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.
- cubefox 2y agoI'm not even sure if any human is still writing code in 10 years.
- ParetoOptimal 2y agoBased on what?
- cubefox 2y agoLooking back where we were 10 years ago in terms of AI: If we get a similar jump in 10 years from now, we have superintelligence.
- NoGravitas 2y agoHonestly, it's more likely that we won't have the working infrastructure for running computer programs, making writing them fairly pointless.