Resurrect PatternSignatures

[nomeata]

Rendered

[nomeata]

Here is a user who was confused by having to use ScopedTypeVariables to get pattern signatures: https://stackoverflow.com/q/29395265/946226
And here is a (decade old) rant about this on haskell-cafe: https://mail.haskell.org/pipermail/haskell-cafe/2009-April/059519.html

[JacquesCarette]

The proposal I'm really looking for is the one that makes ScopedTypeVariables an official part of Haskell the language rather than some language option to turn on. Where would that one be?

[parsonsmatt]

@JacquesCarette I think anything that modifies "Official Haskell" is going to have to be wrapped into the next Haskell Report. I don't know how that process is going. I do agree that would be awesome.

[ocharles]

I believe that's outside the scope of this repository, that's really a haskell prime prosoal.

…

On Fri, 6 Apr 2018, 7:33 pm Jacques Carette, ***@***.***> wrote: The proposal I'm really looking for is the one that makes ScopedTypeVariables an official part of Haskell the language rather than some language option to turn on. Where would that one be? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#119 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AABRjiy5j2ojC5BBQBE5ADFcIrOzY9gkks5tl7TogaJpZM4TKQc9> .

[nomeata]

I believe that's outside the scope of this repository, that's really a haskell prime prosoal.

That’s correct. It might be that the Haskell Prime committee will consider ScopedTypeVariable to be “too big” or not uncontroversial enough; in that case I hope that at least the much more mundane PatternSignatures can become available by default.

[JacquesCarette]

Right -- https://prime.haskell.org/ticket/67 seems to be the ticket.

[gbaz]

That's actually the reason for my conservatism on this too. My feeling is this is all part of a class of "obviously these should be the default" extensions and having more granularity about them seems to be swimming against the stream, since it would be nicer to not have to add any of them at all :-)

[nomeata]

I am all for having both by default! But this discussion here is “what world to we want after the next GHC release”, not “what world do we want if Haskell prime happens”, which maybe much further in the future. Don’t let perfect be the enemy of good.

[JacquesCarette]

@nomeata Good point. +1 from me on this, for that reason.

[gbaz]

Don’t let perfect be the enemy of good.

Wait? Is this the ghc-proposals tracker? I must be lost :-P

[tomjaguarpaw]

Is there somewhere a proposal for -XOptionsWeAllLove which includes all of our favourite options? That seems like it would be a pragmatic approach for getting something accepted into the report.

[nomeata]

@tomjaguarpaw yes, #92

[AntC2]

Thanks @nomeata, it's not clear to me whether you're just complaining ScopedTypeVariables is a misleading name; or that you deliberately don't want type variable scoping but do want pattern signatures.

For myself, I find it far too confusing to give local signatures inside let/where or instance decls that have tyvars same named as the top level signature, but not being the same. So I always have ScopedTypeVariables switched on; and use distinct tyvar names in local signatures. Then this proposal is no use to me. (Arguably it was an omission in Haskell 98 not to scope type variables; so it shouldn't even need an extension, as @JacquesCarette says. Arguably also we should be able to put a type signature on any variable or pattern wherever it appears. Then would you be happy?)

If the complaint is just about a misleading name; well ghc extensions have lots of them. Perhaps "confused users" just have to get used to it?

[nomeata]

it's not clear to me whether you're just complaining ScopedTypeVariables is a misleading name; or that you deliberately don't want type variable scoping but do want pattern signatures.

Mostly the former.

Then this proposal is no use to me

Correct, everybody who uses ScopedTypeVariables will be unaffected. And I agree that both could reasonably be on by default – but that is discussion out of scope (heh) here.

Perhaps "confused users" just have to get used to it?

That’s what I thought 5 years ago, or so. But I still am regularly annoyed by it, so that does not seem to work :-)

[adamgundry]

That's actually the reason for my conservatism on this too. My feeling is this is all part of a class of "obviously these should be the default" extensions and having more granularity about them seems to be swimming against the stream, since it would be nicer to not have to add any of them at all :-)

