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
Since there's many moving parts, I think it makes a lot of sense to establish consensus on the direction like this upfront.

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:

Dependent Haskell initiative has immense benefits for Haskell ecosystem, ergonomics and scope of use both in long- and short-terms.

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:

• GHC codebase is actively reviewed
• Fluency of GHC developers increase across GHC codebase, meaning better maintenance
• Companies who have strategic interest in Haskell are sponsoring GHC development, making compiler better faster

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:

Ergonomic design is the single most important factor for a smooth adoption of DH. If Haskell is to become the dependently typed language, such design should be prioritised and intent of moving Haskell in the direction where such design is possible should be communicated by the committee. Conversely, inaction or declination of this proposal will be detrimental to GHC both in the short-term and long-term (see previous section) and will discourage contributions to GHC.

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:

• the first is led by @snoyberg, that has a very strong focus on Haskel being a reliable tool for production code, and I should say I am using the stack (not just the "stack") it advocates - Reader pattern, unliftio (but not rio), etc. But to me this camp is taking it way too far - almost nobody came to Haskell with the desire to write "boring Haskell", many people I know chose Haskell because it allows to express type invariants in a wider range of scenarios than other languages. The top values for this camp are "reliability" and "approachability" - that is, be able to write production code that is highly maintainable by a wider group of engineers thanks to its approachability.

• the second group is a growing number of commercial users who care much less about "approachability", and much more about "rigor" - they have very high expectations of the correctness and reliability of the software systems they develop, and do rigorous modelling in types. Galois would be a prime example, but there is also a growing number of financial and communication sector companies who have very high expectations about software reliability that can be only achieved via type-driven / algebra-driven design approaches. For these users a wider range of scenarios expressible as type invariants helps them achieve their goals better.

• the third group is "research" - a strong focus on Haskell being a research playground for advanced type systems, and you, Simon, etc. seem to be here. This camp is super important, but unless it will see creating commercial and society value as a very important priority it risks losing industry support from both 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 backward compatible (EDIT: as we are not talking about sacrificing backward compatibility here, from re-reading the proposal, but only about more isolated vs cross-cutting, the position in favour of this proposal can be even stronger) and forward looking approach is the argument between "approachability" and "rigor" - do we choose easier migration path and learning to retain more users, or do we focus on users who need "rigor" over "approachability". Given that there are many languages that offer better "approachability" than Haskel ever will, it would be a strange choice for the community, and yet, that is the choice that @snoyberg and many other people advocate.

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:

