# Need feedback on pattern signature behavior

**URL:** <https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704>\
**Category:** Uncategorized\
**Created:** [September 27, 2023, 4:27pm UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704 "2023-09-27T16:27:45Z")\
**Posts on this page:** 14\
**Page:** 2

<div class="post-metadata">

**Author:** ![Ericson2314](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/ericson2314/32/1026_2.png) [@Ericson2314](https://discourse.haskell.org/u/Ericson2314)\
**Post date:** [September 29, 2023, 5:03pm UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/35 "2023-09-29T17:03:02Z")

</div>

> [@maxigit](#):
>
> I have one more question then. If the signature is `forall a. a -> a` then the previous code should be strictly equivalent to `(x -> x) :: forall a. a -> a`.

I think you meant `(\x -> x) :: forall a. a -> a`? Yes it is equivalent, one is just more “filled in”.

> [@maxigit](#):
>
> So will both version accept the _optional_ parameter even though it doesn’t appear anywhere in the second version?

Not sure what you mean, do you mean `\ @_ x -> x`? That _might_ be accepted in some contexts. There are some type checking questions unrelated to name resolution to work out, however.

> I am interested in the concepts / theory but not when I am actually programming (i.e. I don’t want to have write `@` everywhere just to satisfy my theorist side).

OK!

> That the bit I I still don’t understand but I’ll trust you on that. If it is necessary, then it is. I’m still voting for implicit parameter and I think you understand my reasoning.

I just want to emphasize that optional != leaky implementation detail. There is no real upper bound to how much of your program a clever language implementation might be able to figure out / guess on it’s own. The point of this explicit stuff isn’t that _GHC_ is lost and confused, but that the _human_ might be lost an confused. Of course, this is a matter of opinion.

It is fine if you continue to like it :).

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 30, 2023, 1:13pm UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/37 "2023-09-30T13:13:43Z")

</div>

> [@maxigit](#):
>
> Fair enough, but `id2` signature is only `forall a . a -> a`, which only have one parameter.

`forall a.` is a parameter. To elaborate, the full type is `forall (a :: Type). a -> a`, which is why when calling `id2` you first (optionally) apply a type, and then a value _of_ that type.

> Therefore I should also be able to call `id1` with 2 parameters (`id1 @int 3`) even though `id1` never mentioned any optional parameter ?

You can.

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [September 30, 2023, 8:08pm UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/38 "2023-09-30T20:08:24Z")

</div>

Seems to me there’s a difference here between two schools of thinking. There’s an older school in which `->` is a type constructor, `=>` is syntax used to introduce a constraint, `forall _.` is a universal quantifier, and all of these things are distinct and unrelated ways to form types out of simpler types. The word ‘application’ is strictly used to denote a term combining something that can be subsumed by a type formed with the `->` type constructor, and something that can be subsumed by the first argument to that type constructor. ‘Type applications’ are their own thing, analogous but conceptually separate. Instance resolution isn’t even spoken of in the same breath.

Then there’s a newer school, influenced if not driven by dependent type theory, in which `->`, `=>`, `forall _.`, and the prophesied [`forall _ ->`](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) are all ‘quantifiers’ with different properties like ‘visibility’ and ‘relevance’. Those properties determine whether and how one may provide a parameter when using a term of that type in order to eliminate the quantifier. For some combination of backwards-compatibility and convenience, the `forall _.` quantifier can be inferred if not explicitly present in a type, but regardless of whether it is inferred or explicit, it introduces a parameter (invisible, irrelevant) just like `->` introduces a parameter (visible, relevant).

One doesn’t need to learn dependent type theory to switch gears into the new school (‘dependence’ is a property orthogonal to ‘visibility’ and ‘relevance’, AIUI), but it does represent a shift that was pretty surprising to me when I learned about it, and people educated under the old school might need some pointers when people who have adjusted to the new school use the word ‘parameter’ in its newer, more expansive sense.

Using `@` to explicitly bind type parameters is definitely of a piece with the new school—all parameters are parameters, and the `@` is just a visibility marker—and I support it, but I’m also not surprised that people who haven’t made the shift find it jarring.

---

<div class="post-metadata">

**Author:** ![Ericson2314](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/ericson2314/32/1026_2.png) [@Ericson2314](https://discourse.haskell.org/u/Ericson2314)\
**Post date:** [September 30, 2023, 9:29pm UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/39 "2023-09-30T21:29:50Z")

</div>

@rhendric I think that’s exactly right. I want to make the more limitted`-XPatternSignatures` better for the “new school”, and I don’t think this should adversely harm the “old school” because they can just continue using `-XScopedTypeVariables`.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 1, 2023, 5:45am UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/40 "2023-10-01T05:45:43Z")

</div>

> [@Ericson2314](#):
>
> the “old school” … can just continue using `-XScopedTypeVariables`.

I think it needs older school [\*\*]: `-XPatternSignatures` as was before `-XScopedTypeVariables` came along.

`XScopedTypeVariables` is a terrible extension because it makes explicit `forall` no longer a merely stylistic choice/its effect is exactly counter to your own rule 2. “the rules are strictly local, no outer scopes / enclosing code needs to be consulted …”. For nearly all extensions, merely switching them on does not change the meaning of an existing program: it enables/allows syntax and _that’s_ what brings in the new meaning. (So @goldfirere makes a good point on the github thread that a warning/linter at the point of that new syntax would work as well. How’s a warning going to detect that the signature uses explicit `forall` _and_ the introduced tyvars are used in the body of the function – being careful not to warn if they’re shadowed ?)

[\*\*] **Edit:** Or perhaps I mean [Scoped Type Variables as documented here](https://downloads.haskell.org/~ghc/6.4.2/docs/html/users_guide/type-extensions.html#scoped-type-variables) – no mention of explicit `forall`.

---

<div class="post-metadata">

**Author:** ![Ericson2314](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/ericson2314/32/1026_2.png) [@Ericson2314](https://discourse.haskell.org/u/Ericson2314)\
**Post date:** [October 1, 2023, 2:59pm UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/42 "2023-10-01T14:59:47Z")

</div>

Yes I think you might be the one person who doesn’t like `-XScopedTypeVariables` but does want pattern signatures with implicit binding.

Perhaps this deserves another poll.

---

<div class="post-metadata">

**Author:** ![Ericson2314](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/ericson2314/32/1026_2.png) [@Ericson2314](https://discourse.haskell.org/u/Ericson2314)\
**Post date:** [October 1, 2023, 3:04pm UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/43 "2023-10-01T15:04:38Z")

</div>

The other definition is basically “anything that is a function parameter in core”. That includes “regular” term parameters, type parameters, and dictionary parameters. Once #448 is implemented, we can stop directly referring to Core, and instead refer to the “most explicit Haskell” I did above.

It makes total sense that this is foreign to people that having been following the proposal process / papers super closely, and instead built a mental model based on the Haskell that currently exists.

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [October 1, 2023, 7:58pm UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/45 "2023-10-01T19:58:07Z")

</div>

A non-Core-dependent way of viewing this is that the new school considers a parameter to be anything over which the function abstracts—any aspect of the function’s meaning that would be determined at the call site of the function, rather than at the definition of the function. That encompasses value parameters, of course, and it also pretty clearly covers dictionary parameters. It’s arguable whether this definition is enough to justify lumping type parameters in as well but I think it does for any given theoretical model of Haskell—either your theoretical model includes type abstractions like System F, in which case type parameters being parameters is a given, or your theoretical model doesn’t, which means your theoretical model doesn’t include polymorphism, which means there is no such thing in that theory as a function `a -> a`, only functions `Int -> Int` and `Bool -> Bool`. Which of those types the term `\x -> x` has, and thus what `\x -> x` ‘means’ (what _valid_ object in your theory the term `\x -> x` corresponds to, in other words), is something that would be determined at the call site, so it’s a parameter.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 2, 2023, 12:37am UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/46 "2023-10-02T00:37:25Z")

</div>

> [@Ericson2314](#):
>
> Yes I think you might be the one person who doesn’t like `-XScopedTypeVariables` but does want pattern signatures with implicit binding.

Thanks John, I think there’s plenty who don’t like `-XScopedTypeVariables` in its present form. (And indeed the design runs against more recent approaches with extensions of making each narrowly-focussed.) The trouble is it’s widely used, so how do we split out the parts each camp wants _and_ keep happy those who will put up with the present form?

I seem to be not the only person who wants implicit binding; but the numbers are too small to be reliable.

> [@](#):
>
> Perhaps this deserves another poll.

Heh heh. We’re getting few enough straws in this poll. And I don’t have a proposal for where we go with dismantling `-XScopedTypeVariables`, so I’m not sure what the poll should be asking.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 2, 2023, 1:18am UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/47 "2023-10-02T01:18:14Z")

</div>

> [@rhendric](#):
>
> That encompasses value parameters, of course, and it also pretty clearly covers dictionary parameters. It’s arguable whether this definition is enough to justify lumping type parameters in as well …

I’m comfortable with the idea the types are parameters as well. It’s more a case of:

a) how soon in their Haskell journey do we start facing learners with the idea of types (and constraints) as parameters? (There’s plenty of learner materials saying things like “the type system _infers_ the correct types for us” [from the Gentle Intro].)

b) do all parameters have to be passed only in the form of positionally placed in a decl individually after the function being defined? IOW

```haskell
f :: Num b => b -> b
f (x :: a) = x * 2

```

_is_ passing the type as a parameter in the same way as the decl takes `b` as a parameter (with no explicit `forall`). Where is the dictionary-as-parameter in the LHS of `f`?

> [@](#):
>
> either your theoretical model includes …

I expect a learner not to have a theoretical model – certainly not including dictionaries and types as parameters. Rather, in using Haskell at the term and declaration level, they acquire a theoretical model. (We hope they’ll be interested enough from the examples to read up on it. At least that’s how I got beyond lambda calculus as theory.)

If the only way to get learners ‘over the bump’ into type theory is by them having to learn implementation detail or abstract System F/Dependent typing, most of them will just walk away.

The Gentle Intro also says “Haskell’s type system is powerful enough to allow us to avoid writing any type signatures at all”. (It concedes there are exceptions, but let’s get a learner comfortable before we go into those.) So I in general don’t give signatures for `let`/`where` subfunctions like inner `f` in @jaror’s `g`, `h` above.

> Nevertheless, judicious placement of type signatures … is a good idea, since type signatures are a very effective form of documentation … [Gentle Intro again]

- Top level signatures, and especially from libraries fair enough.
- What effective documentation value is explicit `forall` adding?
- What effective documentation value is `@...` adding?
- What effective documentation value are signatures in `let`/`where` adding?
- Sometimes the answer is to disambiguate existentially quant’d tyvars – like what learners don’t need to worry about yet.
- Sometimes the answer is because we’re passing type params in a non-obvious parameter sequence – ditto.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 2, 2023, 10:06am UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/49 "2023-10-02T10:06:53Z")

</div>

I find that code heckofa confusing with `s` as both a type variable and term variable. Not least because I don’t know your types, so I don’t know if term var `s` is of type `s`. Even if so, punning of vars seems of dubious usefulness.

> [@maxigit](#):
>
> maybe there is other workaround

Since we’re talking PatternSigs, have you tried without the signature in the `where`, but with

```haskell
shiftUsedBoxes isUsed (boxes :: [Box s']) inBucket'strategies = do
  ...
where 
        ...
        doSwap (source :: Box s', dest :: Box s') = do
                 ...

```

And possibly with a signature on RHS of `doSwap`. There I’m using fresh `s'` so not relying on the scoped tyvar `s`.

(I do think in this case I’d put `shiftUsedBoxes @s' isUsed ...` – that is when we get `@...` available in patterns – because that type param is ubiquitous.)

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 3, 2023, 12:45am UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/51 "2023-10-03T00:45:07Z")

</div>

> [@maxigit](#):
>
> > [@AntC2](#):
> >
> > punning of vars seems of dubious usefulness.
> 
> Not sure I understand what you mean.

Well what’s your take with the [“On the contrary” second example here](https://github.com/hithroc/ghc-proposals/blob/master/proposals/0000-support-pun-free-code.md#326--wpun-bindings-example-1)?

> `f :: t -> ()`  
> `f @a = \a -> ()`

The proposal says that’s “fine”: not the word I would use, because the example is deliberately chosen to be counter-intuitive. (“fine” there means won’t trigger a warning, which perhaps would be a higher threshold of counter-intuitiveness.) The `@a` is shadowed by the `\a -> ...`, so is unavailable on RHS. I can’t even go

```haskell
f @a = \(a :: a) -> ...

```

Then in your example you have (or rather you had) `shiftUsedBoxes :: forall s. ...` with `-XScopedTypeVariables`, so `s` is scoped over the whole definition of the function. But then you had some `(\s -> ...)` with complex expressions on RHS of the `->`, where it might be useful to put a type annotation. Except on RHS, `s` now refers to the `\s` not the `forall s`.

Old-fashioned Haskell tends to use `x, y, z, ...` for term vars and `a, b, c` for type vars. So there’s no risk of punning. This Brave New World of terms appearing as types (or _vice versa_) I’m not sure anybody’s worked out a convention yet.

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [October 3, 2023, 1:40am UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/52 "2023-10-03T01:40:33Z")

</div>

> [@AntC2](#):
>
> The `@a` is shadowed by the `\a -> ...`, so is unavailable on RHS. I can’t even go
> 
> ```haskell
> f @a = \(a :: a) -> ...
> 
> ```

I could easily be wrong, but I don’t think that’s the intent of the overall proposal (I think the text that accompanies this example is somewhat misleading and should say ‘would be shadowed’ instead of ‘is shadowed’).

The punning warnings don’t actually collapse data and type namespaces into a single namespace; they just warn in the situations where _if_ those namespaces were collapsed, a variable in a term would refer to a type or a variable in a type would refer to a term.

In `f @a = \a -> ()`, the second `a` _would_ shadow the first _if_ the namespace collapse were to happen, but the namespace collapse doesn’t happen, so the body of the lambda could still refer to the first `a` in type positions (though this would create a -Wpuns warning) and the second `a` in term positions.

In `f @a = \(a :: a) -> ...`, I’m not entirely sure what if any warnings the proposal wants to be generated, but I don’t think the program would be rejected. If the extensions in effect don’t allow pattern signatures to implicitly bind type variables, I believe this would need no warnings, on the grounds that the lambda parameter can’t be considered in scope in its own type annotation, so the use of `a` there could only refer to the previous binding of `a` regardless of the namespace situation. If the extensions in effect do allow pattern signatures to implicitly bind type variables, then I find this example confusing and I don’t know precisely how to interpret the third `a`.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 3, 2023, 6:25am UTC](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704/53 "2023-10-03T06:25:44Z")

</div>

> [@rhendric](#):
>
> (I think the text that accompanies this example is somewhat misleading …

Thanks, I agree, so I’ve asked on the Proposal for clarification. (It’s still not yet (re-)submitted to the GHC Committee after they initially pushed back; and seems to have not made much progress this year.)

I think the language is describing as-if `-Wpun-bindings` is in force; and as-if the programmer wants single-namespace Haskell. I guess a further question would be how is this to be treated?:

```haskell
f @a = \(a :: type a) -> ...

```

(Using the keyword to tell GHC to look in the type namespace. Would that ignore the lambda-bound `a`? Except this is all in context of wannabe single-namespace Haskell; and following `::` is meant to look in the type namespace first anyway.)

I’m afraid I’ve read too many Proposals at too many stages of drafting; and we’re now at stuttering stages of implementation.

Pointing at the Proposal was more a way of eliciting whether @maxigit sees a potential for confusion amongst readers of the code. (I’m not a big fan of eliminating punning; but then I wouldn’t name term vars same as type vars.)

[Previous page](https://discourse.haskell.org/t/need-feedback-on-pattern-signature-behavior/7704.md?page=1)