I think PatternSignatures (as proposed here) "obviously" should be the default, but that ScopedTypeVariables should not. I'd much rather be able to bind type variables using explicit type abstractions (parallel to explicit type applications, cf. #96). Perhaps one day there will be an extension that allows me to! In the meantime, being able to turn on PatternSignatures alone would allow me to use them while knowing that my code does not rely on funky type variable scope rules. Thus I support this proposal.

[tomjaguarpaw]

Does anyone know the reason that PatternSignatures's behaviour is not default? Was it just an oversight in the original report or is there some more important reason?

[treeowl]

Let me be the dissenting voice. I always want ScopedTypeVariables. Anything that suggests to me that it is enabled without actually enabling it leads me to confusion and wasted type-debugging time. Without this proposal, seeing a pattern signature is proof positive that my type variables are scoped. With it, it's just as confusing as ExplicitForAll. I understand some people think we should have explicit type abstraction instead. I think they're probably right, in the absence of explicit type application. But in the presence of explicit type application, I would have to jump through even more hoops to avoid signaling to users that my function has an intentional explicit type application interface they can count on.

[tomjaguarpaw]

@treeowl Let me see if I understand you correctly. You are against an extension to enable syntax like

let x :: Int = 0

because you currently use the presence of such syntax to deduce that ScopedTypeVariables is on?

[treeowl]

@tomjaguarpaw, it's not that I do so intentionally. But I probably do so subconsciously, so I predict this change would make me more likely to get confused. I'm not actually dead-set against the proposal, but I do think the proposal text should include the potential for confusion in the appropriate section. I'd also like to see more discussion of how we can get the power we want from TypeApplications and ScopedTypeVariables without the wild API flux of the former or the potential confusion in the latter over what is being bound vs. what is being specified. I don't know whether this is the appropriate place for that discussion.

[simonpj]

The "proposed spec" says

The language extensions PatternSignatures is no longer deprecated. If enabled, it allows all signatures on patterns that do not bind type variables.

What does that mean? Suppose I have with -XPatternSignatures but not -XScopedTypeVariables. If I write

f (x :: [a]) = b.ah

is that allowed or not-allowed? Perhaps it is allowed, but does not bring a into scope? Please say.

[nomeata]

It’s not allowed. I clarified the proposal.

[simonpj]

It’s not allowed. I clarified the proposal

Why not? It seems like a free design choice to allow or not-allow. And not-allowing means you simply can't use a pattern signature in places you might really want to.

[nomeata]

this point is too marginal to have a long discussion about.

Changed my mind :-]

For one target audience of this extensions (confused beginners who want to add type signatures to every subterm, whether left or right of the =, to hunt down type error) the rules around type variables in patterns are certainly far too confusing. Also, it would be strange to forbid

id :: a -> a
id x = (x :: a)

but allow

id :: a -> a
id (x :: a) = x

I feel that rejecting a program with a message that essentially says “you are doing something non-trivial, please use ScopedTypeVariables like the grown-ups” is going to be more helpful than doing something that only people understand who want ScopedTypeVariables anyways.

[simonpj]

I believe that you are proposing: with -XPatternSignatures and without -XScopedTypeVariables, no pattern signature can mention any type variables.

My judgement differs, but it's just an opinion. It would be good to hear from others, please.

What about this

f :: Proxy Any -> blah
f (x :: Proxy Any) = ...

Is that OK? Because that pattern signature does have some (invisible) kind variables. The real type of f is

f :: forall {k}. Proxy (Any :: k) -> blah

So is that allowed or not allowed? If we didn't have the no-free-var restriction, the question doesn't arise.

[goldfirere]

It sounds to me like the best way forward is to treat pattern annotations exactly like expression annotations, where any type variables are locally bound by a forall. This effectively renders type variables in patterns useless, but it's at least a consistent place to stand.

This is option (1) from #119 (comment)

[nomeata]

Is that OK? Because that pattern signature does have some (invisible) kind variables.

Hence my phrasing: “Does not bind type variables”. It is a pure renamer check: Is there a type variable in the pattern that is not already in scope? Then the program needs ScopedTypeVariable! No need to wait for the type checker to decide that, and the type checker code is unaffected by this proposal.

