[ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept

[Richard Eisenberg]

Here's my take:

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 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-dependent-type-design.rst#syntactic-unification> 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?

Richard

> On Oct 29, 2021, at 11:49 AM, Eric Seidel <eric at seidel.io> wrote:
> 
> I suppose we could use the GHC20XX standards as a way to slowly course-correct.
> 
> 1. Introduce -X at MeansTypeNamespaceOnly
> 2. Enable -X at 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 at 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 at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20211029/0d10ed2a/attachment-0001.html>