I think you meant (\x -> x) :: forall a. a -> a? Yes it is equivalent, one is just more “filled in”.
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.
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 ?
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 _ -> 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.
@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.
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 foralland the introduced tyvars are used in the body of the function – being careful not to warn if they’re shadowed ?)
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.
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.
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.
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.
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
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?
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.
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.
Since we’re talking PatternSigs, have you tried without the signature in the where, but with
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.)
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
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.
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 awould 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.
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?:
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.)