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

[Richard Eisenberg]

> 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/0000-dependent-type-design.rst#431status-quo>) 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210601/de55adf3/attachment-0001.html>