Both of your suggestions (regarding lists and regarding Proxy) seem to require type information in order to resolve the meaning of an expression. Given `f e`, I’m assuming you want to parse/rename ‘e’ as an expression if ‘f’ is an ordinary function, and as a type if `f :: forall a -> …`. However, that would violate the Lexical Scoping Principle described in section 4.3.1 of the "Design for Dependent Types” proposal (#378), which states: "For every occurrence of an identifier, it is possible to uniquely identify its binding site, without involving the type system.” This principle is useful both in the implementation (it enables a clear delineation between renaming/typechecking) and when reasoning about programs. While it’s possible to violate it, I believe that writing `f (List Int)` is the lesser evil. Also, I don’t think that you’d need to "write `List Int` when it's a visible type argument, but `[Int]` everywhere else”. If consistency is an explicit goal, one can write `List Int` everywhere. - Vlad

On 29 May 2021, at 14:15, Simon Marlow wrote:

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

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

On 1 Jun 2021, at 15:12, Simon Marlow wrote:

I'm hoping that what I'm suggesting could be done while still doing renaming strictly before typechecking. It's a kind of lazy name resolution - a name can resolve to a set of entities, and whether that is actually ambiguous or not is decided later during type checking, when we know whether we need to resolve the name in a value or a type context. Does that make sense?

Yes, I see how this can work, but if name resolution returns a set of possible entities rather than one, it means it hasn’t actually done name resolution completely. After all, not doing name resolution at all is also equivalent to having a set of names – if the user refers to a variable by its name “x”, then we already narrowed down the set of possible bindings from “all bindings” to “bindings of variables named ‘x’”. But name resolution is complete only when we find out which “x” exactly is referred to. So this idea of lazy name resolution seems to amount to some name resolution prior to type checking, and then some more during type checking. It might be possible, but it does not strike me as "renaming strictly before typechecking”. I worry that it might cause some trouble in other parts of the compiler. Dependency analysis of declarations comes to mind. Let’s say the user defines: data A = B … data B = A … Currently we can process these declarations independently, there are no mutual dependencies. But if we postpone namespace selection, then this will become a strongly connected component, which will affect kind inference. I conjecture a more realistic example could be produced, but my goal is to simply state that weakening name resolution will have non-negligible impact on the implementation. Implementation aside, the lexical scoping principle to which I referred is also about user expectations. When reading and writing code, I don’t want to inspect types just to figure out which name refers to what binding. It should be deducible from the lexical structure of the program. So, while the idea sounds attractive, and it might be implementable, one would have to abandon the lexical scoping principle to pursue it.

On 1 Jun 2021, at 15:12, Simon Marlow wrote:

Not being able to use `[Int]` where a type is expected would be a serious drawback in my opinion, and I don't like the other alternative either: use `List Int` everywhere (rewrite all the Haskell textbooks!).

Cheers Simon

I share your disappointment, but it’s not as bad as rewriting all Haskell books! We continue to support the old syntax in all the old places, so code examples from the books will continue to compile. At the same time, codebases that lean strongly towards intermixing terms and types might adopt a different convention and require writing `List Int` everywhere. It could be part of a project style guide, for example. Also, it is interesting that you say ‘where a type is expected’, because I there are at least three ways to interpret this: 1. Syntactically, a type is what follows after `@`, `::`, etc. 2. Things of kind `… -> Type` are types, things of other kinds are data. So `Bool` is a type, while `True` is data. 3. Erased things are types, so forall-quantified variables stand for types, while lambda-bound variables stand for terms. Interestingly, under the first interpretation, `[Int]` does stand for the type of lists under this proposal, so I imagine it’s not what you meant. The choice between 2 and 3, on the other hand (and if we did lazy name resolution as you suggested earlier), would determine the meaning of programs such as: import Type.Reflection data True kindOf :: forall a -> Typeable a => String kindOf a = show (typeRepKind (typeRep @a)) main = print (kindOf True) Should this program print “Bool” or “Type”? Under (2), it must print “Bool”, because “True” is first of all data. Under (3), it must print “Type”, because the input to ‘kindOf’ is forall-quantified and erased. Even if we partially postpone name resolution until type checking, there’s a lot of design space to explore (and to explain in the User’s Guide! this is not straightforward). Under (1) it prints “Bool”, and name resolution remains blissfully unaware of any types involved. - Vlad

So this idea of lazy name resolution seems to amount to some name resolution prior to type checking, and then some more during type checking. It might be possible, but it does not strike me as "renaming strictly before typechecking”.

Don't we already do this for DataKinds? The lexical scoping rule is slightly cheating with respect to DataKinds because while we can resolve an identifier to its binding site, the binding site in the case of a promoted constructor is actually two binding sites :)

I don't think we do. With DataKinds, an occurrence of a capitalized identifier in a type (where "in a type" means in type-syntax https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0...) first looks in the type namespace. If this lookup is successful, stop, returning the type-level name. Otherwise, look in the term namespace. If we know what is in scope (and what is in what namespace), we can still uniquely find the single binding site associated with an occurrence. (I'm not sure what you mean by "two binding sites".)

To clarify what I meant here - if we want consistency, where consistency means referring to the type of lists of Int using the same syntax everywhere, then this leads to List Int and having to rewrite the Haskell textbooks. So all the options are bad: we either have two ways to write list of Int (and in some places only one of them works), or we have consistency but we're changing something fundamental (and to a worse syntax).

"worse" is (of course) a matter of opinion. I've had a number of students who, after learning [3] :: [Int], thought that [] :: [] and [3,4] :: [Int, Int]. I actually think that (textbooks/blog posts/history aside -- which is impossible) List Int is better syntax.

