I've always been somewhat confused by the visible/invisible distinction, so I guess @ is a namespace override in my mind. There's another aspect of confusion around @ that came up in proposal #291, which Simon just brought up again. Is @ syntax for application or binding? Originally it was just application, then I believe we allowed it to bind existentials alone, and now there's work underway to allow it to bind any type variable in patterns. But reusing the same syntax for application and binding raises hairy questions like the one we're facing now in #291. On Fri, Nov 13, 2020, at 09:10, Spiwack, Arnaud wrote:

Dear all,

There is a debate which has been held in our heads for quite some time now. But we’ve never really had the conversation. This debate has been raised again in the context of proposal #281. But I’d rather make a separate thread about it.

The question is the following:

When I write

`f @t ` Am I using `@` as a way to change an invisible argument into a visible argument? Or am I using `@` to insert a type expression into a term expression?

The truth is that it’s doing both at the same time. So some of us have taken to believing that the One True Meaning™ of `@` is to override (in)visibility. While others have taken to believing that the One True Meaning™ of `@` is to insert types in term.

And, in both cases, we believe the other part to be incidental.

In favour of types-in-term, there is the pretty-printer for Core, which, if I’m not mistaken, uses `@t` to denote type applications (and all type applications are visible in Core, so there is no visibility override to be had).

Whatever we think about this, it appears that the fact that this meaning ascription is implicit has caused some anguish. So I think that we should have this discussion explicitly for once.

I chose to do so in a different thread than the #281 discussion, because this discussion stands on its own.

Anyway, the floor is yours.

/Arnaud

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

I haven't followed this debate, but the main question I have is: what are the implications of choosing one view over the other? Cheers SImon On Fri, 13 Nov 2020 at 14:10, Spiwack, Arnaud wrote:

Dear all,

There is a debate which has been held in our heads for quite some time now. But we’ve never really had the conversation. This debate has been raised again in the context of proposal #281. But I’d rather make a separate thread about it.

The question is the following:

When I write

f @t

Am I using @ as a way to change an invisible argument into a visible argument? Or am I using @ to insert a type expression into a term expression? ------------------------------

The truth is that it’s doing both at the same time. So some of us have taken to believing that the One True Meaning™ of @ is to override (in)visibility. While others have taken to believing that the One True Meaning™ of @ is to insert types in term.

And, in both cases, we believe the other part to be incidental.

In favour of types-in-term, there is the pretty-printer for Core, which, if I’m not mistaken, uses @t to denote type applications (and all type applications are visible in Core, so there is no visibility override to be had).

Whatever we think about this, it appears that the fact that this meaning ascription is implicit has caused some anguish. So I think that we should have this discussion explicitly for once.

I chose to do so in a different thread than the #281 discussion, because this discussion stands on its own.

Anyway, the floor is yours.

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