Given f :: forall a -> t, while x in f x is a type, it is parsed and renamed as a term, and then reinterpreted as a type

Seeing as, apparently, the only difference between forall a . and forall a -> is visibility, would it make sense to change f @x, given f :: forall a . t, to use this same parsing as term/reinterpreting as type procedure for x? It seems like this should improve consistency and reduce future maintenance burden (one process instead of two for type applications), while not being too much additional work to implement.

And some bikeshedding - while, in principle, I prefer the capitalization of -XVisibleForall, it is inconsistent with the already existing -XExplicitForAll.

Seeing as, apparently, the only difference between forall a . and forall a -> is visibility, would it make sense to change f @x, given f :: forall a . t, to use this same parsing as term/reinterpreting as type procedure for x?

Sounds reasonable, but this would be a breaking change. Consider:

data T = T

x = f @T

Which T is referenced here? Today it's the type constructor, but with updated rules it would be the data constructor.

The proposal says:

• Allow forall a -> blah in types, as proposed.
• For functions with such a type, require an explicit type argument

One way to meet "require an explicit type argument" is to write applications as f type, thus f Int or f (Mabybe Int). An obvious alterantive is to signal those type arugments, with their change of syntax and namespace, explicitly, thus f @Int or f !Int or something. It's worth pointing out that this is a possible choice and discussing the tradeoffs.

It's worth noting that, as proposed,