The third option, namely using the "type" prefix also doesn't seem appealing, because I have to know when to use the "type" prefix.

Precisely! The advantage here is that the author is responsible for figuring out when to put in the "type" prefix, as opposed to the reader. If I write f [Int], what have I passed? Is it a single-element list containing the type Int? or is it the type describing lists of Ints? A reader has no way of knowing -- this is a violation of the LSP. I'd much rather put the disambiguation burden on the author of the code than on the reader. Code is read more often than it is written/revised.

I could use it all the time, but then that's not much better than the current situation (@-prefix)

I think it's better than the current situation, because the type argument can now be required, instead of inferred-and-ambiguous.

and I also have to read code written by other people who don't adopt this convention.

Yes, that's indeed true.

With regard to list syntax in particular, I guess I still don't understand why we can't * require a promoted list to be written '[Int] * change the T2T mapping so that [Int] means "list of Int" rather than the promoted interpretation

Unfortunately, the ' syntax in terms is taken by Template Haskell. So f '[] can be used today to pass the TH Name associated with nil. Ignoring this wrinkle, does your counter-proposal extend to names other than the brackets in [Int]? For example, if I have data T = T and write f T, which T am I passing? There are two, and the LSP suggests that we should be able to answer this question without knowing the type of f.

After all, DataKinds already recommends using the leading quote and not relying on unquoted syntax.

Yes, but I actually think this was a mistake in retrospect -- even though I implemented -Wunticked-promoted-constructors. Better would have been to implement -Wpuns. :)

or perhaps this is undesirable for some reason? Do you think the promoted interpretation is more useful?

In truth, I think the type-level interpretation is more useful. But I'd rather GHC be more predictable (that is, follow the LSP) than try to be clever here. Richard

Cheers Simon

Also, it is interesting that you say ‘where a type is expected’, because I there are at least three ways to interpret this:

1. Syntactically, a type is what follows after `@`, `::`, etc. 2. Things of kind `… -> Type` are types, things of other kinds are data. So `Bool` is a type, while `True` is data. 3. Erased things are types, so forall-quantified variables stand for types, while lambda-bound variables stand for terms.

Interestingly, under the first interpretation, `[Int]` does stand for the type of lists under this proposal, so I imagine it’s not what you meant. The choice between 2 and 3, on the other hand (and if we did lazy name resolution as you suggested earlier), would determine the meaning of programs such as:

import Type.Reflection

data True

kindOf :: forall a -> Typeable a => String kindOf a = show (typeRepKind (typeRep @a))

main = print (kindOf True)

Should this program print “Bool” or “Type”? Under (2), it must print “Bool”, because “True” is first of all data. Under (3), it must print “Type”, because the input to ‘kindOf’ is forall-quantified and erased.

Even if we partially postpone name resolution until type checking, there’s a lot of design space to explore (and to explain in the User’s Guide! this is not straightforward).

Under (1) it prints “Bool”, and name resolution remains blissfully unaware of any types involved.

- Vlad

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 Yes, that was my view to begin with. But I can't come up with any magic! 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). 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. 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! 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. 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: https://github.com/adamgundry/ghc-proposals/blob/no-ambiguous-selectors/prop... If you have any other ideas, I'm all ears. Simon From: Simon Marlow Sent: 02 June 2021 10:06 To: Simon Peyton Jones Cc: Richard Eisenberg ; ghc-steering-committee Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept 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. Cheers Simon On Tue, 1 Jun 2021 at 23:43, Simon Peyton Jones via ghc-steering-committee mailto:ghc-steering-committee@haskell.org> wrote: I am generally in support. Working out the details in the dependent types proposalhttps://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 was extremely helpful. Like Simon, I'm sad that I have to write f (List Int) or f (type [Int]) 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. The tension here is fundamental if you want to have required type arguments at all. It's not an artefact of GHC's history, or the constraints of the existing language. (I suppose that in a new language you might *only* 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.) So I have made my peace with it; and I really like the option of a "type" herald to switch to type syntax. Simon From: ghc-steering-committee mailto:ghc-steering-committee-bounces@haskell.org> On Behalf Of Richard Eisenberg Sent: 28 May 2021 19:49 To: ghc-steering-committee mailto:ghc-steering-committee@haskell.org> Subject: [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept Hi committee, Proposal #281 has been submitted for our consideration. Proposal PR: https://github.com/ghc-proposals/ghc-proposals/pull/281https://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 Proposal text: https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/000...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 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 proposalhttps://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 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 pointhttps://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. 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` heraldhttps://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. I am unsure about this one, but others have felt strongly in favor, and I have no reason to object. - Types-in-termshttps://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. 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 Tupleshttps://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. 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@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committeehttps://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

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. 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. 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). Cheers Simon On Wed, 2 Jun 2021 at 11:02, Simon Peyton Jones wrote:

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

Yes, that was my view to begin with. But I can’t come up with any magic!

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).

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.

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!

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.

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: https://github.com/adamgundry/ghc-proposals/blob/no-ambiguous-selectors/prop...

If you have any other ideas, I’m all ears.

Simon

