<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Here's my take:<div class=""><br class=""></div><div class="">1. We need visibility specifiers: otherwise, we'd have no way of knowing which arguments were original invisible and which weren't.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">2. We would like some type arguments to be visible and some to be invisible. This is the nub of the motivation for #281.</div><div class=""><br class=""></div><div class="">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).</div><div class=""><br class=""></div><div class="">4. The <a href="https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-dependent-type-design.rst#syntactic-unification" class="">Syntactic Unification Principle</a> 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.</div><div class=""><br class=""></div><div class="">Note that we do not have declared-invisible term arguments (ignoring class dictionaries, which operate via quite a separate mechanism).</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">----------------</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">----------------</div><div class=""><br class=""></div><div class="">Does this help motivate the current design?</div><div class=""><br class=""></div><div class="">Richard</div><div class=""><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Oct 29, 2021, at 11:49 AM, Eric Seidel <<a href="mailto:eric@seidel.io" class="">eric@seidel.io</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">I suppose we could use the GHC20XX standards as a way to slowly course-correct.<br class=""><br class="">1. Introduce -X@MeansTypeNamespaceOnly<br class="">2. Enable -X@MeansTypeNamespaceOnly as part of GHC2022<br class="">3. Let the ecosystem slowly adopt the change as they move to newer language standards<br class=""><br class="">But I think there would still be more questions to answer.<br class=""><br class="">1. What becomes the new syntax for visibility specifiers? (I think Agda and Idris use {}?)<br class="">2. Do we really need visibility specifiers? (I wish the answer were no, but I think it's yes.)<br class="">3. If we do need visibility specifiers, do I then have to write `f {@Int}` to specify an invisible type argument? That's gross.<br class=""><br class="">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..<br class=""><br class="">On Fri, Oct 29, 2021, at 11:35, Spiwack, Arnaud wrote:<br class=""><blockquote type="cite" class="">On Fri, Oct 29, 2021 at 5:16 PM Eric Seidel <<a href="mailto:eric@seidel.io" class="">eric@seidel.io</a>> wrote:<br class=""><blockquote type="cite" class="">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.<br class=""></blockquote><br class="">I agree with this. But how would you fix the current situation? `@` is <br class="">used as a visibility specifier in the user language (well, it switches <br class="">both visibility and grammar/namespace). If `@` is to switch only <br class="">grammar/namespace, what do we make of all the `@` that have been <br class="">written in the past half-dozen years?<br class=""><br class="">/Arnaud<br class=""></blockquote>_______________________________________________<br class="">ghc-steering-committee mailing list<br class=""><a href="mailto:ghc-steering-committee@haskell.org" class="">ghc-steering-committee@haskell.org</a><br class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee<br class=""></div></div></blockquote></div><br class=""></div></div></body></html>