[ghc-steering-committee] Type applications in patterns

[Eric Seidel]

Like I said in the discussion, I find it a bit strange to treat @ as an explicit binder as part of a data pattern period. The type should be bound as an earlier standalone pattern, where the signature dictates it should appear.

I guess you would respond that in the world of dependent types it's natural to think of the type parameters as being just as much part of the scrutinee as the value parameters, but this still feels.. off to me somehow. I think one reason is that case analysis is a runtime thing and types are erased, so why are we binding parameters that aren't actually there at runtime and can't be relevant? But more importantly, the way we use type parameters is different from how we use value parameters, even in a dependently-typed setting. Values we bind and compute on, exclusively. But types are also used to guide type checking, and we lose some of our ability to do that with option (B). Maybe doing this in patterns is not all that useful in practice, but it is pretty deeply ingrained into my mental model of how types behave in Haskell.

There is another option for unifying the behavior of type and value parameters in patterns, make values more like types. That is, allow repeated occurrences of term variables in patterns, with the semantics that the pattern only matches if the values are the same. This could be implemented as a trivial desugaring

  f x x = e  ~>  f x x' | x == x' = e

and it would give the surface language a nice extra declarative feeling.

On Mon, Nov 16, 2020, at 16:37, Richard Eisenberg wrote:
> This thread was one of the reasons I posted 
> https://github.com/ghc-proposals/ghc-proposals/pull/378, which 
> advocates for accepting #291 (again, with significant changes to 
> clarify the text).
> 
> I thus think that the better choice would be "(B) like term variables", 
> as I hope for there not to be a distinction between types and terms in 
> the future.
> 
> I admit that (B) is less expressive than (A) and would welcome a 
> proposal allowing for parameterized patterns that can take inputs as 
> well as producing outputs -- among both terms and types.
> 
> Richard
> 
> > On Nov 13, 2020, at 11:10 AM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> > 
> > 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
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> 
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>