*From:* Simon Marlow *Sent:* 02 June 2021 10:06 *To:* Simon Peyton Jones *Cc:* Richard Eisenberg ; ghc-steering-committee < ghc-steering-committee@haskell.org> *Subject:* Re: [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept

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.

Cheers

Simon

On Tue, 1 Jun 2021 at 23:43, Simon Peyton Jones via ghc-steering-committee wrote:

I am generally in support.

Working out the details in the dependent types proposal 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 was extremely helpful.

Like Simon, I’m sad that I have to write

f (List Int)

or

f (type [Int])

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.

The tension here is fundamental if you want to have required type arguments at all. *It’s not an artefact of GHC’s history, or the constraints of the existing language.* (I suppose that in a new language you might **only** 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.)

So I have made my peace with it; and I really like the option of a “type” herald to switch to type syntax.

Simon

*From:* ghc-steering-committee *On Behalf Of *Richard Eisenberg *Sent:* 28 May 2021 19:49 *To:* ghc-steering-committee *Subject:* [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept

Hi committee,

Proposal #281 has been submitted for our consideration.

Proposal PR: https://github.com/ghc-proposals/ghc-proposals/pull/281 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

Proposal text: https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/000... 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

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://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 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://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. 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://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. I am unsure about this one, but others have felt strongly in favor, and I have no reason to object.

- Types-in-terms 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. 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://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. 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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee 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

This proposal has been revised for clarity, yet much of the payload is the same. I've just made a few small suggestions, but I believe we can deliberate here in parallel. To recap: Proposal PR: https://github.com/ghc-proposals/ghc-proposals/pull/281 https://github.com/ghc-proposals/ghc-proposals/pull/281 Proposal text: https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/000... https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/000... 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/0... 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. - One unfortunate consequence of this extra namespace looking is around implicit quantification. If we have `a = 42` in scope and write `f :: a -> a`, that `a` will not be implicitly quantified. Instead, the user will get an error about the appearance of a term in a type -- but only if -XRequiredTypeArguments is on. This change affects no current code, but it does make the extension fork-like, in that enabling the new extension is not conservative. - 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 allows 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/0.... 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. The "unfortunate consequence" above is, well, unfortunate, but I think it is unavoidable in the context of #378 -- and it will not bite if the user avoids puns. It would be great to bring this long-running proposal to a conclusion, so I'd love to hear your opinions in the next two weeks. Thanks! Richard

On Jul 19, 2021, at 3:22 PM, Richard Eisenberg wrote:

This thread has trailed off, having escaped the pen while the shepherd (me) was distracted (first by travel, then by POPL). I'd like to resume it.

You may wish to refresh yourself on the content of the proposal, which I summarize in https://mail.haskell.org/pipermail/ghc-steering-committee/2021-May/002454.ht... https://mail.haskell.org/pipermail/ghc-steering-committee/2021-May/002454.ht...

My recommendation remains to accept, for the same reasons it was originally.

This proposal is somewhat controversial (it has garnered 278 comments!), and so it would be ideal to hear opinions from as many of you as possible, even if the opinion is just to accept the recommendation.

Simon M wrote the last email in the thread before the hiatus, with a few questions. I'll attempt these now:

...

On Jun 7, 2021, at 4:19 AM, Simon Marlow mailto:marlowsd@gmail.com> wrote:

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.

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?

My answer: "shouldn't need to care". This is enshrined in the Syntactic Unification Principle (SUP) in https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-de...: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-de...

...

Syntactic Unification Principle (SUP). In the absence of punning, there is no difference between type-syntax and term-syntax.

Here, "punning" means having the same identifier in scope in both terms and types. Forgetting about the possibility of punning, users shouldn't care about whether they're writing a term or a type. All syntax will have equivalent meanings in the two environments. The *only* challenge is around namespacing -- and the LSP says that, in a term, names should correspond to term-level entities.

...

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).

We *could* do this, yes, but it's in violation of the LSP (and, perhaps, the SUP). Of course, we wrote the LSP and can choose to break it, but, like Simon PJ, I think the ability to resolve names in the absence of type-checking is very valuable to readers of code.

--------------

One development on the GitHub tracker that may be of interest:

@AntC2 proposes a migration trick to allow functions to migrate from today's world to a world with this new feature. The key example is sizeOf. Today, we have

...

sizeOf :: Storable a => a -> Int

where the argument to sizeOf is always unevaluated and ignored. The proposal under consideration would allow this to change to

...

sizeOf' :: forall a -> Storable a => Int

(NB: do not get distracted by the movement of the constraint, which will be invisible at usage sites) The problem is that we would have to make sizeOf' a new function, likely exported from a new library, in order not to clash. This is annoying. So @AntC2 proposes (in my paraphrasing, which @AntC2 has agreed with):

* With -XNoRequiredTypeArguments, if a function f takes a required type argument of kind Type, then instead you can pass an arbitrary expression. f is called with the type of that expression; the expression is never evaluated.

This would allow, e.g. sizeOf True to work with both the old and the new types.

I am against this little addition, because it's narrowly applicable and has negative educational consequences (that is, someone encountering the type written for sizeOf' but then seeing sizeOf' True work correctly will be quite befuddled and likely form a misunderstanding of how forall -> works). Yet I can see this idea's appeal, thus my mentioning it here.

------------------

It would be great if I could hear from everyone on the committee in the next two weeks with their opinion about accepting this proposal.

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

There are a lot of inconvenient side effects and corner cases Arnaud, could you enumerate them? Even if (as I strongly hope) we accept this proposal, it's good to have a concrete list of things to bear in mind. I for one do not have such list in my head. One principle that the proposal espouses (but perhaps does not call out explicitly) is that it should be possible to write an explicit binder for every in-scope variable. So instead of data T (a :: k -> k) = ... I want to write data T @k (a :: k -> k) = ... with an explicit binder for k. So I see the proposal as removing an ad-hoc wart in the language. But I may be blind to the "inconvenient side effects and corner cases" and I'd welcome a list of such cases. Simon PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.commailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.commailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.) From: ghc-steering-committee On Behalf Of Spiwack, Arnaud Sent: 27 October 2021 09:20 To: Richard Eisenberg Cc: ghc-steering-committee Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept I've been struggling to have an opinion on this PR. I'm very sympathetic to the goal of the proposal (and this latest rendition of the proposal is a really good document). There are a lot of inconvenient side effects and corner cases (but, to be fair, these are not special to this proposal: they are inherent to the dependent types plan). But I'm fairly convinced that this is the best possible approach, or close enough. So yes, I don't really feel strongly about it. But on balance, I think that I'm in favour. On Tue, Oct 12, 2021 at 9:05 PM Richard Eisenberg mailto:rae@richarde.dev> wrote: This proposal has been revised for clarity, yet much of the payload is the same. I've just made a few small suggestions, but I believe we can deliberate here in parallel. To recap: Proposal PR: https://github.com/ghc-proposals/ghc-proposals/pull/281https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F281&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688770920%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=9k5jhyoKPDXal1oQoahl7CDReJtVVK3yet1a82td1KQ%3D&reserved=0 Proposal text: https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/000...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%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688780863%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=VBNE3eXKhJKDonDrfeuWoLTWaBsINs5TLPrghtYAdkc%3D&reserved=0 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 proposalhttps://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%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688790833%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=GuMiExefsGrYT8qkQZe1rgmo42M%2By0TDOrEmyXUNcoQ%3D&reserved=0 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. - One unfortunate consequence of this extra namespace looking is around implicit quantification. If we have `a = 42` in scope and write `f :: a -> a`, that `a` will not be implicitly quantified. Instead, the user will get an error about the appearance of a term in a type -- but only if -XRequiredTypeArguments is on. This change affects no current code, but it does make the extension fork-like, in that enabling the new extension is not conservative. - 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 allows 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 pointhttps://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%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688790833%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=VN1vQ77CVUD1Fe9XNfHMzztv%2FD9Jxkt8CjgJtl%2F9w8Y%3D&reserved=0. 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. The "unfortunate consequence" above is, well, unfortunate, but I think it is unavoidable in the context of #378 -- and it will not bite if the user avoids puns. It would be great to bring this long-running proposal to a conclusion, so I'd love to hear your opinions in the next two weeks. Thanks! Richard On Jul 19, 2021, at 3:22 PM, Richard Eisenberg mailto:rae@richarde.dev> wrote: This thread has trailed off, having escaped the pen while the shepherd (me) was distracted (first by travel, then by POPL). I'd like to resume it. You may wish to refresh yourself on the content of the proposal, which I summarize in https://mail.haskell.org/pipermail/ghc-steering-committee/2021-May/002454.ht...https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fpipermail%2Fghc-steering-committee%2F2021-May%2F002454.html&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688800785%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=EsMkJHvCNi30T%2FUneEyJ6mblBO9%2BXv1HUNJGJTSxOy4%3D&reserved=0 My recommendation remains to accept, for the same reasons it was originally. This proposal is somewhat controversial (it has garnered 278 comments!), and so it would be ideal to hear opinions from as many of you as possible, even if the opinion is just to accept the recommendation. Simon M wrote the last email in the thread before the hiatus, with a few questions. I'll attempt these now: On Jun 7, 2021, at 4:19 AM, Simon Marlow mailto:marlowsd@gmail.com> wrote: 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. 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? My answer: "shouldn't need to care". This is enshrined in the Syntactic Unification Principle (SUP) in https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-de...:https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0378-dependent-type-design.rst%3A&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688800785%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=2HE8XEL%2FE4rNvMYcUgmPiNI4NmWX5kO%2B6LhQXi%2FxXmQ%3D&reserved=0

