<div dir="ltr">Can you, maybe, summarize what the various options are? And their conflicts?<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jul 30, 2021 at 11:53 AM Alejandro Serrano Mena <<a href="mailto:trupill@gmail.com">trupill@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"><div><div dir="ltr">
Sorry, I was not clear about the goal of the message. This all stems from the fact that Joachim asked me to shepherd #238. However, when trying to do so, I found that this was not the only proposal changing some of the scoping of types, but that there’s a lot going on with regards to that field.</div><div dir="ltr"><br></div><div dir="ltr">My question to the Committee is: should we continue shepherding the proposals independently, or should we take some time to make a general judgment about how we want scoping to work on types, in the same way that we had a general Dependent Haskell proposal?</div><div dir="ltr"><br></div><div dir="ltr">Regards,</div><div dir="ltr">Alejandro</div><div dir="ltr"><br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">El 29 jul 2021 16:38:07, Spiwack, Arnaud <<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a>> escribió:<br></div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div dir="ltr"><div>I'm not sure what way forward you are suggesting (and judging from the lack of response, it's probably not clear for the other committee members either).</div><div><br></div><div>Philosophically, there is a balance to strike between backward compatibility and consistency. I'd note however that all of the existing behaviour is gated behind `ScopedTypeVariables`, which is fairly stable, but not necessarily unmovable. I don't think breaking backward compatibility would be unsurmountable.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jul 23, 2021 at 11:50 AM Alejandro Serrano Mena <<a href="mailto:trupill@gmail.com" target="_blank">trupill@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"><div><div dir="ltr">Dear Committee,<div><br></div><div dir="ltr">There’s a lot happening right now in the GHC proposals repo about scoping of types in different elements in the language. Richard asked for our decision in #238, but following a very good suggestion from Joachim, I think it’s better to give an overview on what’s going on. In my opinion, this should lead to a consolidation of the different proposals into a unified design.</div><div dir="ltr"><br></div><div dir="ltr"><br></div><div dir="ltr"><i>Current status</i></div><div dir="ltr"><i><br></i></div><div dir="ltr">In Haskell 2010 there’s no way to refer to type variables introduced in a type signature. For a long time, GHC has shipped with -XScopedTypeVariables, which introduced scoping for types by prepending them with `forall`. We could then use it in other types, or as part of a type application if -XTypeApplications is on.</div><div dir="ltr"><br></div><div dir="ltr">> id :: forall a. a -> a</div><div dir="ltr">> id x = f @a x</div><div dir="ltr">> where f y = y</div><div dir="ltr"><br></div><div dir="ltr">In the past 3 years we’ve accepted two proposals which extend this ability:</div><div dir="ltr">- First to patterns <a href="https://github.com/ghc-proposals/ghc-proposals/pull/126" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/126</a>, so we can write `id @a x = …`</div><div dir="ltr">- Then to lambdas <a href="https://github.com/ghc-proposals/ghc-proposals/pull/155" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/155</a>, so we can write `id = \@a x -> …`</div><div dir="ltr"><br></div><div dir="ltr"><br></div><div dir="ltr"><i>What is going on</i></div><div dir="ltr"><br></div><div dir="ltr">It seems that the accepted proposals were not quite right. We have two on-going proposals to <b>amend</b> the current ones:</div><div dir="ltr">- <a href="https://github.com/ghc-proposals/ghc-proposals/pull/291" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/291</a> proposes simplifications to type variable patterns. As I understand this would make type variables in patterns behave like term variables (cannot be repeated, occurrences in inner scopes shadow the outer one, and so on).</div><div dir="ltr">- <a href="https://github.com/ghc-proposals/ghc-proposals/pull/238" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/238</a> introduces -XTypeAbstractions, which make the combination of `forall` and `\@a` behave “as it should be”. But to be honest, I do not fully grasp the problems before, so neither how this amendment solves the problem; there’s a pointer to the GHC issue tracker where some incompatibility is discussed <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/16734#note_203412" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/issues/16734#note_203412</a></div><div dir="ltr">- <a href="https://github.com/ghc-proposals/ghc-proposals/pull/420" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/420</a> amends the current behaviour of signatures in patterns (what happens if I write `id (x :: a)` ).</div><div dir="ltr"><br></div><div dir="ltr">So we have different ways to introduce new type variables: `f :: forall a. …`, `f @a = …`, `f = \@a -> …`, `f (x :: a) = …`; and it’s very unclear what the scoping mechanism for each one should be. I think the problem is characterised very well in the following comment by Simon PJ <a href="https://github.com/ghc-proposals/ghc-proposals/pull/291#issuecomment-726715932" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/291#issuecomment-726715932</a> </div><div dir="ltr"><br></div><div dir="ltr">Note that this problem is arising in other places, too. For example #281, which adds visible `forall a -> ` (<a href="https://github.com/ghc-proposals/ghc-proposals/pull/281" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/281</a>) is also talking about name resolution (see <a href="https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-884810016" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-884810016</a> for an example).</div><div dir="ltr"><br></div><div dir="ltr"><br></div><div dir="ltr"><i>How should we proceed</i></div><div dir="ltr"><br></div><div dir="ltr">Personally, I am a bit worried about having divergent designs on this matter, and the fact that no fewer than 2 amendments are being proposed (!) For me, the best would be to come up with a unified design of how scoping works for types, covering all possible ways to introduce and resolve them. I am happy to help with this.</div><div dir="ltr"><br></div><div dir="ltr">Another important point seems to be how far we want to get from the current status quo (-XScopedTypeVariables make a type variable in a signature scope in its body, type variables in pattern signatures are always fresh), and how that fits with the overall -XDependentHaskell initiative.</div><div dir="ltr"><br></div><div dir="ltr"><br></div><div dir="ltr">Kind regards,</div><div dir="ltr">Alejandro</div></div></div>
_______________________________________________<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>
</blockquote></div>
</blockquote>
</div>
</div></div>
</blockquote></div>