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

Sat May 29 11:15:28 UTC 2021

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.

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.

Would it be possible to require the leading quote to get the promoted
meaning, otherwise defaulting to the usual meaning of `[Int]`?

Also could we defer name resolution until type checking for things like
`Proxy`, so that the obvious thing doesn't require namespace gymnastics?

Cheers
Simon

On Fri, 28 May 2021 at 19:49, Richard Eisenberg <rae at richarde.dev> wrote:

> Hi committee,
>
> Proposal #281 has been submitted for our consideration.
>
> Proposal PR: https://github.com/ghc-proposals/ghc-proposals/pull/281
> Proposal text:
> https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst
>
> The text of the proposal is long and detailed, but do not be daunted: it
> is simpler in practice than it appears.
>
> 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.
>
> This is useful for defining what would otherwise be ambiguous types.
> Example:
>
> sizeof :: forall a -> Sizeable a => Int
> sizeof = ...
>
> intWidth = sizeof Int
>
>
> There are further examples and motivation in the proposal.
>
> 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:
> - Define type-syntax and term-syntax, where the choice of syntax is always
> driven by syntactic markers, such as :: or @. See the dependent types
> proposal
> <https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#lexical-scoping-term-syntax-and-type-syntax-and-renaming> 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.
> - 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.
> - 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.
>
> ---------------
>
> 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 its section on this point
> <https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#dependent-application-and-the-static-subset>.
> 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.
>
> There are several optional pieces:
> - The `type` herald
> <https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst#secondary-change-type-herald>.
> I am unsure about this one, but others have felt strongly in favor, and I
> have no reason to object.
> - Types-in-terms
> <https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst#secondary-change-types-in-terms>.
> 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.
> - Lists and Tuples
> <https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst#secondary-change-lists-and-tuples>.
> 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.
>
> What do others think?
>
> Thanks,
> Richard
> _______________________________________________
> 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/20210529/b767ca86/attachment-0001.html>