<div dir="ltr"><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, 29 May 2021 at 14:19, Vladislav Zavialov (int-index) <<a href="mailto:vlad.z.4096@gmail.com">vlad.z.4096@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">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 -> …`.<br>
<br>
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.”<br>
<br>
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.<br></blockquote><div><br></div><div>Admittedly I might be unfamiliar with a lot of the finer details here (I haven't been tracking the dependent types proposal closely), but 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?</div><div><br></div><div>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!).</div><div><br></div><div>Cheers</div><div>Simon</div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
- Vlad<br>
<br>
> On 29 May 2021, at 14:15, Simon Marlow <<a href="mailto:marlowsd@gmail.com" target="_blank">marlowsd@gmail.com</a>> wrote:<br>
> <br>
> 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.<br>
> <br>
> But the name resolution aspects concern me. I forsee a lot of confusion if we can't write `[Int]` as a type argument with the usual meaning. The error message is likely to be super confusing if it has to talk about the difference between a promoted list type and the usual list type constructor, which have the same syntax. I'm not a fan of having to write `List Int` when it's a visible type argument, but `[Int]` everywhere else.<br>
> <br>
> Would it be possible to require the leading quote to get the promoted meaning, otherwise defaulting to the usual meaning of `[Int]`?<br>
> <br>
> Also could we defer name resolution until type checking for things like `Proxy`, so that the obvious thing doesn't require namespace gymnastics?<br>
> <br>
> Cheers<br>
> Simon<br>
> <br>
> ghc-steering-committee mailing list<br>
> <a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
> <a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
<br>
</blockquote></div></div>