Syntactic Unification Principle (SUP). In the absence of punning, there is no difference between type-syntax and term-syntax.

Here, "punning" means having the same identifier in scope in both terms and types. Forgetting about the possibility of punning, users shouldn't care about whether they're writing a term or a type. All syntax will have equivalent meanings in the two environments. The *only* challenge is around namespacing -- and the LSP says that, in a term, names should correspond to term-level entities. 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). We *could* do this, yes, but it's in violation of the LSP (and, perhaps, the SUP). Of course, we wrote the LSP and can choose to break it, but, like Simon PJ, I think the ability to resolve names in the absence of type-checking is very valuable to readers of code. -------------- One development on the GitHub tracker that may be of interest: @AntC2 proposes a migration trick to allow functions to migrate from today's world to a world with this new feature. The key example is sizeOf. Today, we have

sizeOf :: Storable a => a -> Int

where the argument to sizeOf is always unevaluated and ignored. The proposal under consideration would allow this to change to

sizeOf' :: forall a -> Storable a => Int

(NB: do not get distracted by the movement of the constraint, which will be invisible at usage sites) The problem is that we would have to make sizeOf' a new function, likely exported from a new library, in order not to clash. This is annoying. So @AntC2 proposes (in my paraphrasing, which @AntC2 has agreed with): * With -XNoRequiredTypeArguments, if a function f takes a required type argument of kind Type, then instead you can pass an arbitrary expression. f is called with the type of that expression; the expression is never evaluated. This would allow, e.g. sizeOf True to work with both the old and the new types. I am against this little addition, because it's narrowly applicable and has negative educational consequences (that is, someone encountering the type written for sizeOf' but then seeing sizeOf' True work correctly will be quite befuddled and likely form a misunderstanding of how forall -> works). Yet I can see this idea's appeal, thus my mentioning it here. ------------------ It would be great if I could hear from everyone on the committee in the next two weeks with their opinion about accepting this proposal. Thanks, Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committeehttps://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%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688810744%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=Cl00sfjlpg3xh2jTlToWAsJgBTUfqQcNS1ZxNn6utiI%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committeehttps://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%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688810744%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=Cl00sfjlpg3xh2jTlToWAsJgBTUfqQcNS1ZxNn6utiI%3D&reserved=0

