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.
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.
That sounds to me like implementation details and I am wondering if the “new school” point of view is only the view from the implementor lenses (should I know core to program in Haskell ?)
I asked the following question Is class dictionary passing the result of a implementation choice or theoritical necessity on reddit (to get a different audience and avoid any biais). If I am right this confirms that all of this is exposing implementation detail.
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.
1 Like
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
foralladding? - What effective documentation value is
@...adding? - What effective documentation value are signatures in
let/whereadding? - 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.
1 Like
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.)
s as in ST s a monad. To simplify Box s is a STRef and Warehouse is a ST s.
All the ss are there to make sure that the boxes and shelves belongs to the same warehouse.
Not sure I understand what you mean.
It is actually a bad example, because apparently it compiles if I remove the type signatures and even the forall (I must have put it for a reason though). I’ll try to dig better one lol.
Well what’s your take with the “On the contrary” second example here?
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
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 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.
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.)
Ok, I wasn’t sure by what you mean with “punning”. I didn’t realize that I was using s as type (for state as in STRef s and s as a local binding. As the code deal with boxes and shelves, I sometimes use b for box and s for shelf. In that particular case It should have been b for box. Thank you for letting me know 
.
As I said, I even did see the problem. It just shows that they are really two different namespaces in my head. It never occured to me that there were a risk of shadowing.