Then you don’t even need as. You might as well use good old :.
def run[P]{p: Parser[P]}(x: p.Input): p.Result
I like this! Thanks @regiskuckaertz
2 Likes
Wonderful!
All these viewpoints are equivalent, in a deep sense. This is exactly the Curry Howard isomorphism, which equates function types and implications.
Yup! 
Proposal: Change the syntax for given clauses so that a
givenclause consists of the following elements:
- An optional name binding
id : - Zero or more conditions, which introduce type or value parameters. Each precondition ends in a
=>. - the implemented type,
- an implementation which consists of either an
=and an expression, or a template body.
This is fantastic! 
I totally support the revised proposal.
2 Likes
The def f[A]{Ordering[A]}(x: A) = ??? syntax seems like “symbol salad” to me compared to
def f[A: Ordering](x: A) = ???
And I like that the param list with explicit using params is explicitly marked using, which makes the syntax readable and pronounceable by a Scala learner:
def f[A](x: A)(using Ordering[A]) = ???
Scala 3 has a human-friendly language for implicits based on given and using, which makes a good story to teach and learn and the words show up in the syntax.
The proposed curly braces in the SIP are only needed in the contrived cases where more than one context bound is needed. If we require an extra param list with curly braces all the time we would burden all defs, also the simpler case with just one context bound that currently is OK in my opinion.
4 Likes
Wonderful!
I also like what we have arrived at! 
Zero or more conditions
Hmmm. I guess the type param of the value param needs to come first, and A => Ordering[A] means something else than Ordering[A] as shown in this example:
scala> def f[A](a: A)(using ord: Ordering[A]) = ord.compare(a,a)
def f[A](a: A)(using ord: Ordering[A]): Int
scala> f(12)
val res19: Int = 0
scala> def f[A](a: A)(using ord: A => Ordering[A]) = ord.compare(a,a)
-- [E008] Not Found Error: -----------------------------------------------------
1 |def f[A](a: A)(using ord: A => Ordering[A]) = ord.compare(a,a)
| ^^^^^^^^^^^
|value compare is not a member of A => Ordering[A], but could be made available as an extension method.
|
|The following import might make progress towards fixing the problem:
|
| import scala.math.Ordered.orderingToOrdered
|
1 error found
scala> def f[A](a: A)(using ord: A => Ordering[A]) = ord.apply(a).compare(a,a)
def f[A](a: A)(using ord: A => Ordering[A]): Int
Or did I misunderstand what you meant? @spamegg1
Edit: Yes I misunderstood the comment to be for defs not givens (missed the quote and thought that it was a new proposal. My bad…)
1 Like
Yes, we would never use it like that in a using clause at the call site; the type parameter [A] => ... is only needed at the given definition site.
It’s basically just like instance ... => ... where syntax from Haskell, if you are familiar.
So in that sense, it’s not literally the same as a function type at the syntax level. But it is conceptually (via Curry Howard).
(Now you are probably familiar with the below:)
But rather it’s a conditional in the Curry Howard sense, like Martin said. It’s just like Modus Ponens. Think of it as partially applied functions (currying), but instead of partial application, it’s like “using a background assumption”.
For example,
given [A] => Ordering[A]:
...
means: "IF we have a type A (and all the operations available on it), THEN here is how we can conditionally derive an Ordering[A] by depending on, or using, if you prefer, those operations…
Another example:
given [A] => (ord: Ord[A]) => Ord[List[A]]:
def compare(x: List[A], y: List[A]) = ...
means: “IF we have a type [A] and its operations etc., THEN by depending on / using that, we can obtain / derive / define / prove an (ord: Ord[A]) => Ord[List[A]] as follows…”
(The partially applied function analogy would be: "if you give me an A as input, I can give you a function Ord[A] => Ord[List[A]] as output.)
The conclusion itself is a conditional, (ord: Ord[A]) => Ord[List[A]] means: “IF we have a (ord: Ord[A]), THEN here is how we can obtain Ord[List[A]] from that.”
So it’s like cumulative assumptions that chain together in implication. P => Q => R associates to the right like: P => (Q => R), which is equivalent to: (P and Q) => R:
if we have a type
Aand all the operations available on it;
AND if we know how to obtain anOrd[A]fromA,
then here’s how to obtain anOrd[List[A]]…
The logic is: "If I know how type A works, I have a proof that: (((if I know how type Ord[A] works, I have a proof that I know how Ord[List[A]] works))).
The partially applied function analogy would be: “OK, you gave me an A and I gave you a function Ord[A] => Ord[List[A]] in return. Now, if you additionally have an Ord[A], you can apply this function to it to get an Ord[List[A]] as output.”
Function = implication;
Applying function = using assumption to prove something (or modus ponens, or “implication elimination”).
1 Like
Thanks for clarification @spamegg1 . Yes that’s also how I understood the rationale for givens. (I thought you meant for using-clauses in defs; that’s why I got confused… but when re-reading what you wrote I see that you refer to givens by the quote. Sorry.)
1 Like
I agree with the characterisation, I don’t like it either. Your counter-example is very simplistic though, what about instances with multiple bounds or constraints on path-dependent types, if these are at all supported in the new syntax?
def showMax[X : {Ordering, Show}](x: X, y: X): String
type Foo = [X: {Semigroup, Show}, P: Parser { type Input <: X }] =>> P.Input => P.Result // no idea if this is legal
We may have different thresholds for symbol salads 
Perhaps this could be made legal:
def foo[{M, S}: Action](x: M, y: S): S
but what if M or S needs another bound, then we’re screwed. Perhaps you want to forbid multi-parameter typeclasses—this is not stated anywhere.
That may well be a nice teaching device, but @bishabosha 's statement if I understood correctly is that the new syntax will be at least as powerful and more concise than the low-level explicit syntax, such that there is no reason to use the low-level syntax anymore.
Maybe look at Flix:
def foo[m, s](x: m, y: s): s with Action[m, s]
def showMax[x](x: x, y: x): String with Ordering[x], Show[x]
Type parameter clauses can be omitted:
def foo(x: m, y: s): s with Action[m, s]
def showMax(x: x, y: x): String with Ordering[x], Show[x]
EDIT: I thought the above would not work for path-dependent types, but in their recent paper introducing associated effects they manage to abstract away order of clauses from dependencies, i.e.
trait Div[a] {
type Aef: Eff
def div(x: a, y: a): a \ Aef
}
def avg(l: List[a], z: a): t \ Div.Aef[a] with Add[a], Div[a]
1 Like
Thank you all for coming up with this very welcome improvement!
Finally givens got a proper mental model that will help me to remember the syntax for all variants.
The old syntax wasn’t bad, and I think this makes it even more remarkable that @odersky went the extra mile and pushed for something that is now actually close to perfection, after the refinement process here.
I think the most significant part of the now proposed mental model is that it finally properly explains what givens are supposed to be at the core.
The main problem with the old syntax was that givens aren’t actually neither value definition nor method definitions but looked a little bit like both (I think mostly caused by the fact their internal implementation is in fact that one of a lazy val / def hybrid). But they’re not any of that on the conceptual level! That’s just machinery.
The abstraction is that givens define new entries in a kind of “context map”, conceptually a tree map of types to values, floating implicitly in context. The given “declaration” defines the key—a type!—,and its (optional) body the value. (If one would like to write it like that the separator between the key-forming signature and the body would be actually -> but I’m not going to propose that as I think it would stick just to much out on the syntactic level, even it could be explained by semantics). The main point here is that given “signatures” define types, not values nor methods.
The rest follows naturally: Contextual givens are logical propositions that describe what preconditions you must fulfill (proven / “witnessed” by having constructed values of the required types) in order to be able to retrieve some other value from the “context map” by a specific type-key. The type of a logical proposition is a function type.
All that resembles the Curry–Howard correspondence in a really beautiful way.
The only sore point of the now proposed new syntax is imho the case of named givens. I think it’s still irregular, and what’s actually worse it’s less readable as it could be, as it doesn’t optimize to focus attention on the important part, which is even in the case of named givens the type.
Giving a type (that happen to be the same type as another “context map” key type) an additional “name tag” to distinguish different keys is imho a kind of special case without precedence in the language.
The closes to that are type aliases. This would imply to use = between the given name and its signature and body. This would end up in some cases with a double = instead of a double :. Imho that doesn’t make any significant difference, but is imho more regular, given the semantics. But a type alias would again put the alias name front even the name is in the case of “keys into the context map” just a kind of “tag” to distinguish “same looking” keys.
So in the end I would prefer using the postfix as to “tag” types with names. This puts the important thing, the type, front. Yes, as looks currently very irregular. But I think this is justified by it’s semantics: It’s there to “tag a type with a name”. That’s without precedence. And as it’s something different to anything else it should have it’s own syntax! (In general: Similar things should look similar, but different things should look different.)
“Tagging a type with a name” is kind of similar (even not identical) to renaming a type, something that is done in imports with an as. Also we have a second similar (even not identical) case: Naming a match in pattern matching. This uses currently the dreaded @ syntax… I think making all these cases use as would make for some pretty good improvement in regularity of the language. (Re)naming types (or patterns, which mirror the value structure of types) would uses as¹.
Also the as wouldn’t stick out so much any more in the context of givens in case the proposal for is comes in, I think.
I would additionally argue quite loudly that is should stay is. Not some has, or having, or implying or whatever got proposed so far. It’s is because type classes (let’s better call them concepts!) establish a kind of “is a” relation between types. (That’s also why the context bound syntax looks like a type ascription on a type for good reason. And that’s exactly the “is a” relation here, saying “something is an element of some set (~type)”.)
A concept is a set of common properties / behaviors among some (often not directly related) things. If a thing has the relevant properties or shows the relevant behaviors it IS an instance of said concept. Some examples of proper concepts are Colorful, or Printable, or Encodable / Decodable / Serializable, or Even, or Ordered, or more abstract, Mappable, Foldable, etc.
If writing SomeThing is (an instance of) SomeConcept (like Number is Printable, or String is Mappable) doesn’t make sense when read aloud you just discovered that you didn’t name a proper concept in the first place.
There is also no reason to worry that you didn’t state an (universal) truth when saying is (the remark from @Ichoran): As you can’t query for instances of some concept that has diverging mapping in scope the is statement is ultimately true in the scope you make it if the code compiles. That it’s not necessary a true statement in some other scope doesn’t matter. Nobody would see a problem in defining a val differently under the same name in different scopes, even the val definition reads actually aloud as “the value of ‘someName’ is ‘someValue’ once and for all”…
All in all I very much like the current outcome.
But I would really hope people stay open for the other parts of the proposal. The parts which got for now delayed until later, or frankly took out of scope. I think the complete package including as (please also for pattern matching!) and is looks even more awesome than the current state (which is of course still great on its own). Please look at the whole picture. Having all that (including the Self type thingy) we would have, in my opinion, the best “concepts” implementation of all languages. Let’s get there!
¹ Just “discovered” by chance that this would actually also match one of my older ideas, namely to alias Conversion[A, B] as as[A, B] and use it infix… Conversions can be also seen as kind of “renaming types” (by mapping values) conceptually. That comes unexpected, but fits nicely.
2 Likes
I don’t understand. In the key-value metaphor we are not naming the key but the value. To be able to retrieve it directly without using the key/type.
1 Like
I think this depends on how you want to see the metaphor.
The name can be seen as a kind of “handle” to the value. But the “handle” to a value in a map is a “key”. So the name is part of they key, not the value.
Now the key is a type. “Naming a type” is exactly the “new thing without precedence”.
Of course you can say that “the handle is the value”. But that breaks imho the metaphor.
I agree that this is debatable. It depends on how you want to read and interpret the metaphor. I’ve just tried to offer a different perspective, and show that this perspective is coherent in itself.
To see better what I mean maybe we should look at an example.
Let’s assume, just for the sake of the exploration of the mental model of givens I try to draw, the following syntax. (I’m not proposing it as I think it would be too much of a stretch, especially as things look already good).
given Type -> value
This creates a new entry in the “context map”.
I would parse it mentally as
{{given}} {{Type -> value}}
The given says: “New context map entry”, and than a typical map entry follows.
But what if I want to name things? (And actually what do I name?)
If you say
given typeAlias: Type -> value
how to parse that?
If we try the previous approach it would look like
{{given}} {{typeAlias: Type -> value}}
But what did we get?
This looks like a map from value to value (not type to value!), with a key that has a type ascription.
That’s not what we want to express.
I could also parse it differently:
{{given}} {{ {{typeAlias}}: {{Type -> value}} }}
But now what is it?
The best I could come up is "a type ascription on something typeAlias (what is it actually? A value? But it’s prefixed with given, so should be a map entry???).
But not even this interpretation makes sense as there is no type syntax that reads {{Type -> value}}.
So this interpretation is even worse then the previous. It doesn’t fit any mental model!
We could instead use “type alias” syntax:
given typeAlias = Type -> value
This makes a little bit more sense as it parses (in my mind) as
{{given}} {{ {{typeAlias}} = {{Type -> value}} }}
But what did we name here?
We named the whole map entry! Not the key, and for sure not the value. This seems therefore also off.
The as syntax seems more to the point imho:
given Type as typeAlias -> value
I would parse it as
{{given}} {{ {{Type as typeAlias}} -> value}}
We have still the map entry structure, but now we’re explicitly naming the key (which is a “handle” to the actual value in the map).
Usually you can retrieve values from the context map only by triggering lookup by implicit search. But having a (value level!) “handle” to the entry in the map allows you to get the value directly. But it’s still a value in the “context map”, in a kind of ghostly scope usually only accessible though querying by types. The name is a “handle” to a type therefore (just already on the value level, without the need to call a function which would take type parameters, like summon).
Additionally there is symmetry with pattern matching: Looking up things in a map can be seen as pattern matching on the keys of said map. So as the given syntax puts entries into a map, a pattern match can be seen as the symmetric process of retrieval. (Even pattern matching usually doesn’t match on anything from the “context map”, this is just a analogy to show that there is a kind of “hidden” link in possible syntax).
A pattern match looks (often) something like:
case Type => value
If we want to (re)name the matched pattern we would write:
case Type @ aliasName => value
If you write it with as instead I think the syntactic symmetry is obvious:
case Type as aliasName => value
Change case for given and the fat arrow for the map operator, at viola
given Type as aliasName -> value
This syntactic symmetry can be actually justified because “putting something in a map” and “retrieving something from a map” (which is pattern matching on the key!) is symmetric.
For me this makes perfect sense, and gives some nice, deep explanations of syntax. It’s regular, and nicely symmetric, showing logical links between the fragments of the language.
val foo = new Foo:
def myMethod = "foo"
We name the value which we assign to what we get by mapping from a type Foo to a particular instance (created by defining what we need to define thereby making a new unnamed subtype, and then silently creating one of it).
We already have this–it’s anonymous class instantiation.
2 Likes
@Ichoran, first of all thank you for your other post which I enjoyed to read as they show a kind of similar understanding of the language to my own. I also think in kind of “syntax slots”, a term that is imho a great vehicle to come up with coherent syntactic constructs.
But I have to disagree on the interpretation of what you’ve shown.
I would parse
val foo = new Foo:
def myMethod = "foo"
as
{{val}} {{ {{foo}} = {{new Foo: def myMethod = "foo"}} }}
For me new Foo… forms one entity, and takes up one syntax slot on its own. It’s just a Foo value!
There is nothing that resembles a “key-value construct” inside this entity.
Values are “atomic”, even they have internal structure. You need tools like selection to look inside a value. The definition of class type structure also doesn’t resemble key-value entries from class type to, hmm, what actually, again some map of “body entries”? I think a language that works something like that would be actually funny, but I think this is not Scala. Objects (values) are quite “atomic” in Scala… You can’t move parts of them independently. (Like you can with keys and values of some map!)
If there is any key-value structure somewhere here, than it’s on the outside syntax, namely “foo -> new Entity”. This forms an entry in the “value map” that forms an “environment” (just the lexical scope in this case).
Also foo is in this case again a name for a value, not a type. So this can’t be applied to givens in my opinion. I think I’ve argued already that givens aren’t value definitions, nor methods, but map entries of key of type to (regular) values.
(I understand if this line of view seems alien to some, as we were used to the technicalities for years, having “naked” implicit vals and defs. But I think it makes sense to shift the mental model to a more appropriate high level one. One that embraces the actual abstractions that are expressed, like a “context map with type-keyed entries” for “implicit scope”. In this mental model givens are in fact more types than anything else as the associated value can be often automatically derived and doesn’t even be named, think given ConstructorCall(). Still this is just a shorthand syntax to create a type keyed map entry. Something that written out would look like given ConstructorCall -> new ConstructorCall() in my fictional syntax which emphases the “syntax slots”.)
If one would like to put new Foo… somewhere in the fictional syntax I’ve used
given Type as typeAlias -> value
than it would take the place of the value slot. It would likely look like:
given Foo as fooAlias -> new Foo: def myMethod = "foo"
(Which parses than as before.)
Now for the real syntax I think it’s not a big stretch to say:
given Foo as fooAlias:
def myMethod = "foo"
It’s just a terser version, which removes duplication of the type name, and “hides” the new, like creating anonymous class instances would do. It uses the colon “properly” now, instead of the ->, also now with the mandatory line break.
But this doesn’t influence what forms the syntax meta-elements! I would still parse it as
{{given}} {{Foo as fooAlias}}{{:
def myMethod = "foo"}}
with the {{:\n being the [new] Foo shorthand, which is “normal Scala”, and would work the same without the name tag on Foo.
Also this reads imho much better than
given fooAlias: Foo:
def myMethod = "foo"
or
given fooAlias = Foo:
def myMethod = "foo"
In that syntax (even understandable) we emphasize fooAlias, something that we can directly “see” on the value level, and it will cause directly errors if we have a name clash, but the more important information, namely that we took up a key slot in our “context map”, something that we can’t see and something that won’t provide direct feedback if we create a clashing entry, is put more off side.
One needs to memorize the keys in the “context map”. There is no good way to “see what’s inside”. So it should be imho quite explicit if new entries are added. The key (the type construct!) should come always first as it’s the actual key. An alias name for it is secondary—especially as this alias is directly visible as proper value in scope.
I’ve read about the new soft keyword tracked and I wonder if the keyword transparent should or could be used instead. It seems to me that tracked has a similar meaning in the language as transparent. Has transparent been considered?
By the way, the SIP-64 does not describe tracked. Is it part of that proposal? Or is there another SIP to look at?
2 Likes
I still hope someone finds a way to avoid the keyword altogether.
The functionality is really good, should have been always like that, but needing a keyword for something that looks like it should be default behavior seems odd.
As described in the other thread, I actually don’t even understand fully why the keyword is needed. Does it only fix a corner case (for literal Singleton types), or is it more?
The modularity import describes a lot of features that all hang together. The plan is to propose them successively in several SIPs. SIP-64 makes a start. tracked will hopefully be in a follow-on SIP.
transparent has not been considered so far. It’s an interesting alternative, IMO.
4 Likes