I was indeed confused! Apologies. But my main point remains: enumerating a list of inconvenient side effects and corner cases would be a great service. Simon PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.) | -----Original Message----- | From: Vladislav Zavialov (int-index) | Sent: 27 October 2021 10:10 | To: Simon Peyton Jones | Cc: Spiwack, Arnaud ; Richard Eisenberg | ; ghc-steering-committee | Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall" | in terms; rec: accept | | Simon, perhaps you’re thinking of another proposal that is currently | under committee’s consideration? | | Arnaud was commenting on #281, and you seem to be talking about #425. | | - Vlad | | > On 27 Oct 2021, at 12:05, Simon Peyton Jones via ghc-steering- | committee wrote: | > | > There are a lot of inconvenient side effects and corner cases | > | > Arnaud, could you enumerate them? Even if (as I strongly hope) we | accept this proposal, it’s good to have a concrete list of things to | bear in mind. I for one do not have such list in my head. | > | > One principle that the proposal espouses (but perhaps does not call | out explicitly) is that it should be possible to write an explicit | binder for every in-scope variable. So instead of | > data T (a :: k -> k) = … I want to write | > data T @k (a :: k -> k) = … with an explicit binder | > for k. | > | > So I see the proposal as removing an ad-hoc wart in the language. | But I may be blind to the “inconvenient side effects and corner cases” | and I’d welcome a list of such cases. | > | > Simon | > | > | > PS: I am leaving Microsoft at the end of November 2021, at which | point | > simonpj@microsoft.com will cease to work. | > Usesimon.peytonjones@gmail.com instead. (For now, it just forwards | to | > simonpj@microsoft.com.) | > | > From: ghc-steering-committee | > On Behalf Of Spiwack, | > Arnaud | > Sent: 27 October 2021 09:20 | > To: Richard Eisenberg | > Cc: ghc-steering-committee | > Subject: Re: [ghc-steering-committee] Proposal #281: Visible | "forall" | > in terms; rec: accept | > | > I've been struggling to have an opinion on this PR. I'm very | sympathetic to the goal of the proposal (and this latest rendition of | the proposal is a really good document). There are a lot of | inconvenient side effects and corner cases (but, to be fair, these are | not special to this proposal: they are inherent to the dependent types | plan). But I'm fairly convinced that this is the best possible | approach, or close enough. | > | > | > | > So yes, I don't really feel strongly about it. But on balance, I | think that I'm in favour.

It has been two weeks. I have heard no argument against this proposal, but Simon Marlow (in the springtime) expressed some puzzlement. Simon, what are you thinking about this now? With no further response, I will accept this proposal on Friday. Others are also very welcome to chime in! Thanks, all! Richard

On Oct 27, 2021, at 5:30 AM, Spiwack, Arnaud wrote:

I think that the proposal makes a great job at listing the issues. It's quite transparent about this, I'm not sure what I could add.

On Wed, Oct 27, 2021 at 11:29 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: I was indeed confused! Apologies.

But my main point remains: enumerating a list of inconvenient side effects and corner cases would be a great service.

Simon

PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com mailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com mailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com mailto:simonpj@microsoft.com.)

| -----Original Message----- | From: Vladislav Zavialov (int-index) mailto:vlad.z.4096@gmail.com> | Sent: 27 October 2021 10:10 | To: Simon Peyton Jones mailto:simonpj@microsoft.com> | Cc: Spiwack, Arnaud mailto:arnaud.spiwack@tweag.io>; Richard Eisenberg | mailto:rae@richarde.dev>; ghc-steering-committee mailto:committee@haskell.org> | Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall" | in terms; rec: accept | | Simon, perhaps you’re thinking of another proposal that is currently | under committee’s consideration? | | Arnaud was commenting on #281, and you seem to be talking about #425. | | - Vlad | | > On 27 Oct 2021, at 12:05, Simon Peyton Jones via ghc-steering- | committee mailto:ghc-steering-committee@haskell.org> wrote: | > | > There are a lot of inconvenient side effects and corner cases | > | > Arnaud, could you enumerate them? Even if (as I strongly hope) we | accept this proposal, it’s good to have a concrete list of things to | bear in mind. I for one do not have such list in my head. | > | > One principle that the proposal espouses (but perhaps does not call | out explicitly) is that it should be possible to write an explicit | binder for every in-scope variable. So instead of | > data T (a :: k -> k) = … I want to write | > data T @k (a :: k -> k) = … with an explicit binder | > for k. | > | > So I see the proposal as removing an ad-hoc wart in the language. | But I may be blind to the “inconvenient side effects and corner cases” | and I’d welcome a list of such cases. | > | > Simon | > | > | > PS: I am leaving Microsoft at the end of November 2021, at which | point | > simonpj@microsoft.com mailto:simonpj@microsoft.com will cease to work. | > Usesimon.peytonjones@gmail.com mailto:Usesimon.peytonjones@gmail.com instead. (For now, it just forwards | to | > simonpj@microsoft.com mailto:simonpj@microsoft.com.) | > | > From: ghc-steering-committee | > mailto:ghc-steering-committee-bounces@haskell.org> On Behalf Of Spiwack, | > Arnaud | > Sent: 27 October 2021 09:20 | > To: Richard Eisenberg mailto:rae@richarde.dev> | > Cc: ghc-steering-committee mailto:ghc-steering-committee@haskell.org> | > Subject: Re: [ghc-steering-committee] Proposal #281: Visible | "forall" | > in terms; rec: accept | > | > I've been struggling to have an opinion on this PR. I'm very | sympathetic to the goal of the proposal (and this latest rendition of | the proposal is a really good document). There are a lot of | inconvenient side effects and corner cases (but, to be fair, these are | not special to this proposal: they are inherent to the dependent types | plan). But I'm fairly convinced that this is the best possible | approach, or close enough. | > | > | > | > So yes, I don't really feel strongly about it. But on balance, I | think that I'm in favour.