• Punning of type-level names/syntax with term-level names/syntax (ref Support pun-free code #270, and this is the complexity with Visible forall in types of terms, and types in terms #281's design) runs very deep -- particularly in all the education material for newbies. I'm thinking of the hard-coded "/syntax" for lists and tuples, as much as the user-introduced names.

• How do other Dependently-typed languages express lists and tuples? Or do they? Although lists have a long pedigree in FP since LISP, perhaps they're a data structure that should be avoided? OTOH type-level lists using [ , ] syntax have become ubiquitous in fancy type manipulations, since DataKinds were introduced. I see even less hope of removing tuple syntax from terms or types: which to remove, and what to replace it with?

• For those not using Dependent typing (including newbies, or programmers writing client code which perhaps uses packages with Dependently-typed code but isn't itself dependently-typed): does the proposal favour the coding ergonomics for the package-supplier rather than the package-importer?

• It seems when fancier type machinery is introduced, it's very difficult to insulate newbies or opters-outers from the internals. This isn't about merely hiding the feature behind an extension. Almost always the machinery grins through in error messages. The newbie makes a newbie mistake, or a simple typo. They get an avalanche of incomprehensible gobbledegook, ending with a suggestion that fancy-feature-X might help. (A current example would be GHC's mania for suggesting AllowAmbiguousTypes: almost always for a newbie this will make things a whole lot worse.)

• Re Type applications in patterns #126 / Simplify scoping for type applications in patterns #291 and the scoping of type variables, I can't help but feel this is a symptom of the design for ScopedTypeVariables being disergonomic. That is, not the old PatternSignatures part, but the design where the site of introducing tyvars is textually remote from the pattern match and not syntactically bound to it. (I'm saying that with the benefit of a great deal of hindsight.) Then the argument for ergonomics here is not really an issue of Dependent typing: type applications in patterns seems only a bit of syntactic sugar for PatternSignatures + FunctionResultTypeSignatures. If we'd had that in place first, I wonder if the design for ScopedTypeVariables would have been different -- or indeed considered not worth the candle? I'd favour accepting Simplify scoping for type applications in patterns #291 irrespective of Dependent-typing desiderata, because the non-PatternSignatures part of ScopedTypeVariables is smelly design. (If we're worried about consistency in Haskell, it's a place where explicit forall is not merely a stylistic choice.)

First of all I fully in support of dependent types and I think they bring a lot of benefits to the language.
One concern I do not share is ease of understanding. In fact, I think dependent types will make it easier to understand complex code. What I mean is:

For beginners, there will hardly be any difference. They might encounter an outdated tutorial where [a] is used to say List a (assuming we have no punning in base and are after the transition period of X years) but then either the compiler or Stackoverflow will tell them to use the new syntax, no big deal. I would say this group reaches from absolute newbies fiddling with recursion and IO to people that start to get used to monad transformers.

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" Type) and do what you want. No wondering if this () is a value, a type or a kind. It just is ().

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:

Newcomers

I 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 forall keyword.

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.
@AntC2 mentioned AllowAmbiguousTypes, which (together with TypeApplications) I think is a great example of a design decision that was made with criterion 1 in mind - these features are usable without modifying existing code, but at the expense of a great deal of confusion. If we reconsider the situation in light of criterion 2, I think the decision we would make today is to retire AllowAmbiguousTypes and only allow visible type application to already unambiguous types. To handle the other (today ambiguous) cases, we would introduce visible foralls (#281)

#242

I 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 too

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

Newcomers

Ignoring backwards compat, and assuming beginners don't need foreach -> but might need forall ->, it seems obvious to me what make the language easiest for beginners:

• Must define variables as if there is one namespace: no punning
• Must use variables as if there are two namespaces: using type variable in term and vice-versa is name resolution error
• No punned syntax: e.g. [] has one meaning everywhere
• (type stuff) is the escape for working with forall -> terms
• No AllowAmbiguousTypes
• Double namespace in that only term variables
• Patterns that want to assert equality rather than bind fresh vars need a special syntax, e.g. = a
• @ could just effect visibility, or also visibility and namespace (like today), since there is no invisible relevant stuff for beginners.

The principles to me are also fairly clear:

• Admit as few programs as possible, dividing features like name-spacing to cherry-pick to be more conservative
• Err on the side of more explicitness/noise with type pat and = var

Importantly this is conflicts with both traditional Haskell and ergonomic dependent types. My conclusions are:

• Experts and beginners need different things, and pretending otherwise is a disservice to both
  • My one criteria for how far the languages diverse is libraries should still interoperate flawlessly. None of this stuff is deeply about semantics so there's no problem here.
• Traditional Haskell is a poor proxy for any specific use-case. Constraints on our resources in migrating documentation and existing code are very real and should be taken seriously, but those are the only things we should worry about with breaking tradition; not "timeless" questions of who/what does the language serve.

Some comments about the proposal itself:

Motivation for dependent types
... list of papers ...

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

A rejection of this proposal would likely lead to some "brain drain": I am aware of a number of active contributors to our community who are excited about the possibility of dependent types. Rejecting this proposal may signal to them that Haskell is not interested in what they have to offer; they may join other language communities.

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 deriving facilities, better exhaustiveness checkers, join points...

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 data declarations.

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

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:

For beginners, there will hardly be any difference. They might encounter an outdated tutorial where [a] is used to say List a (assuming we have no punning in base and are after the transition period of X years) but then either the compiler or Stackoverflow will tell them to use the new syntax, no big deal. I would say this group reaches from absolute newbies fiddling with recursion and IO to people that start to get used to monad transformers.

A lot of docs will get outdated if "Dependent" Haskell were to become "Standard" Haskell. But as @kcsongor pointed out

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.

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.

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" Type) and do what you want. No wondering if this () is a value, a type or a kind. It just is ().

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.

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.

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.
I still find the punning of type variables and normal values not good, particularly when it comes to documentation.
Even without dependent typing, I would not be against removing this punning.

Can anyone give concrete examples of how making dependent types more ergonomic, is going to make it harder for newcomers to learn Haskell?
What I'm seeing here is:

• Simplify scoping for type applications in patterns #291 - bring types into scope under certain conditions - if you're dealing with that you're not a newcomer and makes it behave more how you'd expect it to behave. (the default unscoped is kind of strange anyway).
• Support pun-free code #270 - warn when punning. Great idea, this is confusing anyway. Terms and types should be distinct. I believe this will make it easier to understand Haskell for newcomers.
• Visible forall in types of terms, and types in terms #281 - visible forall allows API's to be designed in such a way they produce nicer error messages. Again I believe this makes things easier.

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 Proxy and -XAllowAmbiguousTypes is nice and something that I would appreciate, but it is not very important to me personally. Having to provide a Proxy argument has never stopped me from doing something or changed the way I designed a piece of code because it would be too inconvenient. On the other hand, being able to get rid of some explicit singletons (and especially the large amount of boilerplate around them) would be a much more significant improvement that would actually change my calculations of where it is worth enforcing stronger invariants at the type level. My understanding is that we could have a singleton-free world with Dependent Haskell. I don't have strong feelings on many of the specific proposals that have been mentioned in this thread, but I am strongly aligned with the mission of improving the state of Dependent Haskell.

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:

• How will we know that we have arrived at Dependent Haskell?
• At a high level, what is the design we want to achieve?

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 -XDependentHaskell or something similar). Making this clearer and explicit might help clear up some of the arguments in play. From the proposals I see mentioned in this thread, the impact on users who are not opting in seems pretty minimal.

I have two questions:

• How will we know that we have arrived at Dependent Haskell?
• At a high level, what is the design we want to achieve?
  ...
  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 -XDependentHaskell or something similar). Making this clearer and explicit might help clear up some of the arguments in play.

+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."

I have two questions:

• How will we know that we have arrived at Dependent Haskell?
• At a high level, what is the design we want to achieve?

There's two ways to answer this at this:

1. We have full support for foreach ->
2. The "type level" and "term level" (really "relevant" and "irrelevant", due to already-existing work like data kinds) languages are the same.

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:

It is every expectation that proposals building dependently typed features would maintain backward compatibility.

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.

How will we know that we have arrived at Dependent Haskell?

I'd say that we have arrived when the singletons library becomes redundant.

At a high level, what is the design we want to achieve?

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

When in the history of [humans] did short term thinking prove to be the best strategy years later?

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.

I’m for breaking things to improve them as long as there’s a good plan for the transition.

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.

approachability

what is ergonomic for newbies/learners of a lazy functional language?

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.

I think #372 is a crucial prerequisite

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.

[worries about type erasure]

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 3 :: Nat used at compile-time really shouldn't be called a "type") fully user-specified. No heuristics. Haskell will keep type erasure.

I don't think [the worry about brain drain] is necessarily true.

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.

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

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.

How will we know that we have arrived at Dependent Haskell?

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 ::) is a solid step -- but it's actually one we could achieve without dependent types, just by doing an internal conversion from functions to type families. Writing replicate :: foreach (n :: Nat) -> a -> Vec n a without singletons would be another solid step -- but it's one we could achieve without fixing the namespacing challenges. So, in the end, it will really be a combination of a number of features.

At a high level, what is the design we want to achieve?

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 ' mark for promotion, but otherwise has stood the test of a little time. Proposals #102 and #236 are other stabs at defining this. (To be clear, while @int-index -- the author of #236 -- and I collaborate frequently, I don't fully endorse all of the suggestions in #236.)

There is a chance that new research around quantitative type theories (including my upcoming POPL paper) may change the suggested foreach syntax (because the distinction between foreach and forall should really be in the same bit of syntax as the difference between a linear arrow and an unrestricted arrow), but we haven't worked out the details.

Does this [proposal] imply that there should be no breaking changes whatsoever, or that we should try to minimize them and provide reasonable migration strategies?

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 forall and foreach to be keywords unconditionally to be able to parse a dependently typed Haskell. Making these into keywords would indeed be backward-incompatible. So I guess I mean the latter. I'll update the proposal.

And of course, the slogan from the main website should be changed to "An advanced, purely functional, dependently typed programming language".

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:

• Dependent Haskell is an implementation of Dependent Types as a (set of) GHC language extension(s)
• As such, it is (almost entirely) opt-in and people who want plain old Haskell 2010 get to keep it
• What does that mean to me, a user of Haskell?
  • Unification of types and terms (yay)
  • Eliminate the need for singletons in code that wants to prove more things at the type level (yay)
  • More expressive power in the type system when you want it
• Include the list of motivations in this proposal as examples of what Dependent Haskell will enable
• How does this instantiation of dependent types relate to the languages that started with support for dependent types or similar things?
  • We won't have things like termination proofs (I think?)
  • The expressivity is somewhat different than Liquid Haskell
• Critically, this is not a choice between Haskell and Dependent Haskell; you get to both have the cake and eat it on a per-module basis

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:

• Unify types and terms
• Concretely, eliminate the need for singletons

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.

@JakobBruenker I might be missing something, but if I'm understanding that proposal correctly, it's not actually necessary to enable RequiredTypeArguments at the call site of a function with a required type argument.

Hmm. I'm finding the proposal unclear wrt call sites. Is Section 4.1, esp. point 4, all presuming RequiredTypeArguments is set? If that flag is merely enabling forall a -> ... syntax in signatures and saying nothing about call sites? Then it seems misleadingly named. How to interpret this in point 4. first bullet:

• In expressions and patterns, ..., if only the type constructor is in scope, do not error and resolve the reference as a type constructor occurrence.

If that's to happen irrespective of RequiredTypeArguments (and note the renaming happens before the compiler knows if there's any functions expecting type arguments), it's already resolved wrong for non-DH'ers. The error reporting must not presume the caller intended to use a type constructor in a term. (But perhaps the author is a DH'er who did intend, and this module has no signatures, so they didn't set the flag? How is the error reporting to guess?)

