I think the DH effort has been a pretty transparently incremental project. Many small steps, done well. With some needed bandage-ripping along the way.
1 Like
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.
I wasn’t expecting it, but thank you for your candor.
These days, I’m used to my posts being “flag-hidden” and as sgraf notes, people can still click “through the veil”. (But I still contact the moderators about having them unhidden).
But how many more “small steps” will be needed - to infinity, or beyond?
This is another reason why I’ve been suggesting adding laziness to a existing dependently-typed language (thought that would merely be a starting point, albeit an important one) - one by one, Haskell features could be added to that language, to arrive at parity with Haskell. Then the resulting language would be the dependently-typed successor to (non-dependent) Haskell.
I mean the people working on it have been taking a pretty deliberate engineering approach. And for efforts like this, enumerating steps up front tends to be a waste of time. The direction is clear, the goals imo seem pretty clear, and a lot of care is taking going from N to N+1 on all of this. If you have concrete issues with the current changes or planned next steps as they relate to Haskell overall, sure - bring them up. But I don’t think being this abstract about DH is anything more than online rhetoric.
5 Likes
This gets back to the post which (helped to) start all of this:
So where exactly is the “grand plan” for a “Dependent Haskell” ?
The reason I find Dependent Haskell interesting is that it is the best shot at having a production ready language with dependent types (if it is worth having, that is another issue altogether). Simply put, if you add dependent types to Haskell now, you have a production ready language with dependent types, now. Which is not the case with doing something to Agda or Lean, making them more Haskell like will not magically put them in the same weight category as Haskell.
3 Likes
[…] if you add dependent types to Haskell now, you have a production ready language with dependent types, now.
But you won’t be able to use dependent types to their full potential until all of the “many small steps, done well” are done. Hence my questions:
-
[…] how many more “small steps” will be needed - to infinity, or beyond?
-
[…] where exactly is the “grand plan” for a “Dependent Haskell” ?
Sure, but you also won’t be able to use Lazy Lean (despite the cool name!) to its full potential until it reaches the ecosystem size of Haskell.
I don’t know the answers to your questions. I’m adding something to this equation, because speaking purely of the language, yes it might be easier to go with the Lazy Lean, but also speaking purely of the ecosystem, it might be easier to go with Dependent Java. Speaking of both, I think Dependent Haskell is the closest one.
1 Like
I’ve been working on a task breakdown that I intend to publish by the end of this year.
As it stands, my draft for that page has 18 completed milestones, 5 ready for implementation, and 20 that are yet to be discussed and refined.
That’s in rather broad strokes – I expect to break it into smaller subtasks over time.
18 Likes
Sure, but you also won’t be able to use Lazy Lean (despite the cool name!) to its full potential until it reaches the ecosystem size of Haskell.
But that smaller ecosystem must surely mean that adding Haskell features to Lean (though I have previously suggested Agda) could be done more quickly than adding dependent types to Haskell and it’s much-larger ecosystem. Then once the the new dependent Lean-based language reaches parity with non-dependent Haskell, it would inherit most of the entire existing Haskell ecosystem as a bonus!
If that task breakdown is as informative as the ones available in the weekly GCC-Rust status reports, that would be quite helpful - thank you.
Moreover, such a breakdown may help to improve this project’s “bus factor” :
“What If Linus Torvalds Gets Hit By A Bus?” - An Empirical Study
because other Haskellers could then carry out some of the subtasks - as I currently understand it, only sand-witch and yourself are it’s primary developers.
The work on Dependent Haskell has already made my Haskell-writing life better today. TypeAbstractions and RequiredTypeArguements are breaths of fresh air compared to the contortions you would otherwise have to go through. The consistency regarding wildcards type A _ = ... is a good example of how the DH work is improving overall language consistency, which I consider a huge win.
DH has also spurred efforts to improve the compiler’s internals, which should be important to anyone who cares about Haskell’s future.
Regardless of the “final destination” – to be clear, I still really want foreach and am confident about its future – I am grateful for all of the hard work that is being put into DH, since these incremental steps are wins in and of themselves.
14 Likes
The work on Dependent Haskell has already made my Haskell-writing life better today.
That’s all well and good for an established Haskeller today, but what about new Haskellers today, tomorrow, next week next month, next year, or the next decade? If they perceive “the learning curve” of a “Dependent Haskell” to be too steep, they will simply go elsewhere…
1 Like
They can just stick to Haskell 98 features (or GHC2021/24) it’s not going anywhere.
Haskell is a deep, feature-rich language with many ways to do it. If beginners struggle, it’s because people don’t tell them they don’t need to know it all to use it. I sure don’t know it all and I do great.
8 Likes
They can just stick to Haskell 98 [or 2010] features […]
MicroHs: A Small Compiler for Haskell (2024)
The Haskell 98/2010 ecosystem which would conveniently allow that choice has long since disappeared - will GHC2021 be next?
I think most of the bread-and-butter libraries on Hackage don’t require many extensions at all. I use them the same as I used them a decade ago fine. So the ecosystem is there if you don’t want to go full DH.
And if a theoretical future library does require DH in its API…then either don’t use it or do? Or find a library for your needs that doesn’t lean on DH? If it doesn’t exist, go write it 
[…] the ecosystem is there if you don’t want to go full DH.
For now. And clearly your experience differs to one L. Augustsson…
[…] find a library for your needs that doesn’t lean on DH? If it doesn’t exist, go write it.
In addition to the many strict, unboxed and linear versions of already existing libraries? Ouch…
I had this exact theoretical debate about -XLinearTypes back in the day. “Oh if we do this then it’ll infect the ecosystem. And LTs is half baked so that’d be bad!”
Like…if there are libraries that use these new features, it’s because the new feature is useful. If it gets so popular that you can’t avoid it, that’s a gigantic success and we are living in a new frontier of ergonomic, production-ready dependent types.
It probably won’t be like that though 
but i’m trying to impress how this isn’t a real concern.
5 Likes
Would it? Like, Cabal will work with it somehow? HLS? Nix stuff? Random libraries? I’m sorry, but that doesn’t strike me as obvious, at all. In fact, I don’t think this has ever happened in the PL history, with C++ “inheriting” C, maybe, being the closest case.
And those alternatives are not even close to the detailed plan you wish DH to have. I don’t hold my breath for DH, and I share some of your skepticism, but at least the work is being done here and the ecosystem already exists. That is a huge, practical, difference to whatever “what if” argument. Count me in on Lazy Lean or Agile Agda hype train ride, but so far, it simply doesn’t exist, not even close.
3 Likes