| 1. f @Int -- traditional, invisible forall 2. f Int -- visible forall, | Int is unambiguous 3. f (type Int) -- visible forall, Int is ambiguous Perhaps it would help, in the proposal, to make explicit the argument *against* using @ as the herald for all type arguments. I remember that there *is* such an argument, and I found it quite convincing, but I can't remember it now. Maybe it is there somewhere? Vlad/Richard? Simon PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.) | -----Original Message----- | From: ghc-steering-committee On Behalf Of Eric Seidel | Sent: 29 October 2021 02:16 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall" | in terms; rec: accept | | I would still prefer alternative 5 (using @ as the type herald). I | really dislike that we would now have three ways to specify a type | argument: | | 1. f @Int -- traditional, invisible forall 2. f Int -- visible forall, | Int is unambiguous 3. f (type Int) -- visible forall, Int is ambiguous | | Ideally I would have single syntax for specifying type arguments, | which was historically (1). I know that many people would like to | unify the term and type syntaxes, so I'm ok with (2) as well even | though the T2T algorithm seemed quite involved. But adding (3) really | feels excessive. | | But I believe I'm a small minority in this opinion, so I don't want to | stand in the way of a very useful feature. | | On Wed, Oct 27, 2021, at 09:56, Richard Eisenberg wrote: | > It has been two weeks. I have heard no argument against this | proposal, | > but Simon Marlow (in the springtime) expressed some puzzlement. | Simon, | > what are you thinking about this now? With no further response, I | will | > accept this proposal on Friday. | > | > Others are also very welcome to chime in! | > | > Thanks, all! | > Richard | > | >> On Oct 27, 2021, at 5:30 AM, Spiwack, Arnaud | wrote: | >> | >> I think that the proposal makes a great job at listing the issues. | It's quite transparent about this, I'm not sure what I could add. | >> | >> On Wed, Oct 27, 2021 at 11:29 AM Simon Peyton Jones | wrote: | >>> I was indeed confused! Apologies. | >>> | >>> But my main point remains: enumerating a list of inconvenient side | effects and corner cases would be a great service. | >>> | >>> Simon | >>> | >>> PS: I am leaving Microsoft at the end of November 2021, at which | >>> point simonpj@microsoft.com will cease to work. Use | >>> simon.peytonjones@gmail.com instead. (For now, it just forwards | to | >>> simonpj@microsoft.com.) | >>> | >>> | -----Original Message----- | >>> | From: Vladislav Zavialov (int-index) | >>> | Sent: 27 October 2021 10:10 | >>> | To: Simon Peyton Jones | >>> | Cc: Spiwack, Arnaud ; Richard | Eisenberg | >>> | ; ghc-steering-committee >> | committee@haskell.org> | >>> | Subject: Re: [ghc-steering-committee] Proposal #281: Visible | "forall" | >>> | in terms; rec: accept | >>> | | >>> | Simon, perhaps you're thinking of another proposal that is | >>> | currently under committee's consideration? | >>> | | >>> | Arnaud was commenting on #281, and you seem to be talking about | #425. | >>> | | >>> | - Vlad | >>> | | >>> | > On 27 Oct 2021, at 12:05, Simon Peyton Jones via ghc- | steering- | >>> | committee wrote: | >>> | > | >>> | > There are a lot of inconvenient side effects and corner cases | >>> | > > Arnaud, could you enumerate them? Even if (as I strongly | >>> | hope) we accept this proposal, it's good to have a concrete | list | >>> | of things to | >>> | bear in mind. I for one do not have such list in my head. | >>> | > | >>> | > One principle that the proposal espouses (but perhaps does | not | >>> | call out explicitly) is that it should be possible to write an | explicit | >>> | binder for every in-scope variable. So instead of | >>> | > data T (a :: k -> k) = ... I want to write | >>> | > data T @k (a :: k -> k) = ... with an explicit | binder | >>> | > for k. | >>> | > | >>> | > So I see the proposal as removing an ad-hoc wart in the | language. | >>> | But I may be blind to the "inconvenient side effects and corner | cases" | >>> | and I'd welcome a list of such cases. | >>> | > | >>> | > Simon | >>> | > | >>> | > | >>> | > PS: I am leaving Microsoft at the end of November 2021, at | >>> | which point > simonpj@microsoft.com will cease to work. | >>> | > Usesimon.peytonjones@gmail.com instead. (For now, it just | >>> | forwards to > simonpj@microsoft.com.) > > From: | >>> | ghc-steering-committee > | >>> | On Behalf Of | Spiwack, | >>> | > Arnaud > Sent: 27 October 2021 09:20 > To: Richard Eisenberg | >>> | > Cc: ghc-steering-committee | >>> | | >>> | > Subject: Re: [ghc-steering-committee] Proposal #281: Visible | >>> | "forall" | >>> | > in terms; rec: accept | >>> | > | >>> | > I've been struggling to have an opinion on this PR. I'm very | >>> | sympathetic to the goal of the proposal (and this latest | rendition | >>> | of the proposal is a really good document). There are a lot of | >>> | inconvenient side effects and corner cases (but, to be fair, | these | >>> | are not special to this proposal: they are inherent to the | >>> | dependent types plan). But I'm fairly convinced that this is | the | >>> | best possible approach, or close enough. | >>> | > | >>> | > | >>> | > | >>> | > So yes, I don't really feel strongly about it. But on | balance, | >>> | I think that I'm in favour. | > | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | > .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&a | > | mp;data=04%7C01%7Csimonpj%40microsoft.com%7C69ae5d5e09784d08370708d99a | > | 79ccff%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637710670242799539 | > | %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6I | > | k1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=hGq4xMd5RsHOEGwF7lr3QCuMUXrxSwl | > cjEH89KLcy5A%3D&reserved=0 | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | 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%7C69ae5d5e09784d0 | 8370708d99a79ccff%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6377106 | 70242799539%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=hGq4xMd5RsHOEGwF7lr3 | QCuMUXrxSwlcjEH89KLcy5A%3D&reserved=0

