The future of Dependent Haskell

#6

My argument was not about whether or not I agree with an opinion, rather that discussing such a claim would completely derail from the actual topic of the thread. Now that it has been broken off, I’m fine with discussing it. In fact, @atravers could have just started a separate thread to begin with if he had formulated his musings as proper questions inviting discussion.

First off: Unless you extract a Haskell program (which is lazy) from Agda, you cannot really “run” it.

Furthermore, since it is a total language, you can give its programs whatever (by-value, by-name, by-need) evaluation strategy you want; the type-checker guarantees they evaluate to the same value. Saying that we should “make Agda lazy” insinuates that

  1. It is not currently lazy
  2. It defines some (non-lazy) evaluation strategy in the first place.

Agda does define a notion of definitional equality modulo αβη, but that is full β reduction (I think, feel free to correct me), so it does not specify which redex to reduce next. (Although I think in practice one picks normal order reduction because it guarantees that a normal form is found if it exists.)

Don’t understand this point.
DT langs don’t have type families because in the majority of use cases one can just use (dependent) functions, which are much simpler to grasp and understand than type families. Indeed, this is one of the main points why Dependent Haskell might become simpler than Haskell written nowadays!

Some use cases of associated type families are better served by type classes with proper implicit resolution mechanisms.
Lean is a DT lang that is compiled with a strict semantics, and it has these very features.
So people can just switch to Lean today, but they don’t! The ecosystem is not even close in size to Haskell’s (yet).

I don’t understand what this reply has to do with Agda, dependent types and evaluation strategies.
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. That would be a constructive way to deal with your apparent frustration, and undoubtedly there are others who think the same as you and would be grateful for you engaging in this work.

6 Likes
#7

“Onus of proof” is on you.

““Maybe you’re wrong” is an accusation that must be supported by specific evidence. It cannot be uttered without context, grounds, or basis, i.e., arbitrarily.”

Otherwise, you are burning everyone to find a case to satisfy your skepticism, and the end results are likely: people doing the hard work find little encouragement and throw the towel. Who wins in that case? Ones wish GHC does not engage DT at all, and you may be right that you have sympathizers, but if such sentiment is so strong perhaps you could lead such a fork considering you had been very vocal about it since I have joined this community…

I wish the community has a strong voice to set the record straight, otherwise it is kinda toxic.

10 Likes
#8

“Maybe you’re wrong” is an accusation that must be supported by specific evidence.

As mentioned earlier:

But here’s some interesting graphs:

Having seen that “slow death” graph:

Otherwise, you are burning everyone to find a case to satisfy your skepticism […]

So what’s the backup plan if a fully-implemented “Dependent Haskell” also dies a slow death? As far as I can recall, I’ve only ever seen all the gains a “Dependent Haskell” can provide. But if there was no chance of losses then it wouldn’t be a Risk a b!

As sgraf noted in the other thread, the integration of dependent types into GHC is a major undertaking, much like the Fifth Gen. Project and BitC was. But there seems to be no discussion about what happens if said integration fails, hence that question to all supporters of “Dependent Haskell”.

Getting back to the requirement of proof: where’s the proof that a fully-implemented “Dependent Haskell” won’t fail? If that did exist, then the community would need that big “strong voice to set the record straight” - the “skeptics” could then look at that proof for themselves.

Ones wish GHC does not engage DT at all, and you may be right that you have sympathizers, but if such sentiment is so strong perhaps you could lead such a fork […]

A fork of an entire ecosystem the size of Haskell’s? Because that is what would be required. So if resources to maintain the current Haskell ecosystem are already low, then trying to fork it seems like a guaranteed recipe for failure, again due to resource constraints.

#9

🙋 I flagged the comment because the “…dependent types in action?” joke felt mean-spirited.

5 Likes
#10

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
#11

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:

https://www.haskell.org

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.

#12

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).

#13

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.

#14

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.

6 Likes
#15

This gets back to the post which (helped to) start all of this:

So where exactly is the “grand plan” for a “Dependent Haskell” ?

#16

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.

4 Likes
#17

[…] 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” ?

#18

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
#19

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.

19 Likes
#20

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!

#21

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.

#22

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.

15 Likes
#23

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
#24

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
#25

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?