You might be right: the following bullet says "Guard the data variable occurrences [in types] behind the RequiredTypeArguments, ..." suggesting the behaviour in expressions/patterns isn't so guarded. This is again the single flag conflating separate concerns: decl sites vs usage sites -- which aren't necessarily in the same module.

@int-index ... it falls apart quickly when you start considering other kinds. undefined :: Maybe is ill-kinded.

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 undefined clutter. A bare Maybe isn't a legitimate argument to sizeOf, typeOf.

If that's to happen irrespective of RequiredTypeArguments (and note the renaming happens before the compiler knows if there's any functions expecting type arguments), it's already resolved wrong for non-DH'ers. The error reporting must not presume the caller intended to use a type constructor in a term.

@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 Int is not in scope.

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 forall -> are separate concerns.

@AntC2

under Committee review purdah

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:

Lexical Scoping Principle (LSP). For every occurrence of an identifier, it is possible to uniquely identify its binding site, without involving the type system.

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

There are three namespaces, terms, types and kinds aka type-of-type (what appears after :: nested inside a type, also where you could put * before StarIsType).

I see only two namespaces. Kind syntax (when it was separate from type-syntax, pre-8.0) drew from the type-level namespace.

For some declarations/bindings of an identifier, it's possible to tell which namespace they belong to; but data constructors belong to both terms and types; type constructors belong to both types and kinds.

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.

