I’ll be soon publishing a task breakdown for DH. In addition to the planned changes, I decided to include the recent history of related work (2018–2024) in the form of links to specific proposals, issues, and commits.
Here’s an example of what a single section is going to look like:
A notable omission in the task graph has caught my eye: We need to figure out the interaction between type families, associated types, and dependent types. This is a very foundational point that is both very nuanced and has long lasting consequences. If there is pre-existing agreement or even discussion of this I haven’t seen it.
Just to name a few nuances: Type families on the surface look like promoted functions but their equations aren’t (always) matched from top to bottom, and the equations can repeat quantified variables (example). That makes them more similar in spirit to conservatively extending a theory by adjoining a functional symbol. They use “evaluation by unification”, whereas “normalization by evaluation” is standard in dependent types. Associated types are currently just type families with a cosmetic attachment to a parent type class. However in a dependently typed language we would instead have them as Type-kinded fields in the class dictionary.
Thanks for creating the roadmap - it’s very detailed and well-organized! I have one suggestion for an addition, though. It’s hard to get an idea at a glance what was completed when, and what you’re currently working on. Could you possibly create a timeline that shows what date each commit was made, or proposal accepted? And then at the end, show what is currently being worked on. No need to project any future dates.
X2
I am specially interested in how and when adding dependent type support to GHC core happens. That sounds like an extremely radical change to the compiler
However that also means its an extremely interesting piece of work
Are we going to get dependent haskell updates soon? This is a very complex project that has had many false starts so it would be nice to see how it is going
Isn’t the Serokell effort descended pretty directly from the Eisenberg papers/ghc proposal?
I don’t really get the anxiety about velocity here. This is a huge complicated effort and it’s only worth it if done right, not fast. I’d guess those false starts were probably not especially starts at all compared to what’s been going on lately.
Last time I remember we extended the type system and went a little fast (-XLinearTypes), there was a bunch of freaking out about them being half baked lol.
Also I do not love that I feel like I’m discussing a corporate bullshit project update LOL “velocity” “false starts” is the PM in the room with us right now?
I didnt mention the project going slowly even once.
If you mean my comment “project that has had many false starts so it would be nice to see how it is going” . Yeah , lead devs and researchers have come and go ( several times, i think ) even before Vladislav and serokell decided to get this effort a go. And this doesnt mean the current people involved are doing it slowly. But given that and the fact there have been many proposals ( papers or otherwise ) that decide to change the details. It does suggest dependent haskell is a great undertaking that could encounter many difficulties.
“Last time I remember we extended the type system and went a little fast (-XLinearTypes), there was a bunch of freaking out about them being half baked lol.”
Yeah, but the same thing could happen due to the modifications being developed without external people giving input, due to the great difficulties of this project, etc
That is not one of my primary concerns and reasons for asking about updates either. Those would include : trying to understand whether dependent haskell is something i can prepare for in advance , whether the end result will be for me. And mostly my great interest for the process
Having tried to explain those points. I want to add i do not appreciate my comments being called “corporate bullshit” ( Specially because the main reason for them is trying to understand this project due to a great fascination over it ) Or you putting words in my mouth i never actually said , as far as i know. And lets leave it at that
Indeed. Let’s all recall the HF Guidelines for respecful communcation, which say (among other things) “In our communication, we consistently honour and affirm the passion, professional expertise, and good intentions of others. … We strive to be scrupulously polite at all times.”.
I’m sure that Ambrose meant no harm, but it’s really important that we all visibly treat each other with respect and honour.
ah yes sorry I wasn’t accusing you of anything. EDIT: And it does seem that I misunderstood your concerns too - sorry about that as well
I was more commenting off hand on my revulsion to the words I was typing on my screen. That sort of stuff is one of the biggest drags on Actually Good software in modern society, so I felt like I had to call it out because the goal of Dependent Haskell seems to be Actually Good software (a very refreshing goal compared to the Haskell day jobs I’ve had)
