Need feedback on pattern signature behavior

#1

Hi Haskellers, In the conversation for GHC Proposal #608 I am making some claims on what is popular / what people prefer regarding pattern synonyms. It’s hard to substantiate those claims so therefore I ammaking a poll to get to the bottom of things :).

For background, GHC proposal #448 is the master plan of an effort to make an alternative to ScopedTypeVariables, which fixes a few issues. On a few occasions, we’ve made new proposals to modify it based on experience in other proposals and experience implementing it. GHC Proposal #608 is one of those proposals.

#448 is reintroducing PatternSignatures (which does not currently exist, but use to) in order to enable just that feature without the rest of ScopedTypeVariables. The question is whether that minimized extension should include the implicit binding functionality of pattern signature variables we have today (described below) or not.

(Also, an important disclaimer: we are well aware that ScopedTypeVariables is one of the most popular and widely-used extensions today. For those of you worried about breaking changes, no one is advocating them / we actually get rid of ScopedTypeVariables — it is easy to support it and old code using it indefinitely. So don’t worry about breakage.)

OK, now for the question itself.

Today, in code like

f (_ :: x) = ...

the x inside the pattern signatures can be either a use of an x bound in an outer scope, or a fresh binding of x if no such x is bound in an outer scope.

Note that originally this was added because it it was the only way to bind existential type variables, but now we have a new way with @ which is an explicit binding construct.

The question is do people like this?

  • Don’t care, I don’t use pattern signatures so it doesn’t affect me.
  • Don’t care, I do use pattern signatures but I still don’t care.
  • No, I don’t like implicit bindings, I want to look at code and always know whether something is binding or using variables without consulting surrounding code. If I need to bind a type variable I will instead use @ and write something like
    f @x (_ :: x) = ...
    (the @x binds the variable, the second x uses that bound variable.)
  • Yes, I do like implicit binding. I don’t want to have to use this @... syntax to bind type variables.

0 voters

2 Likes
#2

I’m coming across this a lot these days and I’d really like explicit bindings. It would make so much sense when taken in the context of TypeApplications and type variable bindings in GADT pattern matches.

EDIT: @Ericson2314 Is there some where I should be commenting if I want to make the case that explicit @ type bindings are the way forward? Pretty much every day recently I want that over implicit bindings through type signatures on variables.

2 Likes
#3

Yes Amend #448 so `-XPatternSignatures` does not include implicit bindings by Ericson2314 · Pull Request #608 · ghc-proposals/ghc-proposals · GitHub

Do note we’re getting @... bindings regardless. The question is with @... existing what should a new PatternSignatures language extension include. There are some very subtle interactions with singled namesapce / “Dependent Haskell” in favor of no implicit binding with PatternSignatures that the conversation discussed; I left those out of the poll because I think it’s better to ask the crowd on current pain/pleasure than more hypothetical situations.

#4

Just to clarify, with implicit binding

f (x :: y) = x :: y

is well typed but would not with explicit typing (because the y do not refer to the same type).
If so I am for implicit binding, because I don’t understand why the two xs are the same but two ys are not. Put it another way, why would someone use y (the second time) but expect it to be different from the first one.

NB : I have never used PatternSignatures because I didn’t know I could. But I have been needing it and I will use it now.

#5

Good point. I voted ‘I do like implicit binding’; which doesn’t mean I would avoid @... or would object to others using it; but sometimes @... is awkward to use, I’d prefer implicit binding. (See an example which uses both modes on my recent post to the github thread.)

It might be worth noting the swag of proposals is also reintroducing [**] result signatures, so @maxigit’s example could go

f (x :: y) :: y = x 
--         ^^ result type on LHS

At the moment in GHC, PatternSignatures does the same as -XScopedTypeVariables, so you’ll get a warning PatternSignatures is deprecated. The chief purpose of -XScopedTypeVariables is for explicit forall in the standalone signature to scope its type variables over the equations for the function, so in f :: forall y. y -> y; f (x :: y) = ..., the :: y would be a usage not a fresh binding.

[**] That is, reintroducing from over a decade ago.

#6

I meant I didn’t know that one could write s :: String <- ... with the scoped variable extension.

#7

I think the reason it would be rejected with explicit binding is that y would simply be out of scope, not that the two ys are different. If there was a y in scope then it would be well-typed, e.g.:

g :: forall y. y -> y
g = f where
  f (x :: y) = x :: y

That should be accepted with both implicit and explicit binding.

1 Like
#8

That’s the same, the first y and the second y don’t refer to the same thing. In effect there are two ys, the first one and the second one.

Having y in the type signature defeat the object of the pattern signature.

#9

I mean both ys are out of scope. I don’t think it makes much sense to say they don’t refer to the same thing, because they don’t refer to anything.

If you think the only purpose of a pattern signature is to bind a new variable then yes, but I don’t agree. Pattern signatures can also just be used to specify the type of the argument using a known name. For example you could also write this:

