Status of dependent types?

#1

I suppose that this is literally a FAQ, but … everything I have found on the web about dependent types in Haskell is dated a while ago, and all of the information makes it sound as if dependent types will be available in Haskell in the future, including the dependent haskell wiki page. I found discussion of regular updates about the subject (Daily updates on Dependent Haskell - #12 by rae), but the last I found was the first, in December 2022 (GHC+DH Weekly Update #1, 2022-12-07). That’s not so long ago, so maybe the folks working on dependent types are just busy. I understand that there were various challenging issues to address.

Or are dependent types already available in Haskell, and that’s why no there is no further discussion of the future of dependent types?

Thanks!

3 Likes
#2

From a quick search here:

…seems to be the most recent post (here anyway) - perhaps they’ve centralised their progress reports on a Serokell site?

3 Likes
#3

Thanks! (I did a search for “GHC+DH” but came up with nothing. Maybe a typo on my part?)

That’s still a few months old, but I don’t think weekly updates are needed. I will assume that DH is still in progress—not available, not dead. That’s really all that I want to know. And maybe an estimate of when certain usability milestones are expected (with the understanding that these things are difficult to predict).

(I did a search on Serokell too, but the blog posts I found on DT were old. Might have missed something.)

#4

Using a phrase search (adding literal double-quotes: “GHC+DH”) prevents the + symbol from being interpreted as inclusive-OR, effectively changing the search term to just GHC DH.

Updated previous post accordingly: now 6 results instead of 19.

#5

Ah! That’s it. Thanks.

#6

maybe i’m pessimistic, but to me, it seems like the lack of news is because of the lack of progress. no one is working on it. there’s nothing to report.

#7

No one is working on it.

…(heh) I very much doubt that, considering all the fanfare swirling around this one feature. There are two more likely possibilities:

  • lack of progress due to lack of staff e.g. due to illness or career change;

  • lack of progress due to an obstinate implementation difficulty, despite all the staff that have been assigned to the task.

As I see it, total abandonment would require the cancellation of approval for the associated proposal - a very unlikely decision, considering all the time and effort that has already been expended on this feature (not to mention the anticipation of its arrival)…

1 Like
#8

While I don’t know for sure, I’m afraid “no one is working on it” may not be all that far from the truth at the moment. GHC is primarily a volunteer-driven project and is not plentifully supplied with staff to assign to such tasks!

At Well-Typed we do have a few people paid to work on GHC, but mostly doing less glamorous tasks such as release management, bugfixes, performance improvements etc. rather than introducing new features. And there are some other companies employing people to work on certain features (e.g. the recent JS/WASM targets). But the Dependent Haskell efforts were mostly resting on a few motivated individuals (in particular @rae and @int-index, both of whom have contributed a great deal). So progress may well be slow and variable. That’s just the nature of volunteer projects, and I’m very grateful for all their efforts nonetheless.

It’s certainly not unusual for GHC proposals to be accepted and then sit around awaiting an implementer stepping up, unfortunately.

3 Likes
#9

I suppose there could be … dependencies between projects involved as well: fix/feature x for Dependent Haskell requires feature y in another part of Haskell, and that’s supposed to be handled by such and such folks, but they’re busy, or their change depends on some other change z handled by someone else who’s busy, etc.

#10

we had a phd working on this, but he was snagged by jane street. there is supposed to be a new guy at serokell but its not clear

#11

That Jane Street! And no serious talk of dependent types in OCaml.
Thanks.

(I’m not against OCaml. I used it for a signficant project.)

#12

There was a thread about this on r/haskell days ago: Reddit - Dive into anything, with some great reporting by @ziggurism.

4 Likes
#13

There have been a few things happening in my life that led to this hiatus, and it may take another few months for the situation to stabilize completely. However, I wouldn’t rule out the possibility that you might see new weekly updates this June, albeit smaller in volume.

20 Likes
#14

Thanks @int-index and everyone else. This is all much appreciated information.

For the sake of others’ convenience, I’ll note that the Reddit thread references an interesting post here about a year ago by Richard Eisenberg: Clarifying dependent types - #28 by rae. I had seen the top of that thread, but it didn’t seem relevant to my question and I didn’t read all the way through it. Turned out I was wrong. There are other relevant posts in that thread as well. I’m very glad that I asked, anyway, as there is additional helpful information in this thread, including @int-index’s answer.

2 Likes
#15

No one is working on it.

…(heh) I very much doubt that, considering all the fanfare swirling around this one feature. There are two more likely possibilities:

  • lack of progress due to lack of staff e.g. due to illness or career change;

you haven’t offered a more likely alternative than “no one is working on it”. lack of staff is just the reason that no one is working on it.

#16

A fair point. By “lack of staff”, I was thinking “not enough staff to make any further progress, but enough to keep e.g. the bugs under control”, rather than “no staff at all”.

I had assumed that this remark:

…made it clear that I believed at least one person somewhere was still working on this particular feature (even if it was basic maintenance - apparently not.

But this is now all irrelevant: from the other posts here, there really was no-one working on this, hence no progress - it seems you were correct from the outset…

#17

What I was really wondering about when began this thread was (a) is DH essentially dead—probably because it turned out to be too difficult—and (b) if it’s not dead, what kind of expectation about time should I have. I knew that it was a difficult project, and I was just wondering what to expect.

The claim that no one has been working on DH is not literally wrong about recent months, but @int-index’s response and the link to Eisenberg’s remarks make it clear that DH is not dead, even though I would not expect DH to be near final form soon. From my point of view, there was a pause in the work, but it will continue: @int-index is working on it in, a longer-term sense. That’s consistent with the claims about recent months. Half empty/half full, I guess.

1 Like
#18

I think there’s a misunderstanding in @mars0i’s question: DH is not a single feature but a whole series of features. The hard part of the software engineering is how to slide Dependent Typing (which is relatively well understood in dedicated languages) into an existing lazy functional language with already lots of high-level type features — but without breaking stuff.

I’m not expecting there’ll be an end-point where DHers will declare ‘done’. Rather DH thinking will gradually enter into all design decisions for Haskell — as we’re already seeing with the recent series of meta-/strategic proposals.

I think you should pitch your questions more like: when will I be able to use such-and-such feature from Eisenberg’s thesis/when will I no longer need Singleton types/etc.

2 Likes
#19

There are a bunch of “DH” GHC proposals that have already been accepted by the committee (a quick search yields these). From the GitHub reactions it seems the most popular ones are:

I wonder how close these are to being implemented.

#20

Thanks @AntC2. This is very helpful clarification. It’s much apppreciated.

Those are expert-level questions. It shouldn’t be expected that someone must read and understand a dissertation on X–even when it’s the fundamental document about X–before asking questions about X. Sure, the questions won’t be as specific, and can’t be given answers that are as detailed or informative, but that doesn’t mean one can’t ask, and learn more.

That is why the other part of your post is so helpful–because it summarizes what a naive questioner wouldn’t know to ask about.