Yes, the proposal does argue explicitly against '@', I just don't find the argument all that convincing. 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. On Fri, Oct 29, 2021, at 11:01, Vladislav Zavialov (int-index) wrote:

The problem with ‘@‘, as explained by Richard, is cited right next to the Alternative 5.

However, I agree with Eric that the ’type’ herald feels excessive. It’s not something I personally intend to use. However, I remember Simon PJ and Iavor liked it (if I recall correctly), hence its inclusion in the proposal.

I don’t think it hurts either, though. We can accommodate different programming styles.

- Vlad

...

On 29 Oct 2021, at 17:53, Simon Peyton Jones via ghc-steering-committee wrote:

| 1. f @Int -- traditional, invisible forall 2. f Int -- visible forall, | Int is unambiguous 3. f (type Int) -- visible forall, Int is ambiguous

Perhaps it would help, in the proposal, to make explicit the argument *against* using @ as the herald for all type arguments. I remember that there *is* such an argument, and I found it quite convincing, but I can't remember it now. Maybe it is there somewhere?

Vlad/Richard?

Simon

PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.)

| -----Original Message----- | From: ghc-steering-committee On Behalf Of Eric Seidel | Sent: 29 October 2021 02:16 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall" | in terms; rec: accept | | I would still prefer alternative 5 (using @ as the type herald). I | really dislike that we would now have three ways to specify a type | argument: | | 1. f @Int -- traditional, invisible forall 2. f Int -- visible forall, | Int is unambiguous 3. f (type Int) -- visible forall, Int is ambiguous | | Ideally I would have single syntax for specifying type arguments, | which was historically (1). I know that many people would like to | unify the term and type syntaxes, so I'm ok with (2) as well even | though the T2T algorithm seemed quite involved. But adding (3) really | feels excessive. | | But I believe I'm a small minority in this opinion, so I don't want to | stand in the way of a very useful feature. | | On Wed, Oct 27, 2021, at 09:56, Richard Eisenberg wrote: | > It has been two weeks. I have heard no argument against this | proposal, | > but Simon Marlow (in the springtime) expressed some puzzlement. | Simon, | > what are you thinking about this now? With no further response, I | will | > accept this proposal on Friday. | > | > Others are also very welcome to chime in! | > | > Thanks, all! | > Richard | > | >> On Oct 27, 2021, at 5:30 AM, Spiwack, Arnaud | wrote: | >> | >> I think that the proposal makes a great job at listing the issues. | It's quite transparent about this, I'm not sure what I could add. | >> | >> On Wed, Oct 27, 2021 at 11:29 AM Simon Peyton Jones | wrote: | >>> I was indeed confused! Apologies. | >>> | >>> But my main point remains: enumerating a list of inconvenient side | effects and corner cases would be a great service. | >>> | >>> Simon | >>> | >>> PS: I am leaving Microsoft at the end of November 2021, at which | >>> point simonpj@microsoft.com will cease to work. Use | >>> simon.peytonjones@gmail.com instead. (For now, it just forwards | to | >>> simonpj@microsoft.com.) | >>> | >>> | -----Original Message----- | >>> | From: Vladislav Zavialov (int-index) | >>> | Sent: 27 October 2021 10:10 | >>> | To: Simon Peyton Jones | >>> | Cc: Spiwack, Arnaud ; Richard | Eisenberg | >>> | ; ghc-steering-committee >> | committee@haskell.org> | >>> | Subject: Re: [ghc-steering-committee] Proposal #281: Visible | "forall" | >>> | in terms; rec: accept | >>> | | >>> | Simon, perhaps you're thinking of another proposal that is | >>> | currently under committee's consideration? | >>> | | >>> | Arnaud was commenting on #281, and you seem to be talking about | #425. | >>> | | >>> | - Vlad | >>> | | >>> | > On 27 Oct 2021, at 12:05, Simon Peyton Jones via ghc- | steering- | >>> | committee wrote: | >>> | > | >>> | > There are a lot of inconvenient side effects and corner cases | >>> | > > Arnaud, could you enumerate them? Even if (as I strongly | >>> | hope) we accept this proposal, it's good to have a concrete | list | >>> | of things to | >>> | bear in mind. I for one do not have such list in my head. | >>> | > | >>> | > One principle that the proposal espouses (but perhaps does | not | >>> | call out explicitly) is that it should be possible to write an | explicit | >>> | binder for every in-scope variable. So instead of | >>> | > data T (a :: k -> k) = ... I want to write | >>> | > data T @k (a :: k -> k) = ... with an explicit | binder | >>> | > for k. | >>> | > | >>> | > So I see the proposal as removing an ad-hoc wart in the | language. | >>> | But I may be blind to the "inconvenient side effects and corner | cases" | >>> | and I'd welcome a list of such cases. | >>> | > | >>> | > Simon | >>> | > | >>> | > | >>> | > PS: I am leaving Microsoft at the end of November 2021, at | >>> | which point > simonpj@microsoft.com will cease to work. | >>> | > Usesimon.peytonjones@gmail.com instead. (For now, it just | >>> | forwards to > simonpj@microsoft.com.) > > From: | >>> | ghc-steering-committee > | >>> | On Behalf Of | Spiwack, | >>> | > Arnaud > Sent: 27 October 2021 09:20 > To: Richard Eisenberg | >>> | > Cc: ghc-steering-committee | >>> | | >>> | > Subject: Re: [ghc-steering-committee] Proposal #281: Visible | >>> | "forall" | >>> | > in terms; rec: accept | >>> | > | >>> | > I've been struggling to have an opinion on this PR. I'm very | >>> | sympathetic to the goal of the proposal (and this latest | rendition | >>> | of the proposal is a really good document). There are a lot of | >>> | inconvenient side effects and corner cases (but, to be fair, | these | >>> | are not special to this proposal: they are inherent to the | >>> | dependent types plan). But I'm fairly convinced that this is | the | >>> | best possible approach, or close enough. | >>> | > | >>> | > | >>> | > | >>> | > So yes, I don't really feel strongly about it. But on | balance, | >>> | I think that I'm in favour. | > | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | > .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&a | > | mp;data=04%7C01%7Csimonpj%40microsoft.com%7C69ae5d5e09784d08370708d99a | > | 79ccff%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637710670242799539 | > | %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6I | > | k1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=hGq4xMd5RsHOEGwF7lr3QCuMUXrxSwl | > cjEH89KLcy5A%3D&reserved=0 | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | 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%7C69ae5d5e09784d0 | 8370708d99a79ccff%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6377106 | 70242799539%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=hGq4xMd5RsHOEGwF7lr3 | QCuMUXrxSwlcjEH89KLcy5A%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

