atravers could have just started a separate thread to begin with if he had formulated his musings as proper questions inviting discussion.
I have started threads before:
and it seems they weren’t all that interesting. Based on that experience, I had no intention of starting another such thread. It was only when my final post on the other thread was hidden (and now moved here; this one, with the type Risk a b) that the decision was made to start this thread, and here we all are…
[…] since it is a total language, you can give its programs whatever (by-value, by-name, by-need) evaluation strategy you want […]
I’m not so sure: every other time I’ve seen “logic” and “laziness” appear in the same paragraph, there seems to always be another term: “lenient evaluation” (with a document about Verse being a recent one). Leniency isn’t laziness - in Verse, while the function can still be called before starting to evaluate its arguments, all arguments must eventually be evaluated for the logical predicates to be discharged. To me, that says “no infinite values”, such as the list of all prime numbers which appears here:
this is one of the main points why Dependent Haskell might become simpler than Haskell written nowadays!
- type families were meant to be simpler than associated types;
- and associated types were meant to be simpler that functional dependencies.
But people still sometimes use functional dependencies instead of type families - how exactly is that “simpler” ?
So people can just switch to Lean today, but they don’t! The ecosystem is not even close in size to Haskell’s (yet).
Perhaps those people think it would be a risk to move to such a nascent ecosystem. Therefore these suggestions:
If you want a fork of GHC that does not have dependent types, just do the fork! Or keep maintaining GHC 8.10 (or whatever version) so that it runs on modern systems and receives bug fixes.
are also risky.