(I guess without ScopedTypeVariables there is really never ever a type variable in scope in a pattern… at some point I believed that in type classes their type variables are in scope, but I was wrong … anyways, if someone finds a way to have a type variable in scope, then an occurrence of such a variable would be allowed.)

It sounds to me like the best way forward is to treat pattern annotations exactly like expression annotations, where any type variables are locally bound by a forall.

I see the consistency, but it would be incompatible with ScopedTypeVariables, which is, I believe not helpful.

But still thanks for your point, because the contention only supports the plan to pass such programs right back to the user for clarification :-)

[treeowl]

My concern is magnifying. The proposed extension offers very little power, and there's a tremendous amount of disagreement about what exactly it should mean. If this gets added, someone will have to work out how each new (and more powerful) feature needs to interact with it. My general thinking is that having an extension like this that supports completely monomorphic signatures (no type variables) should be acceptable. Beginners will be able to use that without any trouble, and everyone else can just ignore it. Once type variables come in, my vote goes from "don't care much" to "please don't".

[simonpj]

It sounds to me like the best way forward is to treat pattern annotations exactly like expression annotations, where any type variables are locally bound by a forall

(I assume you mean with -XPatternSignatures but -XNoScopedTypeVariables. ) No, we definitely could not do what you suggest, because the meaning would change radically when you switched on -XScopedTypeVariables. That would be truly gruesome. Joachim's proposal that a pattern signature cannot mention any type variable not already in scope is less terrible.

I'm inclined to agree with David -- it's really not worth the effort to make the distinction between these two extensions.

[nomeata]

David says

My general thinking is that having an extension like this that supports completely monomorphic signatures (no type variables) should be acceptable.

which is what the proposal currently says!

Well, not quite: it says “binds no type variables“, which amounts to, and could be rephrased as, ”has no free type variables”. This intentionally allows (x :: forall a. a -> a), which is useful with RankNTypes:

Prelude> :set -XRank2Types  -XPatternSignatures
Prelude> let foo (reorder :: (forall a. [a] -> [a])) = reorder "hello"
Prelude> :t foo
foo :: (forall a. [a] -> [a]) -> [Char]

But I assume this part is uncontroversial.

Are we in agreement that PatternSignatures without ScopedTypeVariables ought not have any free type variables.

[simonpj]

Are we in agreement that PatternSignatures without ScopedTypeVariables ought not have any free type variables.

No -- I argue that PatternSignatures should have precisely the same semantics as today, except not bringing type variables into scope. That way the two are 100% orthogonal.

But that's just my opinion.

[AntC2]

I am by now pretty much baffled by what it is that's proposed. I can see there's no consensus. Does the write-up at least represent @nomeata's current thinking? Restricting to only monomorphic signatures (no type variables except for RankNTypes) represents really little gain.

If we're worried about "confused beginners" who want to understand the type for every sub-term, I would expect at least some of those sub-terms might be polymorphic (so what's proposed can't help them?); and/or they'd like to put wildcards _ so ghc can tell them what it has inferred. (Currently requires ScopedTypeVariables.)

Then I'm looking at option 1 above

1. foo (x :: a) = … is interpreted like a signature on the RHS: Every type variable is abstracted over inside the pattern, i.e. equivalent to foo (x :: forall a. a) = … (with ExplicitForAll)

