[ghc-steering-committee] Type applications in patterns

[Iavor Diatchki]

Hello Simon,

I think that the consistent choice would be "(A) like pattern signatures".
 I think this would ensure that all types in patterns handle variables in
the same way.  It would be confusing to me if the following two examples
ended up doing different things:

h1 (Nothing :: Maybe [p]) = ...
h2 (Nothing @[p]) = ...

-Iavor



On Fri, Nov 13, 2020 at 3:30 AM Simon Peyton Jones via
ghc-steering-committee <ghc-steering-committee at haskell.org> wrote:

> Dear Steering Committee
>
> You may remember that we approved the Type Applications in Patterns
> <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0126-type-applications-in-patterns.rst>
> proposal, some time ago.  Cale has been implementing it (see ticket 11350
> <https://gitlab.haskell.org/ghc/ghc/-/issues/11350> and MR 2464
> <https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2464>).    It’s
> nearly done.
>
> But in doing so, one design choice came up that we did not discuss much,
> and I’d like to consult you.
>
> Consider first the *existing* pattern-signature mechanism (not the new
> feature):
>
> data T a where
>
> MkT :: forall a b. a -> b -> T a
>
>
>
> f1 :: forall p. T [p] -> blah
>
> f1 (MkT (x :: a) pi) = blah
>
>
>
> f2 :: forall p. T [p] -> blah
>
> f2 (MkT (x :: p) pi) = blah
>
> In f1, the pattern (x :: a) brings ‘a’ into scope, binding it to the type
> [p].  But in f2, since p is already in scope, the pattern (x :: p) does not
> bring anything new into scope.  Instead it requires that x have type p, but
> actually it has type [p], so f2 is rejected.
>
> Notice that a pattern signature brings a new variable into scope only if
> it isn’t already in scope.  Notice how this differs from the treatment of
> term variables; the ‘pi’ in the pattern brings ‘pi’ into scope
> unconditionally, shadowing the existing ‘pi’ (from the Prelude).
>
> OK, now let’s look at the new feature. Consider
>
> g1 :: forall p. T [p] -> blah
>
> g1 (MkT @a x y) = blah
>
>
>
> g2 :: forall p. T [p] -> blah
>
> g2 (MkT @p x pi) = blah
>
>
>
> *Question*: should the variables free in these type arguments be treated
> like pattern signatures, or like term variables?
>
>    1. *Like pattern signatures*.   In this design, in g1, ‘a’ is not in
>    scope, so this brings it into scope, bound to [p].   But in g2, ‘p’ is in
>    scope, so this is rejected (because MkT is instantiated at [p] not p.
>    2. *Like term variables*.  In this design, all the variables free in
>    type patterns are fresh, and brought into scope. In g2,  a new ‘p’ is
>    brought into scope, shadowing the existing ‘p’; indeed the new ‘p’ is bound
>    to [old_p].
>
> The original paper, and hence the accepted proposal, adopts (A).   But
> Cale likes (B).  Indeed John Ericson wrote a Proposal 291: simplify
> scoping for type applications in pattens
> <https://github.com/ghc-proposals/ghc-proposals/pull/291> to advocate
> this change.  (The proposal is not easy to understand, but advocating (B)
> is its payload.
>
> This is not a terribly big deal, but it would be good to settle it.
>
> The right place to have debate is on Proposal 291
> <https://github.com/ghc-proposals/ghc-proposals/pull/291>.  This email is
> just to alert you to it, and ask for your opinions.
>
> Simon
>
>
> _______________________________________________
> 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/20201113/d9bf1ba7/attachment-0001.html>