[ghc-steering-committee] Scoping of types

[Alejandro Serrano Mena]

 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/7f4c48aa/attachment-0001.html>