[ghc-steering-committee] Please review #270: Extend Term-Level Lookup rules

Mon Jun 1 17:20:41 UTC 2020

Disclaimer: I'm biased here, as I've been worried for years about how the current story around namespaces can be reconciled with dependent types.

I'm in strong support of the spirit of the proposal, and I see no concrete improvements to offer to the letter of the proposed change specification. (My phrasing here is to make clear that the new specification may indeed have room for improvement, and I encourage us to find that. And as you'll see, I have a different spin on e.g. motivation than the authors present. But I think the spirit is right on.)

While I agree completely (except that the proposal does not mean we need type families to use tuples) with the facts Iavor has presented, I'd like to present them in a different light.

For me, the key payload of the proposal is Iavor's (4): add two warnings:

a. -Wpun-bindings warns whenever a declaration introduces a name into one of our namespaces that would clash with a name in another.

b. -Wpuns warns whenever a name occurrence matches names that are in scope in more than one namespace.

The proposal lists the process of eventually adding these to -Wall (but not to -W or on-by-default).

In some ideal world, that would be it.

The problem with that world is that we generally like to offer our users ways of avoiding warnings. The entire rest of the proposal is around giving users workarounds to suppress the warnings. Before we go there, let me defend why I like these warnings:

- Whenever I have taught introductory Haskell, the type-level/term-level namespace situation has been a cause for confusion. As soon as we get to instance Functor [], we have to be very careful about distinguishing the higher-kinded type constructor [] from the empty list []. And once we start using libraries (e.g. aeson) that use punning liberally, we are worse off. Interestingly, other languages (e.g. C, C++, Java) support distinguished type-level and term-level namespaces, yet I don't believe it's standard practice in any of those languages to actually give two entities the same name, in a way that's common in Haskell.

- The confusion leaks to many areas of the language. See https://github.com/goldfirere/ghc-proposals/blob/namespaces/proposals/0000-namespaces.rst#background, which is part of a previous attempt to fix this problem, but still accurately describes the very messy status quo. Understanding what T means in code requires knowing what context you are in; some contexts give a meaning to T from either namespace, in which case GHC offers 5(!) different ways of allowing the user to choose what they mean, where the syntax depends on the context. (That is, users need to know all 5 ways to disambiguate, because they don't have the choice, given the context.) The five ways are (1) using ' in a type to use a term-level data constructor, (2) using ' for terms vs '' for types in a TH name quote, (3) using 'type' or 'pattern' in import/export lists, (4) using 'type' or 'module' in ANN pragams (but you cannot use 'pattern' for terms), and (5) using 'type or 'value' in fixity declarations. WARNING pragmas do not even offer a way to disambiguate. Of course, we could clean this up, but much better is to avoid the need to disambiguate in the first place.

- By gently encouraging users to avoid punning, we can open the door to wonderful things in the future, including visible dependent quantification in terms, and the use of ordinary term-level functions in types (thus obviating type families). Neither of these requires dependent types, by the way. Of course, we can get dependent types, too.

But note that I think this proposal holds its water even *without* the need to appeal to future extensions.

Let's now go through the other aspects of the proposals, using Iavor's numbering.

3. If we are avoiding punning, we need a way to talk about lists and tuples, separating types from terms. This proposal introduces a new way to do this. No type families are required, but the proposal includes a Tuple type family (taking a type-level list of types) as a convenience.

2. Users who wish to avoid puns may want to use a library that exports punned names. So the proposal allows you to qualify the types from an import separately from the terms. I agree that most users will want to import both types and terms, but by being able to separate the imports, users can qualify them separately, allowing easy disambiguation based on familiar module qualification.

1. Despite being the title of the proposal, the extended lookup is, for me, essentially an afterthought. It means we will produce more informative error messages when users write the name of a type in a term. The lookup extension really only starts to do something interesting after, for example, visible dependent quantification in terms is available. I'd be happy dropping this part of the proposal if it meets resistance.

Note that this proposal never suggests to move these warnings into the default set, and so users who like punning are free to do so for as long as they like. But it does give a nice nudge to our community to avoid this practice, which I think will improve the readability, searchability, and learnability of Haskell code.

Thanks for your consideration,
Richard

> On Jun 1, 2020, at 5:39 PM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> 
> Hello,
> 
> I am the shepherd for proposal #270, and it is time for the committee to review the proposal.  The discussion and the proposal are available here:
> https://github.com/ghc-proposals/ghc-proposals/pull/270 <https://github.com/ghc-proposals/ghc-proposals/pull/270>
> 
> Here is my summary of the proposal:
> 
> The proposal aims to solve the "namespace problem" which appears to largely be related to fact that Haskell has two namespaces, and so types and values may have the same name. 
> 
> Proposed changes:
>    1. Change the scoping rules for the language so that type names are in scope at the value level, but values always shadow types.
>    2. Add a new form of import, which can import only the names from a particular names space 
>    3. Change the way built-in syntax for tuples and lists works and deprecated ' and '' from DataKinds and TH respectively.   This is a bit elaborate, have a look in the proposal for details
>    4. Add a bunch of warnings that would trigger if you wrote code that made use of Haskell's different name spaces
> 
> My recommendation is that the proposal is rejected, as I don't think that these changes would help Haskell programmers, at least based on the way I use Haskell.  In particular, here are my thoughts on each of the above bullets:
> 
>    1. This is mostly about passing type arguments to functions---I would prefer a notation that is more explicit about the fact that we are passing in a type, and not just a normal argument.
>    
>    2. When I group things into modules, it is usually because they are intended to be used together.  I think I would rarely want to import only the types or only the values in a module, so I imagine it would be much more common to have to write two imports.
>    
>    3. This is quite an intrusive change, that is likely to break code.  I am also not keen to have to use type families, every time I want to use a tuple.
>    
>    4. Using the same name for a data constructor and a type is very common in Haskell.  I find it particularly useful when defining records.  I don't need warnings to let me know that I've done it, as it is highly unlikely that I did it on accident.
> 
> -Iavor
> 
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> 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/20200601/ed192ab7/attachment-0001.html>