[ BTW re "signature on the RHS" I don't follow why a explicit forall on the overall RHS expression signature is needed to trigger ScopedTypeVariables for signatures inside the expression. Is that some hangover from the original design for backwards compatibility? Do we still have to worry about it some 10 years on? ]

take 1. with @goldfirere's comment

let's figure out how to bind type variables in arbitrary patterns,

So we want any tyvar introduced in a pattern binding to scope over the rhs:

foo (x :: aa) = ... (... :: aa) ...

To avoid confusion with what happens under ScopedTypeVariables, we'd better say any such tyvar must not be already in scope -- which is why I've written as aa.

And I think the explicit forall's scope given in option 1 is wrong. (That tight scope is useless, as others have noted.) The effect we want is (making up some illegal syntax)

(foo :: forall aa. aa -> ... aa ...) x = ...                  -- or
foo :: forall aa. aa -> ... aa ... where
  { foo x = ...
  ; -- other equations for foo    
  }

Note there might not be an explicit signature separately given for foo. If there is, all we're doing is providing an alpha-renamed version. (And typechecking it.)

Re @simonpj's last comment

I argue that PatternSignatures should have precisely the same semantics as today, except not bringing type variables into scope.

I'm afraid I've forgotten (if I ever knew) what is the precise semantics for PatternSignatures that is distinct from the semantics for ScopedTypeVariables. Was there ever a paper or a more formal write-up beyond what's in the User Guide?

A(nother) small plea arising from "confused beginners": they learn that all signatures in effect have a forall binding their free tyvars, but it's not usually needed to put explicit forall. Then they are surprised that with ScopedTypeVariables the explicit forall on a function signature (or RHS expression) changes the semantics of the program.

With PatternSignatures binding tyvars I can see value in the proposal:

• beginners can put tyvars on patterns as well as putting monotypes, and put wildcard _, no surprises;
• beginners can avoid writing explicit forall;
• the tyvar bindings are lexically right there decorating the equation, no need to scan up to some function signature or instance head to find out where the tyvar comes from -- oh and remember to check whether there's explicit forall -- oh and remember class and instance heads don't need explicit forall;
• the tyvar binding (which might be inside a pattern match) is consistent with binding for tyvars in existential data constructors, thus addressing the "If all this seems a little odd, ..." comment in the User Guide 10.16.4.

[nomeata]

The proposal doesn’t seem to receive support in the committee anyways, so this discussion somewhat futile now, but I am happy to address some your points (if I understand them correctly, I am notsure)

Because of

Then they are surprised that with ScopedTypeVariables the explicit forall on a function signature (or RHS expression) changes the semantics of the program.

I want to forbid pattern signatures that have free type variables, and have the compiler tell the user “Either close the type signature with forall a., or add ScopedTypeVariables, to disambiguate”.

If PatternSignatures treats free type variables in the same way as ScopedTypeVariables, then it just a synonym for ScopedTypeVariables (status quo). If it treats them differently, then it is not compatible, which would be bad.

[AntC2]

The proposal doesn’t seem to receive support in the committee anyways, ...

Thanks @nomeata. As the proposal currently stands, I'd agree it has low power to weight. I was looking for a way to give more power (and particularly thinking of helping "confused beginners").

Then they are surprised that with ScopedTypeVariables the explicit forall on a function signature (or RHS expression) changes the semantics of the program.

I want to forbid pattern signatures that have free type variables, ...

One of your complaints was that ScopedTypeVariables is a misleading name when you only want to put pattern signatures. Then PatternSignatures is a misleading name if you can't put pattern signatures with tyvars -- as you can usually in a signature.

If PatternSignatures treats free type variables in the same way as ScopedTypeVariables, then it just a synonym for ScopedTypeVariables (status quo). If it treats them differently, then it is not compatible, which would be bad.

I think I've steered a course between Scylla and Charybdis: this is not status quo, because I suggest binding fresh tyvars by introducing them in pattern signatures. (I suspect a lot of the use cases for ScopedTypeVariables can be written this way without needing explicit forall on some distant signature.) It is compatible with/orthogonal to ScopedTypeVariables/explicit forall because tyvars introduced this way must be fresh/not already in scope.

[nomeata]

Then PatternSignatures is a misleading name if you can't put pattern signatures with tyvars -- as you can usually in a signature.

Oh, you still can; you just have to put in the forall’s to clarify your intent (I see the argument for implicit quantification in patterns; it would be a straight analogue to type annotations in terms, but – to me – compatibility with ScopedTypeVariables trumps that argument.)

I suggest binding fresh tyvars by introducing them in pattern signatures

ScopedTypeVariables support precisely that! With ScopedTypeVariables, if you use a type variable in a pattern that is not already in scope, it will be brought into scope right there. It sounds like you were proposing that behavior? (If not, maybe you can give concrete code examples of what you are proposing?)

[AntC2]

Oh, you still can [put pattern signatures with tyvars]; you just have to put in the forall’s to clarify your intent

? Your option 1. above shows f (x :: forall a. a) = ..., in which a is useless because it's not scoped to rhs of the =. (Or if it is, that's not said anywhere.) You do allow forall for a RankNType, which is somewhat more useful.