g :: forall y. y -> y
g = f id where
   f (id' :: forall z. z -> z) x = id' x

You won’t be able to write that without a pattern signature. You could also do it with a type signature on f, but then you’d also need to explicitly state the type of x and the return type of f.

2 Likes
#10

@maxigit Yes the old way of having to use another type signature to bind the variable was subpar, but that is why we are getting @. The new way to write a fully explicit id function without a standalone type signature is

id @a (x :: a) = x :: a

both a in signatures are uses not binds; the general situation for church-style lambda calculi has always been that when we introduce a variable, we give it a type using only already-bound variables, whether this is with \(x :: Int) -> ... or (x :: a) -> ... (polymorphic type variables like a and ground types like Int have the same scoping rules in a simpler language).

The @a binds the a because unlike the other as, it is a pattern, rather than merely being used in a pattern.

1 Like
#12

So, does implicit binding mean that the @a is not necessary?

I understand the reason why it might be necessary but it feels strange that the first x and the first a behave differently. Remembering why seem a unnecessary cognitive burden.

#13

You’re always going to have that inconsistency, because you can’t pattern match on types. For example:

data A = B

f (B :: A) = ...

Here B is a pattern, but A is a constructor.

I find it easier to have a mental model where all types are always constructors, rather than having some types that behave a bit like pattern matching sometimes.

1 Like
#14

@maxigit

I understand the reason why it might be necessary but it feels strange that the first x and the first a behave differently. Remembering why seem a unnecessary cognitive burden.

Also consider this:

id @a = id2 where
   id2 (x :: a) = (x :: a)

both a after the :: are uses in this case, the @a is above, part of a separate definition. I wouldn’t mean the :: a in patterns binding if it was always that case, but as you can see it is not. As @jaror shows for upper-case identifier it is always a use, and as we both showed, it is also not the case for lower-case identifiers when the variable is in scope.

The new world I am hoping to get too has this simple model:

  • If it’s to the right of a :: it is always a use
  • if it is to the left of a ::, or there is no :: it depends:
    • if it is an expression (positive position) it is always a use
    • if it is a pattern (negative position) it is always a bind

This makes for:

  1. a more rigid expression-pattern duality — it doesn’t apply to as much stuff (not to the right of the ::) but where it does apply it always applies, no funny corner cases!
  2. the rules are strictly local, no outer scopes / enclosing code needs to be consulted to understand what each bit of code means.
1 Like
#15

I don’t mean in general, I mean in the example you gave

The forall and the pattern signature are redundant.

#16

How is it simpler than “the first occurrence is a bind, everything else is a use”. This is the case for variable and also type signature, e.g. a -> b -> b. Or maybe this notion of bind and use is artificial and what matters is that all a are referencing the same thing. This is the way I’ve been thinking of binding until now.
However I am not an expert so I am probably missing something.

That the bit I really don’t get. How is it a problem in practice ? In (x :: a) = x :: a, that doesn’t pose a problem to anybody to have to look at the first x to understand the second x, so why is it a problem for the as ???

Why can’t the scoping rules be the same for type and value ?

#17

Yes this is an important objective for me; and is the main reason I’m unhappy with the forall in a distant stand-alone signature scoping over the equation. (For one thing it means that signature isn’t stand-alone, maybe doesn’t mean the same as a version without forall; but maybe does mean the same, depending whether the forall'd tyvars show up amongst some equation.)

We already get enough complaints (including very recently) that Haskell is too purist/academic. Then do I need to read Church before I’m allowed to use Haskell? You can write perfectly good Haskell with no lambdas at all. (And “general” lambda binds terms only, not types.) So following some arcane academic theory is no objective for me.

Then my mental model is:

f (x :: a) = ...

Binds the term var x and binds the type var a at the same time at the same place.

f2 (x :: Maybe a) (y :: a) :: Either a b = ...

Binds two term vars and the type var at the same time in the same place. The theorists can worry whether the appearances of a are bindings vs usages. And the b must also be a binding, from its position – which is why I’m keen to support result type sigs.

Decorating with @... then doesn’t avoid the need for signatures and is just clutter. (I’m not objecting if people want to clutter up their code.)

2 Likes
#18

Yeah, all examples I’m giving are simplified. I hope it is possible to imagine real world scenarios which are not redundant. Of course you could object that those don’t exist or are not common enough, but that is a lot harder to prove or disprove.

3 Likes
#19

In the case of a top-level binding, yes. But the rules are non-local if you consider local bindings, e.g.:

data X = X
data Y = Y

g :: X -> (X, X)
g (_ :: a) = (f X, f Y) where -- error: Could not match expected type 'X' with actual type 'Y'
  f (_ :: a) = X -- reuses the existing binding

h :: X -> (X, X)
h (_ :: b) = (f X, f Y) where -- works
  f (_ :: a) = X -- binds a new variable

Now the type of the f inside g is X -> X and the type of f in h is a -> X. So whether the type variable a is in scope or not, which may be determined by some code far away in a real world scenario, influences the type of f (_ :: a) = X.

Requiring explicit bindings avoids this spooky action at a distance.

I totally agree with this, but I feel this is a separate matter.

1 Like
#20

Is distant stand-alone signature in commond (and good ) practice?

#21

Note that “the first occurrence is a bind” is not how value bindings work. Value bindings have to be linear (no two variables with the same name in the same binding group) and inner bindings shadow outer bindings if they have the same name.

Neither of those two properties hold for implicit binding of type variables (as currently implemented in ScopedTypeVariables), and in my opinion for good practical reasons as long as we don’t have explicit bindings.

However, we can get both properties back if we exclusively use explicit bindings, which will be possible with the TypeAbstractions extension in the future.

2 Likes