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
I’m not really grasping the point. Certainly if you’re writing a Haskell compiler, and you want to test it out on existing packages or you want it to be self booting and still rely on existing packages, you might be annoyed that people are using LambdaCase, ScopedTypeVariables, DeriveFunctor, or any of the other popular extensions that you can’t compile. That’s quite reasonable. It feels like the one use case imaginable where other people’s haskell writing habits actually matter.
But I’m not seeing how that connects to the notion that new haskellers can’t just write regular old haskell. Unless they are trying to write production ready parsers for other people’s haskell, but if you try to do that as a new Haskeller its a self inflicted wound, I’d say.
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.
“If”, “might” - that seems rather “partial”. So what happens if there’s a Loss b? What’s the backup plan?
Having mentioned that, int-index’s listing of subtasks helping to arrive at a “dependent Haskell” more quickly could be enough - if dependent types in Haskell are a loss, it will be much easier to revert back to the most-recent non-dependent version of Haskell (because it won’t quite as old).
We already emulate dependent types in Haskell in many ways. This is not new. In that way, DH isn’t some completely greenfield thing. So I think you’re phrasing what DH is incorrectly. It isn’t some bugbear getting strapped onto GHC. It’s a smooth staircase and it isn’t one thing.
3 Likes
The difference is those features (strict, unboxed, and linear) are all non-default. Type-level programming is also non-default. I don’t understand the concern that DH is going to “take over the world” and force everyone to engage with type-level programming. Precedence clearly shows the opposite i.e. you generally have to go out of your way to use “fancy” features.
1 Like