[…] realize I still don’t understand the roadmap to DT […]
-
Perhaps it would be faster to make Agda lazy.
-
As for these reports from Serokell:
in contrast to:
or:
1 Like
I had nothing to do with the decision, but I think it is good that it has been flagged.
Note that anyone can still read the comment and chuckle if they feel like it. However, it adds nothing to the topic, arguably spreads FUD (“make Agda lazy” is inaccurate on a few levels) and has the potential to derail it. (Just like this answer, in fact. I would be fine if our discussion were broken out or hidden.)
Flagging the comment as such ensures that people do not engage.
2 Likes
data Risk a b = Loss a | Gain b
So to everyone who truly believes that “Dependent Haskell” won’t go the way of the Fifth Generation Computer Systems project or the BitC programming language:
What if you are wrong?
I find it ridiculous to flag comments that are not offensive in absolutely any way (unless the comment was edited along the way).
What? Lol. It’s just an opinion prefixed with “perhaps”. I certainly disagree with that opinion, but I also disagree with your “it is good that it has been flagged” opinion, should I now report your comment? This is just silly.
8 Likes
Having mentioned it elsewhere:
on what levels is it inaccurate?
1 Like
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
- It is not currently lazy
- 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
“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
“Maybe you’re wrong” is an accusation that must be supported by specific evidence.
As mentioned earlier:
-
The BitC programming language project
But here’s some interesting graphs:
-
slide 16 of 74:
-
slide 14:
But I could always find more “research write-offs” like the aforementioned two - I’m reasonably sure there’s plenty of them out there!
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.
🙋 I flagged the comment because the “…dependent types in action?” joke felt mean-spirited.
5 Likes
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.
6 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.
4 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.
19 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!