1. We need visibility specifiers: otherwise, we'd have no way of knowing which arguments were original invisible and which weren't.

Example: `f x y` vs `f (%ThisWasAnInvisibleArgument x) y` (where I've used an obviously brainless strawman syntax... though a shorter modifier is not as obviously brainless). In the second version, y is the first declared-visible argument.

2. We would like some type arguments to be visible and some to be invisible. This is the nub of the motivation for #281.

3. We thus need at least two ways of passing type arguments: one for declared-invisible ones (this is -XTypeApplications since GHC 8.0) and one for declared-visible ones (this is the new part).

4. The Syntactic Unification Principle of #378 tells us that the way of passing declared-visible types must be the same as the way of passing declared-visible terms (that is, ordinary function arguments). Thus, the way of passing declared-visible types must be by just writing the type in an argument position.

Note that we do not have declared-invisible term arguments (ignoring class dictionaries, which operate via quite a separate mechanism).

5. Because of punning (that is, the use of the same name in the term-level and type-level namespaces), a bare type argument might be misinterpreted. (For example, we might want the type T, not its data constructor T.) We thus need a way of stating that we request an identifier from the type-level namespace. The proposal includes the `type` syntax to do this.

I consider the `type` syntax from the proposal a disambiguation mechanism used as part of visible type application, not really a new way of passing types... though users may well think of it as a third way of passing types, so your point that 3 is too many stands.

The good news is that, absent punning, there is no need for the `type` syntax from this proposal. Alternatively, there is nothing stopping a user from writing `type` at *every* visible type application, if they so choose.

Does this help motivate the current design?

On Oct 29, 2021, at 11:49 AM, Eric Seidel <eric@seidel.io> wrote:

I suppose we could use the GHC20XX standards as a way to slowly course-correct.

1. Introduce -X@MeansTypeNamespaceOnly
2. Enable -X@MeansTypeNamespaceOnly as part of GHC2022
3. Let the ecosystem slowly adopt the change as they move to newer language standards

But I think there would still be more questions to answer.

1. What becomes the new syntax for visibility specifiers? (I think Agda and Idris use {}?)
2. Do we really need visibility specifiers? (I wish the answer were no, but I think it's yes.)
3. If we do need visibility specifiers, do I then have to write `f {@Int}` to specify an invisible type argument? That's gross.

So I'm netting out in the same place as Arnaud, somewhat uncomfortable with the proposal, but unable to come up with a better idea that doesn't compromise on expressiveness. I really do wish we could avoid the three ways to specify type arguments, but it seems like they're all necessary for different reasons..

On Fri, Oct 29, 2021, at 11:35, Spiwack, Arnaud wrote:
On Fri, Oct 29, 2021 at 5:16 PM Eric Seidel <eric@seidel.io> wrote:
In my mind the use of '@' as a visibility specifier is the inconsistency, as '@' has been the symbol for type application both in Core and Haskell for much longer than it has been used as a visibility specifier.

I agree with this. But how would you fix the current situation? `@` is
used as a visibility specifier in the user language (well, it switches
both visibility and grammar/namespace). If `@` is to switch only
grammar/namespace, what do we make of all the `@` that have been
written in the past half-dozen years?

/Arnaud
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee