Skip to content

Better syntax for conditional given instances #7788

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
odersky opened this issue Dec 17, 2019 · 26 comments
Closed

Better syntax for conditional given instances #7788

odersky opened this issue Dec 17, 2019 · 26 comments

Comments

@odersky
Copy link
Contributor

odersky commented Dec 17, 2019

Using present given syntax, it's a bit awkward to define conditional given instances:

given listOrd[T](given Ord[T]): Ord[List[T]] ...

It's worse in the anonymous case:

given [T](given Ord[T]): Ord[List[T]] ...

and even worse in the monomorphic case:

given (given outer: Context): Context = ...

Context bounds can help avoid many cases where a given parameter would be needed but
they do not work in all situations, e.g. they don't work if the typeclass in question has more than one parameter.

Going with the "intent over mechanism" motto, it would be nice if there was specific syntax for
conditional givens. Here's a proposal to fix the three use cases:

given listOrd[T]: Ord[T] => Ord[List[T]] ...

given [T]: Ord[T] => Ord[List[T]] ...

given (outer: Context) => Context = ...

The new syntax reads much better: "given Ord[T] implies Ord[List[T]]] ...".

An immediate concern is that this looks too much like we implement a function type. Yes, but

  • in a logical sense, providing an instance of a function type is equivalent to providing a conditional instance (by modus ponens)
  • there's precedent, where we use => also in cases and self-types
  • in all these cases one can still implement a real function type by putting it in (...).

A separate question is whether in that case we would still support the old syntax with given parameters in instances. My vote would be no, let's have a single way to define things.

I believe that the new syntax also alleviates a concern people were having about the dual use of given as a provider and a consumer. In a sense that dual use is inevitable since given parameters are both consumers and providers. But it's still a concern if given's with different meanings are used next to each other. With the new syntax, this is no longer possible since "providers" (i.e. given instances) don't contain anymore "consumers" (i.e. given parameters) in their clauses.

@odersky odersky added this to the 0.21 Tech Preview milestone Dec 17, 2019
@Jasper-M
Copy link
Contributor

in all these cases one can still implement a real function type by putting it in (...).

Would

given listOrd[T]: Ord[T] => Ord[List[T]] ...

be equivalent to

given listOrd[T]: ((given Ord[T]) => Ord[List[T]]) ...

?

@nafg
Copy link

nafg commented Dec 17, 2019

in all these cases one can still implement a real function type by putting it in (...).

Having parentheses change the meaning so radically seems to be a major footgun.

Besides this doesn't solve the problem because in other cases given still means something else. The fact that the implicit keyword can do two different things was the only real issue with the keyword and it's still not solved.

(Also, I still don't see how the given stuff isn't like 5x as hard to learn and teach than implicits. They seem to have a whole bunch of unique syntax rules. This just adds to that.)

Of topic perhaps but here's a crazy idea.

  1. Keep implicit as the keyword for "this should be in the implicit scope."
  2. Some of the shorthands like omitting def/val can be generalized for other modifiers.
  3. Use given as the keyword for "this takes an implicit parameter." It can have new syntax rules like not being limited to the entire last parameter list or whatever.
  4. A parameter marked given but not implicit does not become an implicit for the method body. A parameter marked implicit but not given behaves as previously with a warning that you should use given or implicit given and that in the future, it will not become an implicit parameter but will only give it local implicit scope.

@Jasper-M
Copy link
Contributor

A parameter marked given but not implicit does not become an implicit for the method body. A parameter marked implicit but not given behaves as previously with a warning that you should use given or implicit given and that in the future, it will not become an implicit parameter but will only give it local implicit scope.

That would hamper usability more than anything else IMHO. It would also mostly defeat the purpose of the new extension methods mechanism.

@smarter
Copy link
Member

smarter commented Dec 17, 2019

I'm intrigued but also wary of the reuse of => for the same reasons others have mentioned. I'm afraid to even propose it but it seems like using some dedicated arrow syntax would work better:

given listOrd[T]: Ord[T] ~> Ord[List[T]] ...

(~> is just a strawman, it conflicts with natural transformation in cats unfortunately)

And once we have that, we could also replace the syntax for given function types, instead of given T => Foo[T], one could use T ~> Foo[T], which I think is interesting since conceptually these things are pretty similar, if you do:

def foo(given Int ~> Foo[Int]) = ...

it's immediately clear that foo locally has something equivalent to a global given Int ~> Foo[Int], compared with:

def foo(given (given Int) => Foo[Int]) = ...

@smarter
Copy link
Member

smarter commented Dec 17, 2019

To expand on what I just said: the other interesting thing here is that when teaching this stuff, we could first teach parameter-less givens and given function types, then use them as building blocks for teaching parameterized givens. This is different from how you'd teach implicits, were you'd have to use implicit vals and defs as building blocks to introduce implicit defs/classes, and implicit function types would be a more advanced concept.

@odersky
Copy link
Contributor Author

odersky commented Dec 17, 2019

The issue is, nobody in their right mind should demand a given of function type. It's way too common a type to be passed around implicitly. So it makes no sense to define a given of function type either, which means the => is available. Which is good because having to invent new operator combinations for not-quite functions makes the syntax much harder to understand for non-experts.

@liufengyun proposed going the other way: Drop all type and value parameters from a given instance, and allow given instances to define polymorphic functions instead. Then it would be:

given [T] => Ord[T] => Ord[List[T]] ...

@smarter
Copy link
Member

smarter commented Dec 17, 2019

given [T] => Ord[T] => Ord[List[T]]

I assume that should be [T] =>> to be consistent with polymorphic function types, but even then we have an inconsistency:

This is (conceptually) a function type with a given parameter, which is available implicitly

given Ord[T] => Ord[List[T] = ...

But this is a regular function type available implicitly:

def foo(given Ord[T] => Ord[List[T]) = ...

To get something equivalent I need the dreaded double-given again:

def foo(given (given Ord[T]) => Ord[List[T]) = ...

@odersky
Copy link
Contributor Author

odersky commented Dec 17, 2019

Polymorphic function types use =>. It's type lambdas that use =>>. Which is a good demonstration for my point that having many operators for functions is confusing.

@Ichoran
Copy link

Ichoran commented Dec 17, 2019

I am not sure the reduction in given-given cognitive switching is worth the novel syntax and divergence from typical method syntax. So I'm neutral on the change. I think it starts out non-ideal and ends up non-ideal.

I think the problem remains squarely with given as a keyword to define new implicits in addition to declaring that you want them summoned into in an argument list. Saying "please assume this wherever you need to" is rather different than, "if I can assume this, then I can do that stuff".

If anything, it would make more sense for summon to be the repeated word. Getting your hands on an instance inside a method is the same operation as getting an instance passed into a method. Either way, you don't name the instance, just the type.

I don't particularly like how it looks, but I find it way clearer.

given listOrd[T](summon Ord[T]): List[Ord[T]]]
given [T](summon Ord[T]): List[Ord[T]]
given (summon Context): Context

I think clarity is the most important consideration.

@odersky
Copy link
Contributor Author

odersky commented Dec 17, 2019

A parameter marked given but not implicit does not become an implicit for the method body. A parameter marked implicit but not given behaves as previously with a warning that you should use given or implicit given and that in the future, it will not become an implicit parameter but will only give it local implicit scope.

I tried something like that a long time ago, when we discussed @lihaoyi 's proposal of implicits as default parameters. I found it does not work, since there are too many choices for the user to make. The default that an implicit parameter is also a provider is a good one, it turns out.

@neko-kai
Copy link
Contributor

This syntax looks awfully like a dependent function type signature – in fact, it's exactly a dependent function type signature after the :!
This is extremely confusing, ambiguous syntax and also raises a question of how to define an actual dependent function type as a given – independent of whether that's a "good idea" or not.

@odersky
Copy link
Contributor Author

odersky commented Dec 17, 2019

This syntax looks awfully like a dependent function type signature – in fact, it's exactly a dependent function type signature after the :!

Which is fully intended, and if we adopt @liufengyun's proposal we'd extend the same treatment to polymorphic function types. The idea could be:

A given instance has never parameters on its own but it can define a normal type or a function type.
If it defines a function type, the given on the argument types is implied.

We could go even further and build modus ponens into implicit resolution i.e. if we look for an B and find a given f: A => B and a given b: B, then synthesize f(b). Right now this happens only if f: given A => B. But the fact that f itself is given could be seen as sufficient for doing this. I am not arguing that we should do it now, but we certainly could from a logic standpoint. It would be logically consistent to do so. So, this means that, morally, a given of function type can be seen as a conditional given. The opposite is also true, via eta expansion. That's why I think that in this case the ambiguity is defensible, since (1) one case will never happen in practice (i.e. nobody should want to provide a given instance for a plain function without modus ponens) and (2) the two cases are morally almost the same, so there's no need to split hairs and give them dissimilar syntax.

@jeremyrsmith
Copy link
Contributor

Just wanted to ask everyone to once in a while take a step back and look critically at what we've got so far. Is it better than where we are with implicit in Scala 2? If so, why? If not, why?

I think there's a lot of talk about how the problem with implicit is that it's a mechanism and not an intent. I think that's a fair point, and I'm not arguing against the change to given. But, keep in mind that "mechanism not intent" was very nearly zero people's actual problem with implicit. The actual problem was that implicit meant different things, some of which were bad, and others of which were complex and sometimes confusing. I think this proposal is very syntactically confusing and makes code harder to read, because it looks like one thing but is another thing entirely. Take a critical look at it from the point-of-view of a beginner, and ask yourself whether we'll bikeshedding given's own rebranding when Scala 4 comes.

@jeremyrsmith
Copy link
Contributor

The problem with given (given outer: Context) can be solved by adding a name, or a line break, or any number of other things. The problem in the case of given listOrd[T](given Ord[T]) is more with the first given than with the second, so IMHO you're eliminating the wrong one. You're saying, "given that T has an ordering, it's implied that List[T] has an ordering." Maybe going back to implied for the definition site would be a better way to describe that than overloading a function type syntax (in this specific situation) to mean "implied" because the arrow kinda looks like an implication arrow.

@jdolson
Copy link

jdolson commented Dec 17, 2019

I admit the proposed syntax reads better and looks nice. I just finding it troubling that it looks very much like something it's not: a function. The fact that adding parenthesis changes the meaning is disturbing and will, I fear, be the source of great deal of confusion.

@odersky
Copy link
Contributor Author

odersky commented Dec 17, 2019

Let's try to decompose the ambiguity argument. Why could ambiguity be bad?

  1. It looks like given instances define functions when they do not. I don't believe that matters. Someone new to givens will expect to have to learn what they are anyway, and then the meaning of conditional as implication becomes immediately clear. The effect that at first glance these things look like functions gives actually a good intuition of what is going on. It is not misleading at all.

  2. It's less obvious how to define instances for real functions: You need to put the function type in parentheses. Actually, it turns out that is already the case today (it's the same as for types after extends) and nobody noticed. Which goes to show that nobody would normally want to do that. I generally try to follow Alan Kay's guideline: "Make simple things easy and hard things possible". That guideline is respected here.

  3. It might give rise to false analogies elsewhere. I.e. if we can define a conditional instance like this:

given A => B ...

maybe we should expect that we can define an anonymous given parameter of implicit function type like this?

(given A => B)

But no, in the latter case we have to write given ((given A) => B). I was a bit worried about that. But then I believe that very few people would write given ((given A) => B) either. In our codebase we have a single test that exercises the idiom, and it is arguably a corner case. So, yes, it would be a false analogy, but only the most intrepid would actually venture that far. And they should be able to handle it.

@jeremyrsmith
Copy link
Contributor

To be clear, I'm not worried about being confused when writing the code, moreso when reading it. If my eyes are focused on the source code:

foo: ThingOne => ThingTwo

then now I have to backtrack in order to parse that. Does it have given before it? Or is it def or val? This will take a nontrivial number of milliseconds to figure out whether foo represents a function value or an implicit derivation.

This will also contaminate all usages of A => B as an ordinary type, because my brain will have to consider this new context in order to decide what it means.

It's easy to handwave and say "it will be fine, nobody should be doing X so it won't matter." And maybe that would turn out to be true, but I think the current awkwardness of given (given ...) is preferable to the risk of overloading existing syntax (whatever parallels can be drawn). Recall how overloading implicit to mean "term inference" but also "implicit conversions" was the original reason for its current rebranding. The proposed syntax is overloading existing syntax that's existed for quite a while in Scala already.

There could be a case made for this if the syntax for a function type A => B was changed so that it always has to be wrapped in parameters. That would be an annoying change, but at least there would be a consistency to it such that people could rewire their pattern recognition algorithms over time. I'm not in favor of that, mind you, as I think this is way too big of a backflip to solve an awkwardness which isn't really all that awkward.

If I'm writing given (given ctx: Context): Foo (which is really the only objectionable example IMHO) then I would look at it and say "ick" and add a name for the derivation: given fooFromContext(given ctx: Context): Foo. Problem solved, no backflips necessary. It's always going to be possible to make code look awkward; there are even ways to do it in Scala 2 – most people haven't had that problem so far.

@smarter
Copy link
Member

smarter commented Dec 17, 2019

I was a bit worried about that. But then I believe that very few people would write given ((given A) => B) either

That's a fair point, but it still means that if someone asks "What does given A => B in Scala mean?" on stackoverflow, the answer will have to be twice as long to explain that the meaning depend on the context, and one meaning is equivalent to given (given ... in the other context, not very user-friendly. Contrast with my hypothetical given A ~> B which can be explained through decomposition: first understand given A, then understand A ~> B, then here's what happen when you use both at the same time. I think that's similar to why people still like implicit def, they can explain it in terms of def, whereas given currently can't be easily explained in terms of simpler things, despite having fairly complex semantics.

@odersky
Copy link
Contributor Author

odersky commented Dec 17, 2019

@jeremyrsmith The multiple meaning problem you mention exists already today.

foo: ThingOne => ThingTwo

means one thing, but

case foo: ThingOne => ThingTwo

means another, where => is not a function constructor but an implication. Likewise,

given foo: ThingOne => ThingTwo

would treat the => as an implication. It's OK, since morally all these use cases are related.

@odersky
Copy link
Contributor Author

odersky commented Dec 17, 2019

That's a fair point, but it still means that if someone asks "What does given A => B in Scala mean?"

I would answer it means a given instance for B, provided there is one for A. If someone then corrects and says it could also mean an implicit parameter of type A => B I would disregard this on the grounds that it is irrelevant since nobody writes code like this. We might go and make that usage downright illegal and I bet that nobody would notice. But that would be silly. We should not go into contortions to disallow things that nobody writes anyway, unless there's a strong reason to do so (like a soundness violation, for instance).

@jeremyrsmith
Copy link
Contributor

@odersky

The multiple meaning problem you mention exists already today.

It's true that the same tokens exist within a case definition. But that can only exist inside a match block or partial function, whereas both given and def/val can both be top-level or class/module-level. I think it is easier to disambiguate case, though I'll admit I can't exactly describe why (so maybe I'll just get used to it and shouldn't worry).

I still think that the problem this is meant to solve is a bit overstated, though, and I question whether it's worth it. Anonymous instances are a nice new bonus, but it's always possible to insert a name when the definition looks awkward without one.

I guess you could make an argument that given [A]: Flerb[A] => Glarb[A] is slightly reminiscent of instance Flerb a => Glarb a where ... in Haskell. But Haskell doesn't also use => for function types, so it's not confusing there.

What would it look like for multiple given arguments to a derivation? Like this?

given [T, U]: (Wizzle[T], Wozzle[U]) => Wuzzle[T, U]

@jeremyrsmith
Copy link
Contributor

given (lol) the polymorphic function syntax above I guess it would be one of these:

given [T, U] => Wizzle[T] => Wozzle[U] => Wuzzle[T, U]
given [T, U] => (Wizzle[T], Wozzle[U]) => Wuzzle[T, U]

I have to admit I'm warming up to it a bit, at least when using anonymous instances... and thinking about it more, I never really use derivations without any type arguments involved, which was really the only case that felt difficult to parse.

I'll walk back my objection a little bit 😄

@jdolson
Copy link

jdolson commented Dec 17, 2019

A separate question is whether in that case we would still support the old syntax with given parameters in instances. My vote would be no, let's have a single way to define things.

I'm a bit unclear about what syntax would be no longer supported. You would no longer be able to have final given clause consisting of only anonymous instances on a conditional given? But anonymous given clauses would still be supported in other places (e.g. a non-final clause)?

@jeremyrsmith
Copy link
Contributor

A little more real-world example:

given [H, T <: HList] => (lengthT: Length[T]) => Length.Aux[H :: T, Succ[lengthT.Out]]

doesn't look more objectionable than before. But it does show that the <: return type signature isn't obviously covered by the proposal, e.g.

given lengthCons[H, T <: HList](given lengthT: Length[T]) <: Length[H :: T]

@odersky
Copy link
Contributor Author

odersky commented Dec 18, 2019

@jeremyrsmith

What would it look like for multiple given arguments to a derivation? Like this?

given [T, U]: (Wizzle[T], Wozzle[U]) => Wuzzle[T, U]

Currently both this and

given [T, U]: Wizzle[T], Wozzle[U] => Wuzzle[T, U]

are supported. We might narrow it down to one or the other before the final version ships.

I still think that the problem this is meant to solve is a bit overstated, though, and I question whether it's worth it. Anonymous instances are a nice new bonus, but it's always possible to insert a name when the definition looks awkward without one.

I agree it depends on your use cases. One reason I proposed the change was that I thought of a use case where conditional instances would come up all the time and should be as lightweight as possible. That was using given instances as axioms and inference rules for theorem proving. So, the old syntax might not be a big problem now but it might become one, depending on where people go with givens.

@jdolson

I'm a bit unclear about what syntax would be no longer supported.

given instances would not longer have given clauses.

@nafg
Copy link

nafg commented Dec 18, 2019

That would hamper usability more than anything else IMHO.

The default that an implicit parameter is also a provider is a good one, it turns out.

@Jasper-M @odersky to be clear, I'm not arguing in favor of making implicit parameters not be implicit locally without an extra keyword. My point was that I seem to recall that the argument that it's confusing to have one keyword mean two things was one of the strongest arguments for changing around the whole implicits thing, and in the end we're not actually going along with it.

Just wanted to ask everyone to once in a while take a step back and look critically at what we've got so far. Is it better than where we are with implicit in Scala 2? If so, why? If not, why?

I am very skeptical about this. Scala 2 implicits are dead simple to explain and have almost no syntax rules to learn (we already know what a modifier is). Givens seem to have an arbitrary number of syntaxes and there's no way to know what each one does.

I think there's a lot of talk about how the problem with implicit is that it's a mechanism and not an intent. I think that's a fair point, and I'm not arguing against the change to given.

FWIW I strongly disagree with the whole philosophy. The value-add is in high-level and declarative mechanisms ("this is implicit") vs. low-level or imperative mechanisms ("set byte X into register Y"). I don't agree that we should expect the computer to work well with intuitionist expressions of intent. It results in a much more complex mental model. (In some cases it creates bigger problems, like when people started thinking Google was not just a way of getting to content that people put on the web, but that it could give answers to questions, which is a fiction that falls apart as soon as there's disagreement about something.)

But, keep in mind that "mechanism not intent" was very nearly zero people's actual problem with implicit. The actual problem was that implicit meant different things, some of which were bad, and others of which were complex and sometimes confusing. I think this proposal is very syntactically confusing and makes code harder to read, because it looks like one thing but is another thing entirely. Take a critical look at it from the point-of-view of a beginner, and ask yourself whether we'll bikeshedding given's own rebranding when Scala 4 comes.

I don't think implicit meant different things, but it was used as a lower-level tool to common patterns, and some anti-patterns. Just as scala did with case class, object, and val we should definitely identify the high-level patterns people use and create ergonomic syntactic constructs for those things, and just as scala did with asInstanceOf we should make people think harder before using potential footguns.

I just don't see given as doing that. It's once again a single keyword doing different things, except now it's far from obvious what all those things are.

I can summarize everything a beginner needs to know to understand implicit, including syntactically, in about 2 or 3 sentences. If someone can do that for given, fine. Otherwise I am very nervous about this experiment. (All software is an experiment until it reaches its full audience. Remember Windows 8?)

anatoliykmetyuk added a commit that referenced this issue Dec 18, 2019
Fix #7788: Add new syntax for conditional given instances
odersky added a commit to dotty-staging/dotty that referenced this issue Jan 16, 2020
This reverts commit d1579e6.

# Conflicts:
#	compiler/src/dotty/tools/dotc/parsing/Parsers.scala
#	docs/docs/internals/syntax.md
#	tests/pos/reference/delegates.scala
odersky added a commit to dotty-staging/dotty that referenced this issue Jan 22, 2020
This reverts commit d1579e6.

# Conflicts:
#	compiler/src/dotty/tools/dotc/parsing/Parsers.scala
#	docs/docs/internals/syntax.md
#	tests/pos/reference/delegates.scala
odersky added a commit to dotty-staging/dotty that referenced this issue Jan 23, 2020
This reverts commit d1579e6.

# Conflicts:
#	compiler/src/dotty/tools/dotc/parsing/Parsers.scala
#	docs/docs/internals/syntax.md
#	tests/pos/reference/delegates.scala
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

8 participants