<div dir="ltr"><div>I support the goal of this proposal; indeed I would immediately use it in several places that I can think of off the top of my head.</div><div><br></div><div>But the name resolution aspects concern me. I forsee a lot of confusion if we can't write `[Int]` as a type argument with the usual meaning. The error message is likely to be super confusing if it has to talk about the difference between a promoted list type and the usual list type constructor, which have the same syntax. I'm not a fan of having to write `List Int` when it's a visible type argument, but `[Int]` everywhere else.<br></div><div><br></div><div>Would it be possible to require the leading quote to get the promoted meaning, otherwise defaulting to the usual meaning of `[Int]`?</div><div><br></div><div>Also could we defer name resolution until type checking for things like `Proxy`, so that the obvious thing doesn't require namespace gymnastics?<br></div><div><br></div><div>Cheers</div><div>Simon<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 28 May 2021 at 19:49, Richard Eisenberg <<a href="mailto:rae@richarde.dev">rae@richarde.dev</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;">Hi committee,<div><br></div><div>Proposal #281 has been submitted for our consideration.</div><div><br></div><div>Proposal PR: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/281" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/281</a></div><div>Proposal text: <a href="https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst" target="_blank">https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst</a></div><div><br></div><div>The text of the proposal is long and detailed, but do not be daunted: it is simpler in practice than it appears.</div><div><br></div><div>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.</div><div><br></div><div>This is useful for defining what would otherwise be ambiguous types. Example:</div><div><br></div><div></div><blockquote type="cite"><div>sizeof :: forall a -> Sizeable a => Int</div><div>sizeof = ...</div><div><br></div><div>intWidth = sizeof Int</div></blockquote><div><br></div><div>There are further examples and motivation in the proposal.</div><div><br></div><div>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:</div><div>- 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://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#lexical-scoping-term-syntax-and-type-syntax-and-renaming" 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.</div><div>- 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.</div><div>- 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.</div><div><br></div><div>---------------</div><div><br></div><div>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://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#dependent-application-and-the-static-subset" 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.</div><div><br></div><div>There are several optional pieces:</div><div>- <a href="https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst#secondary-change-type-herald" 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.</div><div>- <a href="https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst#secondary-change-types-in-terms" 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.</div><div>- <a href="https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst#secondary-change-lists-and-tuples" 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.</div><div><br></div><div>What do others think?</div><div><br></div><div>Thanks,</div><div>Richard</div></div>_______________________________________________<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://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</blockquote></div>