For some usages of identifiers it is possible to identify which namespace it appears in, and therefore identify its binding site. Some usages are ambiguous, so there's the ' prefix to disambiguate.

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.

In some cases the compiler must invoke the type system (or perhaps I mean sometimes the compiler is too nervous/is in the wrong phase to consult type inference, makes a wrong guess so rejects with a type/kind error).

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 sizeOf to change in practice, but maybe to have an alternative type of sizeOf available, exported from a separate module. And, I'm convinced (and have been for some time) that GHC should be much more careful around suggesting extensions, something we will be careful to do as we go forward. This is precisely the kind of very helpful feedback we get through this proposals process.

BTW, whilst we're talking about lists and tuples and punning ...

Only a few months ago the libraries team added

data Solo a = Solo a

as the definitive GHC-prim-blesséd naming for singleton tuples. Will that be wrong with Dependent Haskell?

@AntC2

Will [data Solo a = Solo a] be wrong with Dependent Haskell?

Wrong? No. It will be a little awkward to work with, just like it's a little awkward to work with Data.Set, which exports functions named identically to those in the Prelude. Not very awkward, mind you, just a little.

BTW (2) I'm finding the eye slips too easily past the (type ...) herald. I'd prefer something that stands out more as saying 'here comes a type':

f (:: [Int])

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? 🤷🏻‍♂️