Better syntax for conditional given instances

[odersky]

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.

[Jasper-M]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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.