• one can parse expressions without knowing whether an argument is a type or a term, because the syntax of types and terms is united in big union.
• But one cannot rename an expression. For example

  f :: forall a. blah
  f a = g a
  

  In the argument to g, am I referring to f's value parameter a, or to the type variable a bound by the forall? We can't tell until we know the type of g`. That's a problem for the renamer.
• In the typechecker we finally know the types, so we can "reinterpret" the argument as a type if necessary.

we all agree that the term/type unification is The Right Thing.

I am open to that as a future possiblity but, as you know, I am not ready to commit to it. I'd like to accept or reject this propsoal on its own merits.

It's worth pointing out that this is a possible choice and discussing the tradeoffs.

I added this as an alternative and explained why I don't think it's a good one.

In the typechecker we finally know the types, so we can "reinterpret" the argument as a type if necessary.

To be clear, reinterpretation as proposed does not change how the names were resolved. That is, if a was referring to a term-level variable, it continues to do so, and ends up as a type error.

I am open to that as a future possiblity but, as you know, I am not ready to commit to it. I'd like to accept or reject this propsoal on its own merits.

This proposal is a step towards a destination, and if we disagree about the destination, I'm not sure we should invest time and effort into making this step. That is, I don't believe this proposal has a good power-to-weight ratio if we look at it in isolation. Looking at the motivation section, we have:

1. Language consistency (symmetry between terms and types)
2. Ability to design better APIs (good error messages, no proxy types, no ambiguous types)
3. Prepare the compiler internals for further work on dependent types

But:

Point 3 refers to pi-types, which will require term/type unification either way. Point 1 is about symmetry between terms and types, which means little if we do not seek to unify them. Point 2 alone is not sufficient to make this proposal worthwhile (in my opinion).

When VisibleForAll is in effect, lift the restriction that the forall a -> quantifier cannot be used in terms.

I just want to be careful about language here. forall a -> cannot, in this proposal, be used in terms. It can be used in types of terms. This happens in several places.

It is sad that the renaming of a visible dependent argument is different than that of a specified dependent argument. Maybe it is inevitable, but it's sad. If we imagine dependent Haskell, it will be a wart on the language. If we end up accepting this proposal as currently written, I would welcome a separate proposal (or maybe a rider on this one) that we add a warning to -Wcompat whenever a visible type application uses a name in scope at the term level, and then to move the warning to -W, and then switch the renaming, all in due course.

However, since we rename this as a term, we retain the fixities of term-level operators.

This doesn't seem right. Consider an argument x + y. If + is in scope as a term, then we can't reinterpret, as explained elsewhere. Otherwise, + must be in scope as a type and the phrase "fixities of term-level operators" does not make sense.

Do we need to make forall a keyword in terms? It seems possible to live without this, making forall a keyword only in types. If a forall is used in a visible dependent argument, we can just reinterpret the syntax.

Maybe it's s good idea to make forall a keyword everywhere, but I want to establish whether or not it's an essential part of this proposal.

Hence, by accepting this proposal, we all agree that the term/type unification is The Right Thing.

This section is almost worthy of its own proposal. With my GHC-committee hat on (leaving my Dependent-Types hat to the side), I'm very dubious of this. And I don't see it as essential here.

I understand that the proposal process is onerous, and I'm sympathetic to attempts to short-circuit it. Indeed, I support the suggestion you have here (as long as the changes are non-breaking -- fixing Symbol will be a breaking change, for example). But I still say it shouldn't be tied to this particular proposal.

Nice example.

I do not see a need for a new extension here. We have too many extensions! Just hook into ExplicitForAll. I expect others may disagree on this point.

We don't have a unified type/term parser yet, do we? This proposal is designed assuming that these parsers are mergeable. That may be true, but I don't yet have evidence of it. Is this simply impossible because of forall? (I doubt that.) I'm worried that, after we accept this proposal, we'll realize we have to make a subtle syntactic change in order to merge the parsers, and then we'll either have to retract this proposal or make some breaking change to the language.

On the other hand, it would seem a waste of effort to merge these parsers without the acceptance of this proposal, unless it served to reduce complexity in the parser and improve error messages.

I'm unsurprisingly in favor, in general.

It is worth noting that making forall a keyword at the term level by default will break a sizable chunk of code in the wild. A quick Hackage search reveals 53 top-level functions on Hackage named forall. (Ironically, one of those packages is Idris.)

I just want to be careful about language here. forall a -> cannot, in this proposal, be used in terms. It can be used in types of terms. This happens in several places.

Yes, "forall in terms" isn't quite right, I changed the language to "in types of terms".

It is sad that the renaming of a visible dependent argument is different than that of a specified dependent argument. Maybe it is inevitable, but it's sad. If we imagine dependent Haskell, it will be a wart on the language.

This is resolved by #270, no? With -Werror=punning, name resolution is the same in terms and types.

This doesn't seem right. Consider an argument x + y. If + is in scope as a term, then we can't reinterpret, as explained elsewhere. Otherwise, + must be in scope as a type and the phrase "fixities of term-level operators" does not make sense.

Right, I removed the part about fixities.

Maybe it's s good idea to make forall a keyword everywhere, but I want to establish whether or not it's an essential part of this proposal.

Assume we do not make forall a keyword and attempt reinterpretation. We parse x = f (forall a. a) as the . operator, and forall a as its LHS.

Before we get to type-checking (where reinterpretation should happen), we do name resolution. We end up trying to resolve . as an operator (which may fail), forall as an identifier (which may fail), and a as a variable (which is no longer bound). Not good.

The real question is not whether to make forall a keyword in terms, but whether to make it a keyword in terms only when ExplicitForAll is in effect. Implementation-wise, it would be easy to do it as long as that was what we did in types too. That is:

• it is easy to make forall a keyword only under -XExplicitForAll (as was the case before #193)
• it is easy to make forall a keyword, always (as is proposed here)
• it is not so easy to make forall a keyword in types always, and in terms only under -XExplicitForAll

Not to say that it's impossible, but it would require some fancy footwork. Every discrepancy between terms and types is a burden.

Indeed, I support the suggestion you have here (as long as the changes are non-breaking -- fixing Symbol will be a breaking change, for example).

I added "non-breaking" to clarify the intent.

But I still say it shouldn't be tied to this particular proposal.

The thought process behind this is that by introducing this reinterpretation business, we add a bit of ugly complexity, but at least we plan to get rid of it down the line. If we don't agree that we should be moving away from reinterpretation of terms as types, and towards unification of terms with types, then maybe we shouldn't be adding reinterpretation in the first place. It's scaffolding, not the final product.

I do not see a need for a new extension here.

I disagree, but not strongly. Added to alternatives, happy to do whatever the committee decides about this.

This proposal is designed assuming that these parsers are mergeable. That may be true, but I don't yet have evidence of it.

I'm happy to do go ahead and merge them, but before I do this, let's agree first that this is even a thing we want to do!

I'm worried that, after we accept this proposal, we'll realize we have to make a subtle syntactic change in order to merge the parsers, and then we'll either have to retract this proposal or make some breaking change to the language.

Sure, then we'll do either of these things:

• Retract this proposal
• Go through another proposal process for the required breaking changes

I only expect that we first agree that this is the direction we all want to go in, and so far @simonpj indicated that this is not necessarily the case.

A quick Hackage search reveals 53 top-level functions on Hackage named forall. (Ironically, one of those packages is Idris.)

The search query doesn't seem right to me, as the results include identifiers such as pforall, _forall, check_exists_forall, can_eq_nc_forall, ppr_forall, fresh_forall, etc. The actual amount should be smaller than 53, and even then, there will be a three-release (1.5 years) migration period.

we all agree that the term/type unification is The Right Thing.

No. Do not use the first person there. I think you mean the elite and increasingly exclusive brethren at GHC HQ want to unify terms/types. Fine. Suggest you stop calling the resulting language 'Haskell'.

@AntC2

elite and increasingly exclusive brethren at GHC HQ

I'll point out that both Simon and I have balked at the bit of the proposal you're criticizing here. I personally do think this is a good direction of travel, but I wouldn't presume to say that others do, too.

@int-index

Before we get to type-checking (where reinterpretation should happen), we do name resolution. We end up trying to resolve . as an operator (which may fail), forall as an identifier (which may fail), and a as a variable (which is no longer bound). Not good.

I'll point out that name lookup failures do not stop the compilation pipeline. They don't even induce warnings or errors! (It's trying to give them a type that produces the errors.) So I still claim that this is possible. Maybe not preferable, but possible.

[Difference between name lookup in required arguments and specified arguments] is resolved by #270, no?

Not quite. While -Werror=punning does make the problem go away, nowhere do we have a plan to put -Wpunning even in -W, much less make it a hard error. One might argue that anyone using dependent Haskell is well-advised to do so, but it would still be a strangeness in the language.

@goldfirere I'll point out that both Simon and I have balked at the bit of the proposal you're criticizing here.

Thank you Richard, I apologise my intemperate language was a (visceral) reaction against @int-index's high-handed presumption. If there's some merit to unifying types/terms, Vladislav needs to carry everybody with him by persuading and demonstrating how it supports better programming (for some value of 'better').

We've always had unified syntax for type construction and data construction; and somewhat similar for pattern matching (if we allow class and TF instances as type-level patterns). That doesn't persuade me we have or need unified semantics; because ...

GHC Haskell (even more than Hugs Haskell) is a multi-module compiled language. There's a phase distinction between the semantics at compile time (type inference) vs execution time. Needing to support multi-module (where the compiler can't know what other modules this might get imported into) puts a hard block on what can happen when.

I think it's important users of Haskell understand that distinction. Even if the language tries to unify types/terms, that distinction will 'grin through' the abstraction.

To @AntC2,

No. Do not use the first person there. I think you mean the elite and increasingly exclusive brethren at GHC HQ want to unify terms/types.

In this particular sentence, "we" refers to everyone involved in the discussion. I see that you disagree – alright, then it's up to me to improve the Motivation section until that phrase, "we all agree that the term/type unification is The Right Thing", becomes true.

Note how it is prefixed by "by accepting this proposal". Let's not accept it until we reach consensus.

Even if the language tries to unify types/terms, that distinction will 'grin through' the abstraction.

I'm afraid this argument went over my head. There are other multi-module compiled languages, which are dependently typed and use the same language for types and terms. Could you demonstrate how this distinction grins through the abstraction in those languages, using the one most familiar to you? (I'll make the effort to understand the example whatever language you pick, but I'm most familiar with Agda/Coq/Idris)

To @goldfirere,

I'll point out that name lookup failures do not stop the compilation pipeline. They don't even induce warnings or errors! (It's trying to give them a type that produces the errors.) So I still claim that this is possible. Maybe not preferable, but possible.

That's something I didn't realize. I think there are other ways this hack may fail. For example:

infix 9 %
x = f (forall a. T a % G x)

This results in an error before the type checker:

    Precedence parsing error
        cannot mix ‘.’ [infixr 9] and ‘%’ [infix 9] in the same infix expression

In general, I'm very wary of reinterpreting syntactic constructs. Parsing forall a. t with . as an infix operator is exactly the sort of thing that sets off an alarm in my head. Another one was parsing bang patterns f !x = ... as infix operators, which led to #1087 and #17162. Fixing this required the proposal #229, which I'm still implementing (there's a prototype, !1664).

So, why would we add new faulty code like this, while firefighting its consequences in other places? The reason reinterpretation as described in this proposal isn't that bad is that there are direct equivalences between the reinterpreted constructs:

1. HsLit becomes HsTyLit
2. HsVar becomes HsTyVar
3. HsApp becomes HsTyApp
4. OpApp becomes HsOpTy

... and so on. The reinterpretation of terms as types is direct. My hope is that in the end, we can fully unify them, removing the need even for a direct reinterpretation. On the other hand, parsing forall a. t as OpApp and then reinterpreting it as HsForAllTy rather than HsOpTy is just the sort of thing that can't end well.

While -Werror=punning does make the problem go away, nowhere do we have a plan to put -Wpunning even in -W, much less make it a hard error. One might argue that anyone using dependent Haskell is well-advised to do so, but it would still be a strangeness in the language.

What if -XVisibleForAll implies -Werror=punning, would that work?

Even if the language tries to unify types/terms, that distinction will 'grin through' the abstraction.

There are other multi-module compiled languages, which are dependently typed ...

There you go again making a high-handed presumption (in fact much the same presumption) that Haskell must become a dependently-typed language. It's a lot less than clear how we get there from a language whose typing theory was originally based on Damas-Hindley-Milner. It's an open research question whether such a migration is possible without breaking too much. My guess is it's hard; and that you might end up with a language that is 'based on Haskell' but is not Haskell.

You need to not only improve the Motivation section here, but the Motivation for each step along the journey. There's currently no roadmap. Section 4 Meta is not a roadmap, it reads more like handing over the hen-house to the fox. (This is my favourite language you're messing with. Already the fluffy chicks I first knew have become cantankerous broilers.)

Could you demonstrate how this distinction grins through

It's already grinning through in a small way. With promoted DataKinds there's occasionally ambiguity within types as to whether some name (eg Bool) denotes a type or a promoted type-of-type, thus needing the ' prefix. Haskell was not originally designed for Dependent typing; it was designed with separate namespaces for type-level vs term-level (and no namespace for type-of-type level). So with no risk of ambiguity, punning type names as term names is ubiquitous. So within the syntax for terms there's always clear syntactic demarcation that types appear only to the right of :: (or within the scope of @). That syntactic demarcation is a valuable analogue of the phase distinction. In

ghci> rgb "red"
ghci> Foo Foo Bar Bar

(And of course real-life terms will be more complex) I'm seeing "red", Foo, Bar as term-level. You're ushering me into a world of fear, uncertainty and doubt for any term: which are the types, which are the terms? If the first Foo is a data constructor, the second could be a type, the Bars could also be one of each.

To understand the semantics I need to bear in mind: terms are evaluated left-to-right by Beta-reduction; types are solved Outside-In by unification. (Yes that's a gross simplification.)

[languages that] use the same language for types and terms.

Those languages designed from the ground up for Dependent Typing: do they support punning type-names as term-level names; and punning term-level literals as types?

the abstraction in those languages, using the one most familiar to you? (I'll make the effort to understand the example whatever language you pick, but I'm most familiar with Agda/Coq/Idris)

Coq is a theorem-prover not comparable to Haskell; Agda/Idris are as much theorem-provers/proof assistants as programming languages. I don't see any of them as achieving the industrial-strength optimised object code that Haskell achieves.

And thank you for the invitation, but no I'm not going to enter into some language war. As @simonpj already said "I'd like to accept or reject this propsoal on its own merits." The argument you're making implicitly 'This proposal moves Haskell closer to Coq/Agda/Idris' does not give any merits.

(@int-index you might want to edit the PR name and description to "in types of terms" as well?)

2. Ability to design better APIs (good error messages, no proxy types, no ambiguous types)
   Point 2 alone is not sufficient to make this proposal worthwhile (in my opinion).

I want to add that point 2 is enough for me to consider this proposal useful and worthy to be implemented. It opens a possibility to improve the UX of Haskell users which I value a lot (and I think we all should care about improving Haskell UX for beginners, but that's just my opinion). Haskell has a reputation for being non-beginner-friendly and with this feature, developers can implement better libraries. Below I'm going to provide a few examples from production usage of Haskell where I can find this feature useful.

1. Better show. Sometimes I use show to format custom values. And sometimes people silently update their dependencies and my code breaks (which also can sometimes be quite painful to debug if maintainers don't update CHANGELOG properly and don't write proper migration guides). So in some cases, I want to require explicit type annotations. The following function solves this problem:

   show :: forall a -> Show a => a -> String

2. Sometimes I call length on various containers data types. And sometimes I refactor code changing types from [a] to Maybe [a] or [a] to (Int, a). Since length works for any Foldable, the code after such refactoring still compiles, but it contains an invisible error that can lead to some serious hard-to-find bugs later (we had this happening, and we spent 2 days to find this bug). I agree that this is a general problem with such polymorphic code and with Foldable the proposed solution doesn't work if you change [a] to [[a]]. However, the solution might not be perfect it's is still extremely useful.

   length :: forall a. forall f -> Foldable f => f a -> Int

3. In our code, we have the Id newtype with a phantom type parameter. And we also have castId function that changes this tag. It would be much nicer to be able to force users of this function to specify type argument of result to make code more readable and not break it accidentally when you change Id User to Id Admin.

   newtype Id a = Id { unId :: UUID }
   
   type AnyId = Id ()
   
   castId :: forall from . forall to -> Id from -> Id to

4. We're using proto-lens library by Goole which implements Protocol Buffers data type and codecs generation in Haskell. In this library you need to use a polymorphic variable defMessage :: Message a => a to construct data types. However, we want to specify the type argument of this defMessage explicitly not to break code accidentally and make the refactoring easier and improve code readability. So we want the following functions:

   defMessage :: forall a -> Message a => a

As you can see from my examples, I often want to be able to force users to specify the type of argument explicitly. It's often useful that with forall x. type is inferred automatically for you, but sometimes you want to the specify the type explicitly. I believe that it's possible to solve this problem differently, with some external tools or enforcing guidelines (which is fragile) or some ad-hoc mechanism for this specific case. But at least the solution with visible forall in terms seems sane and elegant enough for this problem.

@goldfirere

Not quite. While -Werror=punning does make the problem go away, nowhere do we have a plan to put -Wpunning even in -W, much less make it a hard error. One might argue that anyone using dependent Haskell is well-advised to do so, but it would still be a strangeness in the language.

I think this is good enough. I am fine with people using multiple namespaces thinking of @arg as a "type thing", and plain arg as a "term thing". The beauty of @ being just about visibility and orthogonal to everything else is the same beauty as using the same parser and namespace for both types and terms. If the user isn't drawn to the aesthetics of one of those, they probably aren't drawn to the other, either.

As to the eventual goals discussion, I think it's important to remember that these are ghc-proposals not haskell-proposals. I am fine rebranding "Dependent Haskell" as, I dunno, "Alonzo", if we agree that GHC should support both and they should freely interoperate type safely.

Now, when this proposal says

Hence, by accepting this proposal, we all agree that the term/type unification is The Right Thing

We should understand not as

Hence, by accepting this proposal, we all agree that the term/type unification is The Right Thing for Haskell.

but as:

Hence, by accepting this proposal, we all agree that the term/type unification is The Right Thing for GHC's core, in order to support future language research for Haskell or other interoperable languages.

I think that's hard to argue against. The people working on GHC which to research these things. This proposal is inarguably a good step in service of that goal. Haskell 98 remains Haskell 98. What's the problem?

@chshersh improve the UX of Haskell users which I value a lot (and I think we all should care about improving Haskell UX for beginners, but that's just my opinion). Haskell has a reputation for being non-beginner-friendly

Yes where I'm coming from is the UX. For beginners we used to offer an easier experience, with the mind-twisting bits hidden away behind extensions.

Then I'm very puzzled by @chshersh's comment. Haskell 98, and even including common extensions such as MPTCs is user friendly. What has made GHC Haskell non-beginner-friendly is that it's increasingly difficult to hide the mind-twisting bits. I see this proposal as one more twist.

and with this feature, developers can implement better libraries.

Well yes maybe (for some value of 'better'). The examples you give of better libraries: do you expect beginners to use them, with explicit type application? And without some syntactic marking that types are appearing in terms? That seems to me the opposite of beginner-friendly. To remind, the story we give to beginners is:

1. Recommend giving signatures for your functions, as machine checked documentation and sanity check over both the equations for those functions and the usage sites. Having done that ...
2. The power of type inference (Hindley-Milner) means you can write higher-order functions and partial applications and use library-supplied highly abstract combinators, without having to hand-thread the types through them.
3. That is, beginners rarely need type annotations in terms nor explicit type applications.

Unfortunately GHC is currently failing at point 1. If you write a dodgy signature (which beginners are very prone to), GHC rather than saying that's probably not what you meant, recommends you switch on AllowAmbiguousTypes; then you slide down a few rabbit-holes and find you need ExplicitApplication -- i.e. at point 3 where beginners should not be. Absolutely not beginner-friendly when the problem was the original signature. There's a proposal to avoid that -- motivated precisely by the large amount of beginner-confusion.

@Ericson2314 the term/type unification is The Right Thing for GHC's core,

I have no view on that. Remember GHC's core is not Haskell, and has always had explicit type application; that's compulsory explicit-type-application-everywhere. Remember that GHC core is type-checked; but has no type improvement/type inference mechanisms. That's OK as an intermediate language whose type applications are generated mechanically. Nobody writes core by hand do they? That would be like bit-aligning and byte/word-aligning data layouts by hand.

For some features from core, it has been useful to expose them in surface Haskell. Compulsory explicit-type-application-everywhere is not one of those features. I (for one) don't expect beginners to look at core; I don't expect they'll know that core has explicit type application; I do position Haskell for beginners as a High Level Language which to a large extent looks after the types for itself. If you enjoy burdening your code with type-management, C is a fine language.

@AntC2 With all due respect, please knock it off. Virtually nothing you've written on this thread pertains to this specific proposal. It's all general grousing about the direction of GHC.

Let's be clear: I've been to many talks by Richard and others on the work being done to bring dependent types to haskell. Invariably, the first question, to significant applause, is "how soon can we get it?" So yes, there is great demand for this, and there are many proposals pertaining to it.

If you don't like that direction -- go find a better venue to convince people otherwise. Write to a mailing list, write a blog post. Complain on reddit.

But derailing specific proposals over your complaints about a general direction that many people, with much support, are working towards -- that's not appropriate, and I wish you would stop.

To @glaebhoerl,

you might want to edit the PR name and description to "in types of terms" as well?

Yes, thank you. Fixed it.

To @chshersh,

Thank you for all the examples. I'm not sure what would be a good way to incorporate them into the proposal, as it is a matter of judgement whether to use visible or invisible forall there. After all, there are no ambiguous variables in those examples.

But it's still valuable to see these examples in the discussion, and to know that visible forall could be used to improve APIs, even if the improvement is subjective.

To @AntC2,

There you go again making a high-handed presumption (in fact much the same presumption) that Haskell must become a dependently-typed language.

I'm rather of the opinion that Haskell should provide an option of dependent typing, as I find it immensely useful, but it's up to the programmer whether to make use of dependent types.

What has made GHC Haskell non-beginner-friendly is that it's increasingly difficult to hide the mind-twisting bits. I see this proposal as one more twist.

The proposed change is hidden behind an extension, VisibleForAll. Haskell2010 remains as is. Same goes for the extended clause about term/type unification: it would not affect the standard language.

With promoted DataKinds there's occasionally ambiguity within types as to whether some name (eg Bool) denotes a type or a promoted type-of-type, thus needing the ' prefix. Haskell was not originally designed for Dependent typing; it was designed with separate namespaces for type-level vs term-level (and no namespace for type-of-type level). So with no risk of ambiguity, punning type names as term names is ubiquitous.

Let's put dependent types aside for the moment.

As far as I understand your arguments, you care a lot about making Haskell beginner-friendly (so do I). But then, the consistent thing would be to become a proponent of term/type unification and getting rid of punning. In my teaching experience, it's difficult for beginners to keep track of the current context, and to realize that [a] may mean either a singleton list with the element a, or the type of lists where each element has type a.

So, even without dependent types, using a single language for terms and types, and eschewing punning, would be a win.

1. Recommend giving signatures for your functions, as machine checked documentation and sanity check over both the equations for those functions and the usage sites.
   Unfortunately GHC is currently failing at point 1.

With all the extensions that were added to GHC, the inference is not any worse as long as you do not enable them. So I don't think that GHC is failing here, its inference engine is a blazing success.

I do position Haskell for beginners as a High Level Language which to a large extent looks after the types for itself. If you enjoy burdening your code with type-management, C is a fine language.

I'm afraid there are differences between C and Haskell other than the amount of required type annotations.

And thank you for the invitation, but no I'm not going to enter into some language war.

This was not an invitation for a language war, but an attempt to understand your point of view on the matter. As far as I can tell, the argument goes like this:

1. Haskell is a multi-module compiled language
2. In such a language, there is a phase distinction between terms and types
3. Therefore, any attempt to unify terms/types is a leaky abstraction

I don't believe we can jump from (2) to (3), and the existence of other multi-module compiled languages with dependent types is evidence that I used to back up the claim that, in fact, term/type unification is a very reasonable thing to have in a multi-module compiled language such as Haskell.

But of course I'm always considering the possibility that I'm wrong, so I asked you to compromise my evidence, so that I could change my view and we'd end up on the same page.

The goal of this argument is to arrive at the consensus, is it not?

Just to reiterate, I think the following holds true:

1. I care about industrial applications of dependent types, but you do not. (That's fine!)
2. We both care about beginner experience with Haskell. (Very good, we agree here)
3. You believe term/type unification and dependent types would be detrimental to beginners' experience (I disagree, but it doesn't matter because...)
4. The proposed features are to be hidden behind extension flags, and GHC continues to support the Haskell dialect that you cherish (lacking dependent types).

Or, as @Ericson2314 puts it:

This proposal is inarguably a good step in service of that goal. Haskell 98 remains Haskell 98. What's the problem?

Finally, to @gbaz,

With all due respect, please knock it off. <...> If you don't like that direction -- go find a better venue to convince people otherwise.

I appreciate the fervor of your comment, but I think this venue is perfectly fine. We are discussing an addition to Haskell, and, furthermore, a new policy about future additions!

I like to believe that @AntC2 argues in good faith, trying to do the best for Haskell. Except we don't quite agree on what would be best.

It is true that Haskell 2010 is a different spot in the design space than Dependent Haskell. It has name punning, it has better inference at the expense of other features.

@AntC2 enjoys this spot in the design space and tries to protect it from the invasive changes, motivated by dependent types, that threaten it. And it's a noble thing to do that. I like Haskell 2010 as well.

But! I don't believe we are threatening it. The reason Dependent Haskell isn't a new language but an extension of Haskell is that it's designed to have perfect interoperability with Haskell 2010. GHC will continue to implement Haskell 2010, and the new features are to be hidden behind extension flags as appropriate.

I would much prefer that @AntC2 and the dependent types crowd (of which I'm a vocal member) would realize that we don't need to be at odds with each other. And we should not exclude anyone from the conversation.

I often want to be able to force users to specify the type of argument explicitly

Regarding the proposal as it stands (rather than as a pathway to something more ambitious), this ability to specify a compulsory type argument looks like the main benefit. And I agree that it is a benefit, and it's one that is quite independent of the full-spectrum dependency issue. The question is: how much does this benefit cost.

The main cost is resolving the syntactic and name-space difference between types and terms. On obvious way of resolving that is via a syntactic marker. We already have one, namely @. So we could use @ for those compulsory type arguments too. This would be simple to explain, and require none of this re-interpretation. But it would occasionally be inconvenient. For example, if f :: forall k. forall (a:k) -> blah, then you could not write f @Int; you'd have to write f @_ @Int. Or change the type of f to f :: forall {k}. forall (a:k) -> blah.

@simonpj I added this as another alternative. Unsurprisingly, I'm not enamored with it either, as the primary motivation for me is to blur the distinction between terms and types, not to make it stand out with a syntactic marker.

@int-index I would to add to that alternative that even without of dependent types we may want want invisible relevant non-dependent quantification (that is to say, @ for terms). Now using one sigal for visibility and namespacing bights us even harder--no terms are in scope!

I hate to be negative, but I personally would rather do away with this proposal than to require the @ sign for required arguments. You might -- just barely -- be able to convince me to use some other syntactic marker, but requiring @ seems a step in the wrong direction.

I personally would rather do away with this proposal than to require the @ sign for required arguments

OK. Would you like to say why it seems like a step in the wrong direction?

Would you like to say why it seems like a step in the wrong direction?

It moves us away from uniformity. Let's even pretend for a moment that I'm not trying to actually merge the term-level and type-level.

Right now, we can say this:

type VDQ :: forall k1. forall k2 -> k1 -> k2 -> Type
data VDQ k2 a b

type VDQIntTrue = VDQ @Type Bool Int True
type VDQCharFalse = VDQ Bool Char False

If we were to require the @ in terms, the term-level equivalent would be

vid :: forall a. forall b -> a -> b -> ()
vid _ _ _ = ()

ex1 = vid @Int @Bool 3 True
ex2 = vid @_ @Bool 'x' False

These look different! Why different syntaxes for the same idea?

Worse, imagine a data constructor:

data Silly a b where
  Mk :: forall a. forall b -> a -> b -> Silly a b

Now we have this oddity:

type Different1 = Mk @Nat Bool 3 True
type Different2 = Mk Bool "hi" False
different3 = Mk @Int @Bool 3 True
different4 = Mk @_ @Bool "hi" False

Here, the right-hand sides should be the same, but they have to be different.

Today, we have non-uniformity by omission: we have no visible forall in types of terms. But with your proposed @ on required dependent arguments, we would have active non-uniformity, which seems worse as it paints us into a corner that's difficult to escape from. At least non-uniformity by omission can, in theory, be fixed uniformly, later.

I pushed an updated version of the proposal. Let me know if this is what you had in mind.

Thank you Vlad for your re-working. The 'phase distinction' from introducing the type herald to writing bare types in terms helps a lot in understanding the motivation. (My understanding it better doesn't mean I like it any better, but I can be clearer what it is I don't like. That ship has sailed.)

👋 @goldfirere, check on the committee .

The committee discussion has been generally in favor. @simonmar expressed some hesitance once upon a time and has not updated his vote. I've sent another email to the committee, but plan on accepting this on Friday if there is no further response.

/remind me to accept on Friday.

@goldfirere set a reminder for Oct 29th 2021

👋 @goldfirere, accept .

What's the status here, @goldfirere?

This proposal is now accepted. Thanks, all!

The (type ..) signifier presents a syntactic way to extend the data declaraton syntax with forall->

data Proxy (type k) (a :: k) = MkProxy (type k) (type (a :: k))

type Proxy :: forall (k :: Type) -> k -> Type
data Proxy (type k) a where
  MkProxy :: forall (k :: Type) -> forall (a :: k) -> Proxy (type k) a

Interesting observation, but I don’t think it works out. The type signifier is there to switch from term syntax to type syntax, but in the positions you’ve shown, we are already in type syntax.

So your declaration

data Proxy (type k) (a :: k) = MkProxy (type k) (type (a :: k))

is not supported by the proposed syntax (the type signifier is not allowed in these positions). But even if we allowed it, its meaning would’ve been a no-op, since we’re already in type syntax:

data Proxy k (a :: k) = MkProxy k (a :: k)

Thus you’d simply get an error:

    • Expected a type, but ‘a :: k’ has kind ‘k’
      ‘k’ is a rigid type variable bound by
        the data constructor ‘MkProxy’
        at <interactive>:6:22
    • In the type ‘(a :: k)’
      In the definition of data constructor ‘MkProxy’
      In the data declaration for ‘Proxy’