I suppose we could use the GHC20XX standards as a way to slowly course-correct. 1. Introduce -X@MeansTypeNamespaceOnly 2. Enable -X@MeansTypeNamespaceOnly as part of GHC2022 3. Let the ecosystem slowly adopt the change as they move to newer language standards But I think there would still be more questions to answer. 1. What becomes the new syntax for visibility specifiers? (I think Agda and Idris use {}?) 2. Do we really need visibility specifiers? (I wish the answer were no, but I think it's yes.) 3. If we do need visibility specifiers, do I then have to write `f {@Int}` to specify an invisible type argument? That's gross. 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.. On Fri, Oct 29, 2021, at 11:35, Spiwack, Arnaud wrote:

On Fri, Oct 29, 2021 at 5:16 PM Eric Seidel wrote:

...

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.

I agree with this. But how would you fix the current situation? `@` is used as a visibility specifier in the user language (well, it switches both visibility and grammar/namespace). If `@` is to switch only grammar/namespace, what do we make of all the `@` that have been written in the past half-dozen years?

/Arnaud

On Fri, Oct 29, 2021, at 13:56, Richard Eisenberg wrote:

2. We would like some type arguments to be visible and some to be invisible. This is the nub of the motivation for #281.

Possibly a slight tangent, but if I were to replace every occurrence of "visible" with "required" and "invisible" with "optional", would that be a valid way of reading the discussion around visibility? For some reason the terminology has always been a bit confusing. Veering off a bit further, if the above substitution is valid, would visibility give us a formalism to deal with optional *value* arguments? It's always bothered me that OCaml has optional/named parameters but Haskell does not.

Yes, to be absolutely clear, I’m ok with merging. Sent from my iPhone

On Oct 29, 2021, at 18:06, Vladislav Zavialov (int-index) wrote:

There’s indeed a similarity, but also some differences. Optional parameters are typically defaulted rather than inferred by unification, and they can be passed by name rather than by position. Both of those would be welcome additions to Haskell, y the way (at least in my opinion, surely this also would need a full proposal).

Those features wouldn’t be a replacement for visible forall, though, but an addition. So before we continue this discussion: what do we think of the proposal at hand?

Richard, you were planning to merge today. My interpretation of Eric’s position (correct me if I’m misrepresenting) is that there are some unfortunate consequences of the proposed design, but we are more or less forced into it by the SUP and other constraints, so there don’t appear to be any better alternatives.

Shall we pull the trigger?

- Vlad

...

On 30 Oct 2021, at 00:17, Eric Seidel wrote:

...

On Fri, Oct 29, 2021, at 13:56, Richard Eisenberg wrote: 2. We would like some type arguments to be visible and some to be invisible. This is the nub of the motivation for #281.

Possibly a slight tangent, but if I were to replace every occurrence of "visible" with "required" and "invisible" with "optional", would that be a valid way of reading the discussion around visibility? For some reason the terminology has always been a bit confusing.

Veering off a bit further, if the above substitution is valid, would visibility give us a formalism to deal with optional *value* arguments? It's always bothered me that OCaml has optional/named parameters but Haskell does not. _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee