<div dir="ltr"><div>As a user I usually need to know whether I'm looking at a type or a term in the code. For doing renaming in your head, it makes a difference whether you're looking at a type or a term: the namespaces are different.</div><div><br></div><div>Is it reasonable for that to apply to visible type application too? That is, are we assuming that the user knows they're looking at a type, or are we assuming that the user "shouldn't need to care", or something else? I ask this question because, if we believe that the user should know when they're looking at a type, then it's reasonable to interpret types differently from terms even when they appear naked in the term context, as they do with visible type application.</div><div><br></div><div>What could we do if we were allowed to treat types differently? Well, we already do various bits of magic in T2T. But we could also use different name resolution rules. That doesn't necessarily mean we have to defer renaming until during type checking: we could resolve each name twice, once for the term context and once for the type context, and then pick one of these later when we apply the T2T mapping. (earlier Vlad objected to this idea on the grounds that it might introduce spurious recursive dependencies, though).</div><div><br></div><div>Cheers</div><div>Simon<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, 2 Jun 2021 at 11:02, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="overflow-wrap: break-word;" lang="EN-GB">
<div class="gmail-m_-2296057027449592794WordSection1">
<p class="MsoNormal" style="margin-left:36pt">Intuitively it doesn't seem unreasonable to add a little more magic to the T2T mapping to preserve what (to me) seem to be reasonable expectations<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Yes, that was my view to begin with. But I can’t come up with any magic!<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">I cleave strongly to the view that given a name like T, I should be able to say what T is meant (the data constructor or the type constructor) without knowing the type of the function applied to T, as in (f T). That is, the renamer can
do its work without thinking about types. This is the Lexical Scoping Principle (LSP).<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Although the LSM makes GHC’s implementation much cleaner, it is not driven by implementation considerations. it’s to do with user understanding. What if that T isn’t the argument to a function, but appears in some other context? What
if `f` is polymorphic, so its type in turn depends on its context? It goes on and on.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">So, if we espouse the LSP and see (f T), we can only say that T is the data constructor. If you want the type constructor you can say (f (type T)). This tension seems fundamental, not driven by implementation considerations, nor by back-compat
constraints, nor by GHC’s history. There is no room for magic!<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">You might wonder if we could do some magic for built-in syntax like [T]. But it would be terribly strange to treat (f [T]) completely differently from (f [T,T]), say.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">The only way I can see to add magic is to give up on the LSP. But I really think that would be a Bad Thing. Indeed we recently removed the only bit of GHC that didn’t obey the LSP:
<a href="https://github.com/adamgundry/ghc-proposals/blob/no-ambiguous-selectors/proposals/0000-no-ambiguous-field-access.rst" target="_blank">
https://github.com/adamgundry/ghc-proposals/blob/no-ambiguous-selectors/proposals/0000-no-ambiguous-field-access.rst</a><u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">If you have any other ideas, I’m all ears.<u></u><u></u></p>
<p class="MsoNormal"><br>
Simon<u></u><u></u></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border-color:currentcolor currentcolor currentcolor blue;border-style:none none none solid;border-width:medium medium medium 1.5pt;padding:0cm 0cm 0cm 4pt">
<div>
<div style="border-color:rgb(225,225,225) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> Simon Marlow <<a href="mailto:marlowsd@gmail.com" target="_blank">marlowsd@gmail.com</a>>
<br>
<b>Sent:</b> 02 June 2021 10:06<br>
<b>To:</b> Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>><br>
<b>Cc:</b> Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank">rae@richarde.dev</a>>; ghc-steering-committee <<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a>><br>
<b>Subject:</b> Re: [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept<u></u><u></u></span></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
Thanks Richard and Simon - I think I understand the constraints better now. I still find the conclusion somewhat unsatisfying, and I'm not sure I could convincingly explain to someone why [Int] in a visible type argument means something different from [Int]
in a type signature. Intuitively it doesn't seem unreasonable to add a little more magic to the T2T mapping to preserve what (to me) seem to be reasonable expectations. But perhaps it's my expectations that need to be adjusted.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
Cheers<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
Simon<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
<u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
On Tue, 1 Jun 2021 at 23:43, Simon Peyton Jones via ghc-steering-committee <<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-color:currentcolor currentcolor currentcolor rgb(204,204,204);border-style:none none none solid;border-width:medium medium medium 1pt;padding:0cm 0cm 0cm 6pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal">I am generally in support.<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Working out the details in the <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fdependent-types%2Fproposals%2F0000-dependent-type-design.rst%23lexical-scoping-term-syntax-and-type-syntax-and-renaming&data=04%7C01%7Csimonpj%40microsoft.com%7Cdcb5e8e284534fbe907e08d925a5a8fd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637582215722924051%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=WuKipA%2Fm1OenKtDFqX1UpWUsUslzGDcdgASfUyF%2BT7Y%3D&reserved=0" target="_blank">dependent
types proposal</a> was extremely helpful. <u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Like Simon, I’m sad that I have to write<u></u><u></u></p>
<p class="MsoNormal"> f (List Int)<u></u><u></u></p>
<p class="MsoNormal">or<u></u><u></u></p>
<p class="MsoNormal"> f (type [Int])<u></u><u></u></p>
<p class="MsoNormal">but I think the alternative (of requiring the reader to know the type of the function in order to resolve the binding of names in its argument) is much, much worse.
<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">The tension here is fundamental if you want to have required type arguments at all.
<i>It’s not an artefact of GHC’s history, or the constraints of the existing language.</i> (I suppose that in a new language you might *<b>only</b>* provide “List Int” and “Pair a b”, but I do like [Int] and (a,b) as types, and they will continue to work just
fine in types.)<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">So I have made my peace with it; and I really like the option of a “type” herald to switch to type syntax.<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Simon<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<div style="border-style:none none none solid;border-width:medium medium medium 1.5pt;padding:0cm 0cm 0cm 4pt;border-color:currentcolor currentcolor currentcolor blue">
<div>
<div style="border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm;border-color:currentcolor">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> ghc-steering-committee <<a href="mailto:ghc-steering-committee-bounces@haskell.org" target="_blank">ghc-steering-committee-bounces@haskell.org</a>>
<b>On Behalf Of </b>Richard Eisenberg<br>
<b>Sent:</b> 28 May 2021 19:49<br>
<b>To:</b> ghc-steering-committee <<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a>><br>
<b>Subject:</b> [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept</span><u></u><u></u></p>
</div>
</div>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Hi committee,<u></u><u></u></p>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Proposal #281 has been submitted for our consideration.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Proposal PR: <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F281&data=04%7C01%7Csimonpj%40microsoft.com%7Cdcb5e8e284534fbe907e08d925a5a8fd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637582215722924051%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=SYgTG4eay7HpZT3nTbpHA7UpY1e5j1CRvzY0e0Flp78%3D&reserved=0" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/281</a><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Proposal text: <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fint-index%2Fghc-proposals%2Fblob%2Fvisible-forall%2Fproposals%2F0000-visible-forall.rst&data=04%7C01%7Csimonpj%40microsoft.com%7Cdcb5e8e284534fbe907e08d925a5a8fd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637582215722934043%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=532wRXqTp2taTHovb60Ox7hlQ6nEYsc559vwxT3k9og%3D&reserved=0" target="_blank">https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst</a><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">The text of the proposal is long and detailed, but do not be daunted: it is simpler in practice than it appears.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">The main payload of the proposal is: Introduce a new extension -XRequiredTypeArguments. With this extension enabled, the `forall ... ->` syntax, currently in existence in kinds,
is now available in types (of ordinary functions). This means that function definitions and call sites are sometimes required to write a type argument. The type argument is *not* preceded by @ or any other syntactic marker.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">This is useful for defining what would otherwise be ambiguous types. Example:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<p class="MsoNormal">sizeof :: forall a -> Sizeable a => Int<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">sizeof = ...<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">intWidth = sizeof Int<u></u><u></u></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">There are further examples and motivation in the proposal.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">The rest of the proposal is simply about dealing with odd corner cases that come up with the main payload. In particular, mixing types in with terms with no syntactic signifier
means that we must be careful about parsing and namespaces. If a type argument is written in the syntax that is shared between types and terms (including function application!) and uses identifiers in scope in only one of the two namespaces, nothing unusual
can be observed. But, of course, there are corner cases. Here are some of the salient details:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">- Define type-syntax and term-syntax, where the choice of syntax is always driven by syntactic markers, such as :: or @. See the <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fdependent-types%2Fproposals%2F0000-dependent-type-design.rst%23lexical-scoping-term-syntax-and-type-syntax-and-renaming&data=04%7C01%7Csimonpj%40microsoft.com%7Cdcb5e8e284534fbe907e08d925a5a8fd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637582215722934043%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=8iWimwY3208NqZ10odohmJbsUfqd2%2Bj6mKtMzd642d0%3D&reserved=0" target="_blank">dependent
types proposal</a> for more details. Parsing and name-resolution are controlled by whether a phrase is in type-syntax or term-syntax. For name resolution, if a lookup fails in the first namespace (the term-level namespace in term-syntax or the type-level namespace
in type-syntax), we try the other namespace before failing.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">- Because term- vs type-syntax is controlled by syntax, a required type argument is in *term*-syntax and gets name-resolved *as a term*. In the absence of punning, this works out
fine, but it is possible that a punned identifier will cause confusion. The proposal includes section 4.3 allowing users to write `type` to signify a switch to type-syntax.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">- The proposal also includes a way to avoid punning for the built-in types with privileged syntax: lists and tuples. This method allows users to specify -XNoListTupleTypeSyntax
to disable the list and tuple syntax in types (but still allows it for terms). The proposal also suggests exporting type List = [] from Data.List and other synonyms for tuples from Data.Tuple.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">---------------<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">I recommend acceptance. When doing type-level programming, the lack of this feature is strange, leading to ambiguous types and easy-to-forget arguments and easy-to-make type errors.
The design space here is difficult, but this proposal is very much in keeping with the design sketch of our recently-accepted #378, in particular <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fdependent-types%2Fproposals%2F0000-dependent-type-design.rst%23dependent-application-and-the-static-subset&data=04%7C01%7Csimonpj%40microsoft.com%7Cdcb5e8e284534fbe907e08d925a5a8fd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637582215722944041%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=eI%2FKNYePV3PSZItvBM39WTss1N%2BsrvmxLKwRazczIl8%3D&reserved=0" target="_blank">its
section on this point</a>. I believe the design described here is both backward compatible with what we have today (users who do not use this feature will not notice a difference) and forward compatible with a cohesive design for dependent types.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">There are several optional pieces:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">- <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fint-index%2Fghc-proposals%2Fblob%2Fvisible-forall%2Fproposals%2F0000-visible-forall.rst%23secondary-change-type-herald&data=04%7C01%7Csimonpj%40microsoft.com%7Cdcb5e8e284534fbe907e08d925a5a8fd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637582215722954031%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=MZz0YZHOxGdeVUoU0iMDJ9dTh00628V4vc%2FcfH%2F2KqY%3D&reserved=0" target="_blank">The
`type` herald</a>. I am unsure about this one, but others have felt strongly in favor, and I have no reason to object.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">- <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fint-index%2Fghc-proposals%2Fblob%2Fvisible-forall%2Fproposals%2F0000-visible-forall.rst%23secondary-change-types-in-terms&data=04%7C01%7Csimonpj%40microsoft.com%7Cdcb5e8e284534fbe907e08d925a5a8fd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637582215722954031%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=uy5hAExvn4lm1xiPuB181w%2BBPEIeC%2BhGzeQ8RscXAVo%3D&reserved=0" target="_blank">Types-in-terms</a>.
I think this is necessary in order to avoid annoying definitions of type synonyms for one-off usage sites. It is a straightforward extension of the term-level parser to allow previously type-level-only constructs. It is necessary in order for us to achieve
the vision of dependent types in #378. The only challenge here is that this requires us to make `forall` an unconditional keyword in terms. This does pose a backward-compatibility problem. I see, for example, that the sbv package exports a function named `forall`,
so we may need to think more carefully about how to proceed here -- possibly by guarding the keyword-ness of `forall` behind the extension for some number of transitionary releases.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">- <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fint-index%2Fghc-proposals%2Fblob%2Fvisible-forall%2Fproposals%2F0000-visible-forall.rst%23secondary-change-lists-and-tuples&data=04%7C01%7Csimonpj%40microsoft.com%7Cdcb5e8e284534fbe907e08d925a5a8fd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637582215722964026%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=vDjhdgzssqJaO5PlR6kj9E9J7IR16cd5n5pODPcovM0%3D&reserved=0" target="_blank">Lists
and Tuples</a>. This section describes the -XNoListTupleTypeSyntax extension. I am not convinced that this change needs to be part of this proposal (thinking it belongs more in #270), but I do think we'll need it in the end. Is it OK to export new type synonyms
from Data.List and Data.Tuple? Not sure, though I'd like these exported from some central place.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">What do others think?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Thanks,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Richard<u></u><u></u></p>
</div>
</div>
</div>
</div>
<p class="MsoNormal">_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
<a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&data=04%7C01%7Csimonpj%40microsoft.com%7Cdcb5e8e284534fbe907e08d925a5a8fd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637582215722974020%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=3%2FFa5wYfUBIUWnuK7w2mwkBAnBSkWDcty7LwTyV6fqw%3D&reserved=0" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><u></u><u></u></p>
</blockquote>
</div>
</div>
</div>
</div>
</blockquote></div></div>