New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support the design for dependent types #378
Conversation
I love this proposal. Choosing a design direction can have a much larger impact than deciding on any single feature. Finding and explaining the options we have in a way that makes the question well-defined and answerable is super valuable by itself. I need more time to write up my thoughts on the question itself, but for now I just want to thank you for bringing it up in the first place—this is a kind of discussion we'd benefit from having throughout the Haskell world. |
💯 support I want to reserve a bit of space though between accepting this proposal directly implying the rest - eg #270 in particular rules out some nice patterns (like constructor sharing the type's name) that I'd like to keep around somehow or at least think harder about. |
Remarks on Dependent Haskell initiative at large Serokell—after examining the body of research, the family of proposals, and popular arguments for and against DH with harsh scrutiny—has the following stance on the topic:
I would like to emphasise short-term benefits, which are often overlooked. People working on such a massive extension of GHC have to go through the entirety of GHC stack and, together with authors and co-authors of the components, reevaluate design and implementation. On more than one occasion, such reevaluation triggered at least refactoring, at most component redesign. For the regular Haskell users, right here, right now, the benefits of this process are twofold:
Dependent Haskell initiative and research conducted by @goldfirere was a threshold for us to start a dedicated GHC development department. Remarks on this proposal in particular I will let @int-index voice the official position of Serokell on this particular proposal, but my personal opinion is the following:
|
The situation up until now did at times feel a bit like a catch-22, where each individual proposal had to be considered solely on its individual merits, but would only unfold it's usefulness wholly when combined with several other proposal which also had to be considered on their own. I'm in full support of this proposal. One interesting area which would be made much more powerful with dependent types, that I didn't see in the list, is the potential for automatic type-driven program synthesis, like is being explored in Idris for example. I don't have a good link on hand to add via PR at the moment, but will do so if I find one. Though if anyone else knows of a fitting resource, feel free to mention it. |
I am strongly in favor of this proposal. When I look at design questions, I have a few mental tools to orient myself. One is a thought experiment about what a design would look like in an ideal world. If we could wave a magic wand and do away with restrictions of backwards compatibility and historical accident, what should Haskell look like? I can't imagine all the details, but I absolutely believe that some form of dependent types is part of that scenario. Not so much because I think dependent types would help improve safety in Haskell—I imagine they would, but not sure how much—but because dependent types have the potential to make Haskell substantially more expressive while, counter-intuitively, making the language simpler! Haskell, today, is a less like one language and more like two different languages grudgingly sharing space; a language of types and a language of values. It seems like dependent types would help better unify type-level and value-level Haskell while also providing more straightforward and ergonomic replacements for the motley collection of type-level features Haskell has evolved over the past three decades. Moreover, I don't see any alternative to dependent types to simplify Haskell without giving up on capabilities that, while awkward, are definitely useful. I've written my share of trickier type-level logic so I know just how awkward it can be, but also how useful. I've often found myself pining for dependent types not to prove a more complicated property at the type level but to make my existing types more direct and self-documenting and to avoid extra complexity and boilerplate. My ideal future Haskell would not only have dependent types, but would also remove features and extensions that dependent types obviate. It is much easier to learn and work with a language that does not have a wide range of subtly different ways to accomplish the same goals. Removing lots of features is not realistic in a living language with an active community, but that's not the point of the thought experiment. Instead, given an "ideal" point in the design space, the next question is how close we can get and what actions should we take to get there? While we can't just wish away existing features and complexity that would either be unnecessary or actively clash with dependent types, the least we can do is not add any more. From this perspective, this proposal—making design decisions with an eye towards fitting into a greater dependently typed whole—is the clear path forward. The only final caveat is whether we risk trying for perfection but getting nowhere. If I were not convinced dependent Haskell was a realistic goal, I would not recommend taking its design into consideration. But I've read some of @goldfirere's writing on the subject and I'm personally convinced that dependent types in Haskell are absolutely feasible. And if it's a realistic goal, we should start making decisions concurrent with it sooner rather than later. So I am entirely on board with this proposal. |
When in the history of man did short term thinking prove to be the best strategy years later? I’m for breaking things to improve them as long as there’s a good plan for the transition. |
@goldfirere firstly, I am very happy to see that you are still working on it - there were no big updates for a couple of years (although I may have missed some). Personally, I am strongly in favour of having ergonomic dependent types in Haskell, I wrote a bit about it, and neither singletons nor parameterized-utils offer viable approaches for many codebases. But my opinion is not what is important for the community decision. As a community, Haskell has to decide which values are more important to it - this excellent talk by Bryan Cantrill can give some context why the decision on values is so important: https://vimeo.com/230142234. There seems to be a split in the community into two (or even three) camps:
With all my respect to the work @snoyberg is doing, I strongly disagree that Haskell should be "dumbed down" to be adopted by all industries and all engineers. There are many more approachable languages out there (JavaScript, Python, Go, even Rust) and Haskel will never become as easy to start using as these languages - to me Haskell has unarguably a steeper learning path but it leads to a much higher (or even infinitely higher) mountain, but if all you need is to get on top of a hill, why would you want to climb a wall? I believe that where Haskell creates a huge value is the growing second camp - as more and more software based businesses realise that they need much lower failure rate than the languages they use allow to achieve, they will be turning to Haskell and type-driven modelling as a solution. So the argument between I am definitely on the side of Haskell being the choice for users that need "rigor" over "approachability" - and it is the only real choice for them today - so, from my point of view, the only viable choice that will ensure longevity of Haskell is "rigor", and, as a consequence, forward looking ergonomic dependent types. But community has to answer the question about "rigor" vs "approachability" first, as at the moment there is no alignment. |
One consideration seems to be screamingly absent from the proposal: what is ergonomic for newbies/learners of a lazy functional language? Or do we expect newbies would be able to dive into Dependent typing from the get-go? Or has GHC more or less abandoned the idea it's a platform for newbies to learn Haskell? A few immediate observations:
|
First of all I fully in support of dependent types and I think they bring a lot of benefits to the language. For beginners, there will hardly be any difference. They might encounter an outdated tutorial where For intermediate Haskellers, I see the mentioned benefit because dependent type (IMO) unify and thus simplify the language. There is so looking up syntactic differences for type families, wondering about limitations, trying to have constraints on arguments etc, because it is just a normal function, something they are familiar with from the beginning. Just pattern match on an argument (that happens to be of "kind" For advanced users, dependent types enable more complex checks at lower syntactic noise (e.g. compared to singletons). One might argue that code written by these users is hard to understand for the other groups, but this is true for any language. Be it clever pointer magic in C for optimization purposes, C++ template shenanigans or emulating higher kinded types in Java. Every company/team/individual has to decide where the border for "too much" is for their use case. |
I am also strongly in favour of this proposal, for many of the same reasons others have outlined above. I have two comments, unrelated to each other: NewcomersI do think @AntC2's point about new learners is an important one, and there's going to be some inevitable selection bias in the responses to this proposal, as potential future learners are not going to weigh in (by definition). There are parts of the language that are deeply ingrained in education materials that are going to be much harder to change than others, so perhaps it might be worth classifying new changes with respect to which "existing version of Haskell" they fit in. For example, the punning syntax for tuples might be much more important to keep (or rather, much more painful to drop) than scoping rules around the That being said, many other languages seem to be able to cope with change quite well. Java has gone through several major changes over the years. Why do newcomers not struggle with these changes? Reflecting on my own learning experience, it's because there is a clear notion of what Java means in 2020. For instance, no one is trying to learn the 1.4 flavour, as learners either interact with the language via some higher education system or simply by searching for "learn java in 2020", both of which will give them access to a recent snapshot of the language. The advantage of GHC's extensions is modularity, but this modularity is what makes learning the language harder (and I'm projecting my own learning experience here once again). With that said, I think #372 is a crucial prerequisite to this proposal. We can much more confidently take a stance in favouring ergonomic dependent types if we have an authoritative reference for where the language stands today. Education materials can then be explicitly marked as outdated with respect to "GHC2020". When we think of newcomers, of course it's important to think of their experience in the first couple of days when they learn the basic syntax, but it's equally important to allow them to smoothly learn more advanced features of the language. #242I see that the proposal already includes a section on unsaturated type families, mentioning syntax as the point of contention. In fact, there is another decision to be made, around type inference, where we can either retain backwards compatibility or make future uses much more ergonomic. I don't want to use up any more space here, so I will refer anyone interested to the relevant section (point 2.) of the proposal. When I wrote the proposal I kept backwards compatibility in mind, with the tacit understanding that that's the clearly favourable route. The discussion around taking a stronger stance on future ergonomics gave me more confidence to consider a better design that might break some programs today. The motivation for #242 stands whether or not this current proposal is accepted, but there are concrete decisions to be made based on the outcome here. |
Even though I am undecided yet, let me try to give a different view of how I see Haskell as a language. For me, Haskell is (or at least started as) a nice syntax over System Fω + data types. Inference, type classes, deriving, ... are useful as they remove some of the more annoying parts of using System Fω directly. In general, I am supportive of those extensions which allows the programmer more control over that underlying core language (like impredicative types, or type variables in patterns -- a way to express type abstraction). And very importantly, System Fω separates the type and the term worlds. Of course, right now GHC comes with sort of a dependently-kinded type language, and I've always found this to be a great innovation! Whereas other languages struggle with erasure, when programming in Haskell I always assume that my types will be removed at runtime. The main downside, of course, is that when I need that information, I need to reify them as singletons. For me, this is a good design choice in the language. Furthermore, how would a version of GHC look like when such a simple heuristic is no longer true? Unfortunately, I think many of the voices here underestimate the difficulties related to newcomers. The fact that the language is more "unified" does not imply that it is easier. We need to acknowledge that people are used to the dichotomy between values and types. Finally, I don't agree with @serokellcao on the fact that Dependent Haskell on itself has anything to do with how companies invest on GHC and the ecosystem in general (maybe in their case it's true, of course). Speaking personally, I've found the combination of GADTs + LiquidHaskell to be more approachable than hardcore Dependent Haskell. |
Very glad to see this, I've long been clamoring for this sort of thing. A few points I've said elsewhere but want to repeat here: Having our cake and eating it tooIn the grand tradition of the bikeshed observation, the most contentious stuff is often the simplest to understand---and implement. It would not be hard to e.g. support separated-namespace and single-namespace name resolution in perpetuity, so everyone gets what they want. NewcomersIgnoring backwards compat, and assuming beginners don't need
The principles to me are also fairly clear:
Importantly this is conflicts with both traditional Haskell and ergonomic dependent types. My conclusions are:
|
Some comments about the proposal itself:
I take this as showing how far you can go with today's machinery! In fact, what I would like to have is automatic derivation and syntax for singletons, which is often the missing piece, in the same way I have derivation of
I don't think this is necessarily true. There are lots of places open for contribution, we have seen an increase in the last years even though we don't have DH yet: new |
A small comment FWIW: I do feel strongly that punning adds confusion for beginners, especially who aren't used to thinking clearly about types vs terms. I remember being really confused by the syntax for I don't know what to do with that exactly. |
I read this proposal as "we can't agree within the GHC team on whether we are doing depending types for real or just kidding around, so we decided to ask the community". In my view, both "doing dependent types for real" and "not doing them at all" are sensible options, unlike "just kidding around". So I'd encourage the GHC team to bite the bullet and commit to either of the sensible options. |
I really don't think even more effort should be put into singletons machinery. It comes across as nothing more than status quo bias to suggest it is a good experience in any way. I have written a reasonable amount of Agda but would basically never reach for singletons in Haskell because it is so needlessly complicated in comparison. Richard and others have written plenty about relevance vs irrelevance as an importance axis in dependent haskell and we now have developments like quantitative type theory, so I can't say that "knowing what will be erased" is a very good argument for Haskell as it currently exists. |
As a software engineer - not an academic - I've been using Haskell for the past 2 years to get stuff done correctly in less time. The biggest problem - as some comments already pointed out - is the existence of " two languages": "Standard" Haskell (Haskell 98) and "Dependent" Haskell. I found a big barrier when trying to move from "Standard" to "Dependent" since a lot of features in the later one feel bolted in, and as such, are harder to understand. I think that @jvanbruegge makes a great observation regarding the "experience level" of the Haskell developer:
A lot of docs will get outdated if "Dependent" Haskell were to become "Standard" Haskell. But as @kcsongor pointed out
Is important to note that moving forward to "Dependent" Haskell will break stuff and it should - from documentation to language extensions. Trying to find a middle ground by compromises will satisfy neither group of users.
This is, for me, the most important part. Using "Dependent" Haskell - or trying in my case - forces the user to learn a whole new world of syntax, rules and constraints. Simplifying the language - and with that, the whole tooling - should be a desirable goal.
Again, on point with the analysis. Finally, I think that moving Haskell to a "dependently typed" language should come also with a new Haskell Standard, be it 2020 or 20XX, in order to properly reflect the change in direction and formally define what the community actually means with it. And of course, the slogan from the main website should be changed to "An advanced, purely functional, dependently typed programming language". |
As a beginner, and found the punning of type constructors and data constructors confusing. |
Can anyone give concrete examples of how making dependent types more ergonomic, is going to make it harder for newcomers to learn Haskell?
Does this trash some existing documentation? Yes. But I believe the potential upside of proper support is big enough to justify some friction to newcomers. Because in the long term all these changes do make things easier and more consistent. I never even knew this was up for debate, I assumed this was always a goal of Haskell to become fully dependently typed. I'm hoping for more libraries like servant, grenade, type-of-html etc. Those are all amazing projects and with a lower barrier to dependent Haskell we can expect even more of this! |
I regularly work on a fairly large codebase that is firmly in the direction of Dependent Haskell (https://github.com/GaloisInc/crucible), so I am pretty thoroughly in favor of making it more ergonomic. We use parameterized-utils (http://hackage.haskell.org/package/parameterized-utils) instead of singletons, but I think the two are approximately equally unpleasant. In crucible and and its related codebases, I get significant value from the invariants we are able to encode in the type system given the current state of dependent-ish types in Haskell. I consider myself in the "more is better" camp of enforcing invariants in the type system. While I am strongly in favor of improved ergonomics, I am more interested in what I think of as "ergonomics in the large" as opposed to "ergonomics in the small". As an example of "ergonomics in the small", removing uses of So far the discussion I have seen (in this thread and others relating to Dependent Haskell) has mentioned a number of proposals that, from an outsiders perspective, chip away at the edges of Dependent Haskell. This proposal is essentially asking: Should we steer the ship towards Dependent Haskell, which may involve adopting intermediate changes that do not obviously individually align with previous criteria for proposal acceptance. I have two questions:
I think it would be very helpful to articulate those things; if we do, all of these proposals can be a bit more easily contextualized to let us know why they are important to the Dependent Haskell story. Each proposal in this space could include some commentary on how it brings us closer to Dependent Haskell. Maybe that information is completely implicitly understood by the committee members, but surfacing it explicitly would certainly help the community engage productively in these conversations. As a further point of clarification, some of the conversation around Dependent Haskell makes it seem like some people think that this work will result in Haskell becoming Dependent Haskell and ghc becoming a Dependent Haskell compiler. At least, I'm inferring that belief from the concerns people raise around Dependent Haskell becoming a serious impediment to learning Haskell. My understanding has always been that nearly all of the changes under discussion are going to be hidden under language extensions (hopefully to be all subsumed one day by |
+1 to all this. A lot of the doubtful feedback to this proposal so far has been about the feasibility, implementation, and timeline of Dependent Haskell period. People seem uncomfortable to sign on to a cultural commitment to something they see as "vague." |
There's two ways to answer this at this:
The first one is the "expressive power" criterion, as pi types are the cornerstone which generates everything else. The second one is the "cleaned up unnecessary differences" one, after which there is nothing more to unify. While 1 is the "shiny new stuff" that builds excitement, I think it's 2 that's actually more important. And in recent years, the work that has happened has mainly been after the lower-hanging parts of 2, to "clean the workbench" before we finish crafting 1. I think that's good, too. |
I'm generally in favor of this proposal, but there's one point I find confusing:
Does this imply that there should be no breaking changes whatsoever, or that we should try to minimize them and provide reasonable migration strategies? Because the former just doesn't sound realistic, while the latter should be indeed an important consideration. |
I'd say that we have arrived when the
https://richarde.dev/papers/2016/thesis/eisenberg-thesis.pdf is a great read on that, laying out the foundation. There are also more recent developments in this space, for example https://richarde.dev/papers/2017/dep-haskell-spec/dep-haskell-spec.pdf and https://richarde.dev/papers/2019/dep-roles/dep-roles.pdf, maybe more. But there definitely has been enough theoretical work to set the direction and begin implementation. Future results are likely to be informed by implementation experience. |
First off, it's exciting to see so much enthusiasm here! Thanks for joining the discussion. :)
While I certainly agree that long-term thinking is best, I want to clarify that I do not think rejection of this proposal is necessarily prioritizing short-term over long-term. Instead, it's perhaps prioritizing what Haskell has been (in part, what has made it successful thus far) over what Haskell could be.
Also to clarify: I don't think we have to break anything... just perhaps design new features in a way that may be (slightly!) awkward at first, only to fit in better later.
I think these are great points, and it's an oversight of the proposal that these points were not addressed. I've added a new "Effect", saying that this proposal is agnostic on this point -- but that the committee should do a better job of considering learnability. The proposal is agnostic because it's not clear that dependent types make a language harder to learn. If a proposal would make the language harder to learn, then we should seek to find a way to avoid that complication. Perhaps we should require proposals to be more explicit about error messages, and to ensure that the experience of a user who does not want to use the new feature is not degraded. My guess is that learnability issues are easier to address than the criterion 1 from the proposal. Why? Because criteria 1 and 2 in the proposal are both about the input to GHC, while a learnability concern can often be addressed by improving GHC's output. Thus I think learnability is less likely to end up in direct conflict with dependent types.
Interesting. I had not thought of it this way. Perhaps. I'm not currently inclined to add this to the proposal, but I see your point.
I've added a little commentary to the proposal on this point. See #102, where syntax is proposed that will keep the choice between erased compile-time terms and unerased compile-time terms (a
I can name specific people who have already left the Haskell community due to our lack of ergonomic dependent types (and ambivalence toward getting there), and name specific other people who are around today but have told me that they would strongly consider leaving if we close the door to ergonomic dependent types. I won't do this in public. However, I do believe that a rejection of this proposal would still leave us with an interesting language that would continue to attract research and great thinkers -- it's just that there would be specific (but far from universal) losses.
To be clear, this proposal is not written by "we the GHC team", but just by me. No one else on the committee asked me to do this. If I'm to be honest, I wrote this proposal because I worried that the committee might naturally lean against the line of thought advocated by the proposal. Yet I also thought that the community would be in support. And so the proposal is both a way of clarifying what we're talking about and attracting the community support that might convince the committee to go in a different direction than they might go otherwise.
My old answer was GHC 9.0. Now it's GHC 10.0. More usefully, I don't think there is one point that will say we have Dependent Haskell. Allowing normal term-level functions to be used at compile-time (that is, to the right of
At a high level, read Chapter 4 of my thesis. The chapter has no typing rules, and it should be understandable by an intermediate Haskeller. That text still uses the There is a chance that new research around quantitative type theories (including my upcoming POPL paper) may change the suggested
Most new features are guarded behind an extension flag, and so maintaining backward compatibility should usually be relatively easy. However, I recognize there are exceptions. For example, we probably need
Ooh. I can't wait. :) Throughout several comments, there were a number of good points raised that (to me) fit better in the debate on individual proposals. I will not address them here (even to say which comments they were), as my experience is that even mentioning them again will continue debate here, where I think it does not belong. |
My question above about the goals of Dependent Haskell was partly rhetorical (I am already sold on it - give me those pi types). I wanted to bring it up because I think it wouldn't take much to communicate the goals of Dependent Haskell more accessibly to a wider audience and address a lot of uncertainty all at once. Reading parts of Richard's thesis is very informative, but not approachable to everyone. A simple introduction section in the wiki entry on Dependent Haskell (https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell) that tells people what this is all about would go a long way. It would be great to centralize a pitch for the work in one place (and that is, happily, the first hit when you search for Dependent Haskell). A few simple things that would probably help include noting that:
The current wiki page makes references to things like "the new Haskell will...". I think phrasing like that is a useful shortcut for discussing the details of a change, but it probably drives some of the confusion in general audiences when new proposals come up. It seems like most of the concrete proposals referenced in this discussion map pretty clearly to sections in the existing Dependent Haskell page. I think that is great and grounds them into a concrete roadmap to let us know when we do actually have Dependent Haskell. I like the dual phrasings of Dependent Haskell that have come up in this thread:
Is it possible to classify the initiatives on the Dependent Haskell page into those required to achieve those goals, versus those that simply make them more ergonomic to use? If the answer is that they are all prerequisites, that is really interesting information that helps motivate individual proposals even more. |
Hmm. I'm finding the proposal unclear wrt call sites. Is Section 4.1, esp. point 4, all presuming
If that's to happen irrespective of You might be right: the following bullet says "Guard the data variable occurrences [in types] behind the
Sure. If you're wanting to pass around types like that, you clearly are au fait with DH, and you'll be happy writing types as arguments in expressions/you won't be using |
@AntC2 For error messages, GHC already checks whether a type constructor is in scope when it can't find a data constructor: ghci> Int
<interactive>:17:1: error:
* Illegal term-level use of the type constructor `Int' This was done in the context of #18740 with the goal of improving the error message, with the idea that this informs the user that they're doing something more fundamentally wrong than just misspelling a data constructor. Previously the error would simply say that the data constructor Edit 2: I now realize this goes somewhat against what I said previously, that the renamer will still stop at the term-level and not throw a corresponding type error if no extension for it is enabled. However, I do believe what was done here is an improvement to the error message, for DHers and non-DHers alike. Edit: Though by the way, I'm inclined to agree that data variable occurrences and |
While, once upon a time, we did ask commenters to refrain from participating during review, that was deemed ineffective, and so we changed that policy some time ago. It probably just got communicated in a PR making the change, not more broadly, so apologies if this catches you unaware. (It was ineffective in large part because few were aware of the rule!) Bottom line: there is no such rule any more, and you should write a comment where you think it is more germane. Others have, above, made similar arguments to what I would make, so I'll restrict myself to matters of fact: The LSP has always been respected, in 2010 and with DataKinds. To remind ourselves:
@AntC2 agrees that this was respected in 2010. I claim that it is still respected today. (Quotes below from @AntC2. Also, I should say: I hope this dissection is OK -- comments on the internet live forever, and I think it's helpful to everyone to try to correct misunderstandings.)
I see only two namespaces. Kind syntax (when it was separate from type-syntax, pre-8.0) drew from the type-level namespace.
I disagree: All declarations are associated with precisely one namespace. In particular, data constructors are in the data-level namespace. Forgetting about my crusade against the idea of "promotion", the previous sentence has always been true: data constructor names have never been available in the type-level namespace.
I agree here, but with the following addition: for ambiguous identifiers (this can happen only in type-syntax for capitalized identifiers), the type-level namespace is preferred, and thus the occurrence is no longer ambiguous.
I'm not sure what this means. At no point must the compiler invoke the type system when doing name resolution (beyond ambiguous record field names, which are not at issue here). In the glorious future, some programmers will program as if there is one namespace, some won't. Both modes will be supported. All the LSP says is that, for someone thinking about two namespaces, it will be possible to tell which namespace an occurrence comes from without invoking the type system. Lastly: as others have said, I do hope library authors are careful in how they use language features. That's a cause worthy of concern, but it would hobble the Haskell language if we never introduced a feature that library authors could abuse. I would not expect |
BTW, whilst we're talking about lists and tuples and punning ... Only a few months ago the libraries team added
as the definitive |
Wrong? No. It will be a little awkward to work with, just like it's a little awkward to work with |
BTW (2) I'm finding the eye slips too easily past the
|
I surely support this proposal !! Though only beginning learning Haskell, I think that dependent types will essentially add to the expressiveness of the Haskell language in a way as profound as, if not much more than, how simple types have added to that of the Lambda Calculus itself. And as such it is the necessary direction forward and should actually be considered of the utmost priority over other, perhaps minor, features. |
@nomeata, I suspect that this MR needs to be relabelled. |
Thanks! |
@nomeata I think this should also be labelled as implemented, because I don't think there is any concrete work to be done. That way it is easier to filter accepted proposals that really do still need implementation work. |
Hmm, calling “Dependent Types” implemented is a stretch :-) I agree the binary nature of labels does not do reality justice… What do you think, @goldfirere. |
I mean, looking at the proposed change specification, this proposal is "just" a set of guidelines for the committee. I would say it is implemented if the committee uses these guidelines, which I assume they do now. This proposal is not proposing any actual implementation work. |
That’s a fair perspective. I’ll add the label since you say it's more useful that way; if someone complains we can still un-label it. |
I agree that this could be labeled implemented, though I don't feel strongly. |
Do we have dependent types? Depends on the point of view? Maybe? 🤷🏻♂️ |
The proposal has been accepted; the following discussion is mostly of historic interest.
This proposal describes the tension between two important criteria the committee (and broader community) have implicitly been using to evaluate new features. In several proposals (#270, #281, and #291), these criteria -- essentially, cohesiveness of the language today vs. cohesiveness of a hypothetical future with dependent types -- appear to be at odds, with no mutually pleasing design. The proposal payload is to explicitly acknowledge the importance of designing with ergonomic dependent types in mind, and accepting this proposal (or rejecting it) will hopefully clarify our deliberations on other proposals.
Put more simply: Support this proposal if you think GHC should design with an eye toward adopting ergonomic dependent types; argue against this proposal if you think GHC should focus more on maintaining cohesion in the short term, possibly closing off future avenues toward ergonomic dependent types.
Rendered