[ghc-steering-committee] Scoping of types

[Spiwack, Arnaud]

Can you, maybe, summarize what the various options are? And their conflicts?

On Fri, Jul 30, 2021 at 11:53 AM Alejandro Serrano Mena <trupill at gmail.com>
wrote:

> 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.
>
> 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?
>
> Regards,
> Alejandro
>
> El 29 jul 2021 16:38:07, Spiwack, Arnaud <arnaud.spiwack at tweag.io>
> escribió:
>
>> 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).
>>
>> 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.
>>
>> On Fri, Jul 23, 2021 at 11:50 AM Alejandro Serrano Mena <
>> trupill at gmail.com> wrote:
>>
>>> Dear Committee,
>>>
>>> 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.
>>>
>>>
>>> *Current status*
>>>
>>> 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.
>>>
>>> > id :: forall a. a -> a
>>> > id x = f @a x
>>> >   where f y = y
>>>
>>> In the past 3 years we’ve accepted two proposals which extend this
>>> ability:
>>> - First to patterns
>>> https://github.com/ghc-proposals/ghc-proposals/pull/126, so we can
>>> write `id @a x = …`
>>> - Then to lambdas
>>> https://github.com/ghc-proposals/ghc-proposals/pull/155, so we can
>>> write `id = \@a x -> …`
>>>
>>>
>>> *What is going on*
>>>
>>> It seems that the accepted proposals were not quite right. We have two
>>> on-going proposals to *amend* the current ones:
>>> - https://github.com/ghc-proposals/ghc-proposals/pull/291 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).
>>> - https://github.com/ghc-proposals/ghc-proposals/pull/238 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
>>> https://gitlab.haskell.org/ghc/ghc/-/issues/16734#note_203412
>>> - https://github.com/ghc-proposals/ghc-proposals/pull/420 amends the
>>> current behaviour of signatures in patterns (what happens if I write `id (x
>>> :: a)` ).
>>>
>>> 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
>>> https://github.com/ghc-proposals/ghc-proposals/pull/291#issuecomment-726715932
>>>
>>>
>>> Note that this problem is arising in other places, too. For example
>>> #281, which adds visible `forall a -> ` (
>>> https://github.com/ghc-proposals/ghc-proposals/pull/281) is also
>>> talking about name resolution (see
>>> https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-884810016 for
>>> an example).
>>>
>>>
>>> *How should we proceed*
>>>
>>> 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.
>>>
>>> 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.
>>>
>>>
>>> Kind regards,
>>> Alejandro
>>> _______________________________________________
>>> 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/20210730/2c506568/attachment.html>