If we're thinking about "confused beginners", putting explicit forall is what they find confusing. (And if they're using RankNTypes (or existentials) they're not beginners.)

Then it appears I've been labouring under a misunderstanding. Thank you for pointing this out:

I suggest binding fresh tyvars by introducing them in pattern signatures

ScopedTypeVariables support precisely that!

OK. Then I'm proposing that bit of ScopedTypeVariables (additional to your proposal) be included in PatternSignatures -- good! So it is compatible.

What's confused me is the User Guide 10.16.4 saying "pattern type signatures are not implicitly generalised. The pattern in a pattern binding may only mention type variables that are already in scope." It goes on to discuss binding for existentials: "in this situation (and only then)" is just false. "If all this seems a little odd, ..." that I quote above is just false. Neither the User Guide nor your proposal have any dead-simple examples like:

-- no signature for bar, baz; aa is not in scope
bar (x :: aa) = x :: aa        -- } no explicit forall
baz (Just (y :: aa)) = y :: aa -- } currently only valid with ScopedTypeVariables [Note **]

-- it does no harm to put signatures for bar, baz, but the tyvars don't scope over their equations

And your comment -- my bar is your id in that comment -- is also warning against odd behaviour.

With ScopedTypeVariables, if you use a type variable in a pattern that is not already in scope, it will be brought into scope right there. It sounds like you were proposing that behavior?

Yes. Hooray! Where is that behaviour described? And why wouldn't you want it included under PatternSignatures?

So I'm proposing PatternSignatures (in the absence of ScopedTypeVariables) does not imply ExplicitForall -- but neither does it contradict that.

[Note **] I'm getting weirded out: that bar, baz appears to be valid in Hugs (and works). Does that mean it's H98 and ghc is not compliant? No I don't think so. If it's in Hugs, I rest my case about "confused beginners".

ADDIT: Heh, heh. In fact this technique of putting tyvar pattern signatures works in Hugs for all of the examples in the ghc User Guide on ScopedTypeVariables. So you don't need the confusing forall. See Hugs extensions 7.3.3, 7.3.4. So my variant of the 'Resurrect PatternSignatures Proposal' amounts to: please follow Hugs.

[nomeata]

This proposal was rejected for insufficient merit.

[goldfirere]

Just in case anybody ever wanders back here: I just wanted this feature.

I'm writing a Haskell application which I will use in a class that teaches a very limited amount of Haskell. For it to actually get work done, I sadly need a stack of monad transformers. I won't be requiring students to edit that code, but I want some guidelines for the intrepid. At one point, I have

  result <- flip evalStateT initialState $ runMaybeT $ runExceptT $ runMyMonad thing_inside

Even I go cross-eyed on that line. So I modified it to be

  result :: Maybe (Either String ())
         <- flip evalStateT initialState $ runMaybeT $ runExceptT $ runMyMonad thing_inside

Much better -- now I know what I'm working with. But silly GHC won't accept this without -XScopedTypeVariables. I certainly don't want scoped type variables for this. But, today, I get them whether I want it or no. And now, my students may see that extension and get more than they bargained for. (Though, perhaps, if they're bargaining with a stack of monad transformers, they've already lost the bargain.)

I'm not trying to reverse a decision, but just laying out an additional use case I just ran into for posterity.

[nomeata]

Yeah … precisely my thinking. Maybe we can sneak this in as part of a more general splitting of ScopedTypeVariable into individual features as discussed at #155.

[AntC2]

... or persuade that PatternSignatures should always have been part of the language, and get it into the Haskell 2020 standard.

[nomeata]

... or persuade that PatternSignatures should always have been part of the language, and get it into the Haskell 2020 standard.

That was my other motivation: By giving the extension a name in the first place we can talk about it on the way to a new standard.