Adding language motivation document#649
Conversation
|
Some things i need to do
|
|
It would be nice to start such a document talking about the two key differentiating features of the language: region-based ownership and behaviour-oriented concurrency. I worry that someone coming to the language and seeing this would not see what makes Verona interesting. |
|
@microsoft-github-policy-service agree |
I agree. I think we aimed to explain the main features of the type system, with less focus on capabilities, regions and BoC. I could try to add parts about these as well, or perhaps change the introduction to more clearly state what the document is supposed to be. |
EliasC
left a comment
There was a problem hiding this comment.
This is a really useful document to have! I have added some comments and questions, and also opened a pull request with spelling fixes.
| In Verona, a trait with multiple methods can be further simplified by breaking | ||
| up each method into what we call an "atomic" trait and combining them with a | ||
| conjunction. E.g. the definition of `Number` above is simply syntactic sugar for | ||
| ```verona | ||
| type Number = { | ||
| add(self: Self, other: Number): Number | ||
| } & { | ||
| sub(self: Self, other: Number): Number | ||
| } | ||
| ``` |
There was a problem hiding this comment.
Is this important for a language motivation, or is it an effect of how we formalise things? Maybe it actually helps with intuition for things.
There was a problem hiding this comment.
It probably doesn't make much difference to most people. On the other hand, I don't think it hurts to mention it?
There was a problem hiding this comment.
I think it might even help with the intuition for &, reading it again now. But maybe it should be more of a note than a proposed simplification (I would argue that it is less simple to compose atomic traits than to write a composite trait).
There was a problem hiding this comment.
yeah, i agree, i'll see if i have time to write something before the meeting
There was a problem hiding this comment.
"syntactic sugar" ==> "can also be understood as"
I think our readers do not care about syntactic sugar.
| ###### External trait inheritance | ||
| A possibility is to allow externally declared trait inheritance, i.e. | ||
| declaration of trait inheritance can be separated from class definition. | ||
| ```verona | ||
| // file 1 | ||
|
|
||
| // class C definition | ||
| class C { | ||
| toString(s: C) : String | ||
| ... | ||
| } | ||
|
|
||
| // file 2 | ||
| // declaration that C implements Printable together with its default method | ||
| class C : Printable | ||
| ``` |
There was a problem hiding this comment.
Should we group hypothetical features in a section of their own? Or maybe mark these headings as hypothetical (or "in flux" or something else that makes sense)?
There was a problem hiding this comment.
Compared to the previous example, it is the ToString trait that implements print.
There was a problem hiding this comment.
probably, we should discuss where we should put this
docs/motivation.md
Outdated
| ```verona | ||
| type A[T] = { | ||
| type Self | ||
| type Anon = { | ||
| type Self | ||
| g(self: A[T].Anon.Self) : A[T].Anon.Self | ||
| } | ||
| f(self: A[T].Self) : A[T].Anon | ||
| } | ||
| ``` |
There was a problem hiding this comment.
Is local types a thing? Looks like Scala's path-dependent types. I think the desugaring would hold even if Anon was a top-level trait.
There was a problem hiding this comment.
I think this desugaring is wrong, since self is basically an implicit type parameter
| Note that type constraints such as `N <: GNode[E]` and `E <: GEdge[N]` are part | ||
| of the syntax for types, so we can combine them using conjunctions and | ||
| disjunctions as in the definition of `Graph[N, E]`. |
There was a problem hiding this comment.
This makes me think if I should really parse a method with a where clause as the where belonging to the return type, i.e. the difference between
print(self: Self) : Unit where (T <: Printable)
and
print(self: Self) : (Unit where (T <: Printable))
There was a problem hiding this comment.
Perhaps the syntax should be
print(self: Self) where T <: Printable : Unit
Though typing that I don't like it either. Then I thought:
print where T <: Printable(self: Self): Unit
which I like even less. So I think we need good syntax highlighting!
There was a problem hiding this comment.
T is free in the above. IS that on purpose? If it was not, perhaps the problem would not arise?
| type Printable = { | ||
| print(s: Self) : Unit // this will have to be defined if Self </: ToString | ||
| print(s: Self) : Unit where (Self <: ToString) { | ||
| sys.io.out(s.toString()) | ||
| } | ||
| } |
There was a problem hiding this comment.
Is there always a most specific constraint? There is a parallel to pattern matching where you can have a matching order that does not depend on the order that cases are written, but on their specificity, and then you need to look out for patterns that cannot be ordered, e.g., the patterns for tuples of lists (nil, l2) and (l1, nil). I wonder if a similar problem can appear here.
There was a problem hiding this comment.
don't know, we should discuss later
| Note that type constraints such as `N <: GNode[E]` and `E <: GEdge[N]` are part | ||
| of the syntax for types, so we can combine them using conjunctions and | ||
| disjunctions as in the definition of `Graph[N, E]`. |
There was a problem hiding this comment.
Perhaps the syntax should be
print(self: Self) where T <: Printable : Unit
Though typing that I don't like it either. Then I thought:
print where T <: Printable(self: Self): Unit
which I like even less. So I think we need good syntax highlighting!
|
@viewedlobster do you think you will be able to make the requested changes? |
Spelling and language
|
|
||
| ## Structural type system | ||
|
|
||
| A type system is all about managing a complexity budget. Make it too complicated |
There was a problem hiding this comment.
Nitpick: I'm not sure it is all about this! But I morally agree :)
There was a problem hiding this comment.
But this is important. We need to avoid such phrases. Perhaps: "one aspect of a type system is".
There was a problem hiding this comment.
haha, yeah, wrote that in a heated moment 😓
| // TODO add ToStringNumber version | ||
| ``` | ||
|
|
||
| In contrast, in a nominal system like Java, we would have to define a new |
There was a problem hiding this comment.
The Java equivalent of this is Object<Number, ToString>.
There was a problem hiding this comment.
I didn't know that, which version of Java added that?
There was a problem hiding this comment.
Well, technically, Objective-C 4 (I think, might have been 3), but Java inherited it from there.
| Verona. One between classes and one between class and trait. | ||
|
|
||
| ##### Class inheritance | ||
| Inheritance between classes works as you would expect in a language like |
There was a problem hiding this comment.
It is not clear from the document (at this stage) whether you allow multiple inheritance. Is this the purpose of "language like Java" here?
There was a problem hiding this comment.
Inheritance, perhaps use "reuse"?
Make clear that you can reuse code from multiple traits and classes.
| // here we reuse functionality of C in D, specifically the method f, but | ||
| // we do not get a subtyping relation D <: C | ||
| class D : C { | ||
| equal(self: D, other: D): Bool {...} |
There was a problem hiding this comment.
What would have happened if D hadn't redefined equal like this? Would it have picked up an equal : (C,C) -> Bool that then could be called with :: as in D::equal(c1,c2) but not via ., since D </: C?
There was a problem hiding this comment.
Yes. Caveat: mentioning your own type could also be treated as Self, so that D got equal: (Self, Self)->Bool, that needs discussion (it may be that such a trick leads to too many type errors in the body of the function).
More generally: I think we should favor the term "code reuse" instead of "inheritance".
|
|
||
| #### Self types | ||
| In Verona, the Self type represents the concrete type of which the object is | ||
| part. When defining class types, Self mereley acts as an alias for the |
| ``` | ||
|
|
||
| By extension this means that polymorphism in Verona doesn't need special | ||
| handling of capabilities in type parameters. A type `A[T]` parameterized on `T` |
There was a problem hiding this comment.
Might need the introduction of this notation to be a bit more gentle.
There was a problem hiding this comment.
Square bracket notation - language spec to cover. Probably should say a bit more here.
| This document aims to cover the parts of the type system that are similar to (though in some places diverge in interesting ways from) other languages. | ||
|
|
||
| Verona is an object oriented reference capability language with structural | ||
| subtyping and bounded polymorphism. This document aims to describe the aspects |
There was a problem hiding this comment.
Not sure that bounded polymorphism is the right phrase here.
| and programmers will find it difficult to use and be less productive. Make it too | ||
| simple and it will give you less guarantees to lean on as a programmer. | ||
|
|
||
| We opt to use a structural type system since we beleive it simplifies some parts |
There was a problem hiding this comment.
| We opt to use a structural type system since we beleive it simplifies some parts | |
| We opt to use a structural type system since we believe it simplifies some parts |
| ``` | ||
| A type describing numbers implementing addition and subtraction can be described with | ||
| ```verona | ||
| type Number = { |
There was a problem hiding this comment.
I wonder if Number should have a carrier for the type of Number. E.g. Number[T]
| type s = A of int | ||
| B of int |
There was a problem hiding this comment.
| type s = A of int | |
| B of int | |
| type s = A of int | |
| | B of int |
|
|
||
| #### Self types | ||
| In Verona, the Self type represents the concrete type of which the object is | ||
| part. When defining class types, Self mereley acts as an alias for the |
There was a problem hiding this comment.
| part. When defining class types, Self mereley acts as an alias for the | |
| part. When defining class types, Self merely acts as an alias for the |
| type Equal[V] = { | ||
| equals(v1: V, v2: V) : Bool | ||
| } |
There was a problem hiding this comment.
Equals not used here? Delay to next bit?
| searchGraph[V, N, E](n : N, v : V) : Option[N] | ||
| where ValueGraph[V, N, E] & (V <: Equal[V]) & (N <: Comparable[N]) | ||
| { |
| ``` | ||
|
|
||
| ### Type predicates | ||
| Type predicates allow us to describe assumptions about subtyping. These can be |
There was a problem hiding this comment.
I think for most readers the distinction between subtyping here and what we say above (i.e. " inheritance
subtyping. This means that there is never any subtyping between two distinct classes.") may be lost, i.e. they would react with "but I thought there was no subtyping in this language". Maybe it is just me, but it seems a bit confusing.
There was a problem hiding this comment.
Yes, I think this is important. We can avoid the word "inheritance" entirely. For describing predicates, I think we'll need to try several times :) We're looking for the "simplest possible" language - with no metric for what that is!
| @@ -0,0 +1,553 @@ | |||
| # The Verona language: Core type system | |||
|
|
|||
| Verona is a language with a behaviour-oriented concurrency model and a region abstraction for ownership. | |||
There was a problem hiding this comment.
General question: who is the audience for this? And what do we want the effect of reading this document to be on them?
There was a problem hiding this comment.
Add a section on the audience, expectation of the understanding the reader will get, and purpose of the document.
There was a problem hiding this comment.
Newspaper style... important first, and less important as you go.
There was a problem hiding this comment.
Tree of documents versus newspaper style? To be decided
| @@ -0,0 +1,532 @@ | |||
| # The Verona language: Features and Motivation | |||
|
|
|||
| Verona is an object oriented reference capability language with structural | |||
There was a problem hiding this comment.
I think here we should also say which parts of the type system are novel, and which are more standard.
The capabilities part seems to me not to be fully explained here. Is that so? Is that on purpose? Should there be a reference to OOPSLA?
There was a problem hiding this comment.
There was a problem hiding this comment.
Novelty should be part of the top level description.
|
|
||
| ## Structural type system | ||
|
|
||
| A type system is all about managing a complexity budget. Make it too complicated |
There was a problem hiding this comment.
But this is important. We need to avoid such phrases. Perhaps: "one aspect of a type system is".
|
|
||
| A type system is all about managing a complexity budget. Make it too complicated | ||
| and programmers will find it difficult to use and be less productive. Make it too | ||
| simple and it will give you less guarantees to lean on as a programmer. |
There was a problem hiding this comment.
Similarly, we're provoking argument with an implicit productivity claim. For this to be effective, we need to back up the claim. Also s/less/fewer/.
There was a problem hiding this comment.
Evidence on productivity? Jan Vitek paper about productivity citation. We approximate dynamic programming through the really cool typesystem.
There was a problem hiding this comment.
There was a problem hiding this comment.
| simple and it will give you less guarantees to lean on as a programmer. | ||
|
|
||
| We opt to use a structural type system since we beleive it simplifies some parts | ||
| of reasoning, e.g. we don't need co/contra-variance notation on type parameters. |
There was a problem hiding this comment.
Let's avoid the word "believe". The more concrete claim is that we are eliminating type hierarchies and improving extension (classes may be subtypes of structural types that are added later).
There was a problem hiding this comment.
Changing structure to address this.
|
|
||
| We do however treat classes nominally and have opted to not have inheritance | ||
| subtyping. This means that there is never any subtyping between two distinct | ||
| classes. |
There was a problem hiding this comment.
I would prefer to avoid the word "opted", and state our concete motivations. In this case, we are distinguishing classes from types - a class is a closed binary layout.
We also need to highlight early on here that the type system is both structural and algebraic, allowing both "open world" and "closed world" subtyping, in both cases without hierarchies.
There was a problem hiding this comment.
Class is an implicit final type, but more importantly a fixed binary layout.
Structural types are open world types.
|
|
||
| ### Traits | ||
| Verona is a structural type system based on traits, i.e. types can be described | ||
| using combination of methods on an object. E.g. we can describe a type |
There was a problem hiding this comment.
This is so minor, but: "e.g." is "for example" in Latin, requires a comma after it, and is bad form to use at the beginning of a sentence. Here it can be "object, e.g., we". "i.e." is "inter alia" and also requires a comma. Using both in the same sentence is an indicator that you probably had an entirely different structure in mind and you might want to rewrite :)
There was a problem hiding this comment.
Is the comma issue a British vs. American English thing? I agree on not starting a sentence with either though.
There was a problem hiding this comment.
I think I would put comma's in like Sylvan says, e.g., like in this sentence.
But mostly, I use
"for example" instead of "e.g."
and
"that is" instead of "i.e."
| Note that `g` cannot have a more refined type than `t -> s`. | ||
|
|
||
| #### Type discrimination | ||
| In ML we might want to construct a type such as |
There was a problem hiding this comment.
Don't introduce ML when trying to explain Verona. Instead, discuss open and closed world types, without reference to other languages.
There was a problem hiding this comment.
Define first, and compare second.
Perhaps want language comparison docs for each similar language.
X-lang for Y programmers docs - often negative signposting.. e.g., common misunderstandings.
| ``` | ||
| but it is now impossible to discriminate between the two cases. This is however | ||
| easily fixed by defining `S` instead as | ||
| ```verona |
There was a problem hiding this comment.
This is really about defining data types. There's no need to address discriminated vs. anonymous unions here - that's for a language comparison doc.
There was a problem hiding this comment.
| ``` | ||
|
|
||
| #### Explicit nullability | ||
| We can easily encode nullability with a class `None` |
There was a problem hiding this comment.
This is not "Null". A null is a value that can inhabit many types. Instead, this can be addressed as "verona uses algebraic types to express options and absence".
There was a problem hiding this comment.
Precision of Null versus option types.
| ``` | ||
|
|
||
| ### Subtyping and inheritance | ||
| Verona is an object-oriented system with classes and traits. When it comes to |
There was a problem hiding this comment.
This isn't quite right. We can remove the use of "nominal" everywhere. Classes are concrete, traits are structural (there's no nominal type relationship).
There was a problem hiding this comment.
Nominal comes with baggage from nominal subtyping, so avoid the baggage.
There was a problem hiding this comment.
Open and close world types discussion too
| Verona is an object-oriented system with classes and traits. When it comes to | ||
| subtyping, classes are treated nominally, and traits are treated structurally. | ||
| Furthermore there is no subtyping between classes. This means a class | ||
| can be a subtype of a trait, but never a subtype of a class other than itself. |
There was a problem hiding this comment.
This can be covered early in a Structural section. Introduce Eq separately in a section that shows how to build useful structural primitives, and covers F-bound polymorphism and Self types.
| equal(self: D, other: D): Bool {...} | ||
| g(...): ... { ... f(...) ... } | ||
| } | ||
| // TODO: find a realistic example |
There was a problem hiding this comment.
Meta comment: we don't need realistic examples. In fact, they can be actively harmful. Examples of languages to emulate for language docs and language specs include: Go, Rust, C#, and to some degree TypeScript (that one is problematic as it spends a lot of time referencing JavaScript).
There was a problem hiding this comment.
Realism versus teaching. Need to teach
|
|
||
| There is a case to be made for not allowing inheritance from a | ||
| class, since this allows unanticipated code reuse. This might however also be | ||
| a positive. |
There was a problem hiding this comment.
This can be removed. Language docs aren't the right place to have design discussions.
There was a problem hiding this comment.
Third type of doc... Design decisions. Neither Spec nor motivation.
| // TODO: find a realistic example | ||
| ``` | ||
| If we want to describe a relation between `C` and `D`, we can only do so by | ||
| subtyping them under a trait. |
There was a problem hiding this comment.
This isn't quite right. There may exist many relationships between C and D, based purely on structural commonality. There's no need to write a trait for such commonality to exist - this is a key point in structural subtyping.
| Here, the definition `ToString` contains a default implementation for the print | ||
| method. | ||
|
|
||
| * Question: Should traits be allowed to define default fields? |
There was a problem hiding this comment.
They already can. Also, questions are for other docs :)
There was a problem hiding this comment.
Should be addressed by the language spec.
| ###### External trait inheritance | ||
| A possibility is to allow externally declared trait inheritance, i.e. | ||
| declaration of trait inheritance can be separated from class definition. | ||
| ```verona |
There was a problem hiding this comment.
I don't understand what this means, or what the example is illustrating. Questions and design discussions are great! Let's move them to a different doc.
|
|
||
|
|
||
| ## Dynamic and static dispatch | ||
| Method calls can be dynamically or statically dispatched based on the type of |
There was a problem hiding this comment.
I think it's too early to try to give optimization tips. Perhaps the interesting thing to cover here is call syntax?
| written on both type and method level, and both has their distinct uses. | ||
| Specifically, predicates on both type and method level allow us to express | ||
| F-bounded polymorphism, while method level predicates are further useful in | ||
| reducing code duplication, somewhat akin to type classes. |
There was a problem hiding this comment.
Calling out "what something isn't" leads to confusion. Either the audience doesn't have that context, or worse yet, has it - and makes unfounded additional assumptions! Go/Rust/C# docs are very good at explaining without reference to other languages or out-of-language terminology.
| capabilities to enforce isolation and region topology. | ||
|
|
||
| We do however treat classes nominally and have opted to not have inheritance | ||
| subtyping. This means that there is never any subtyping between two distinct |
There was a problem hiding this comment.
This was answered below so now my question is why and is it multiple?
| classes. | ||
|
|
||
| ### Traits | ||
| Verona is a structural type system based on traits, i.e. types can be described |
|
|
||
| #### Capabilities and conjunction | ||
| In Verona, each concrete type is tagged with a *reference capability*. The reference | ||
| capability decides which operations are permitted through and with a reference |
| Verona also includes disjunction types. Assuming two types `C` and `D` we can | ||
| define the new type | ||
| ```verona | ||
| type COrD = C | D |
There was a problem hiding this comment.
Described as C and D above but now C or D
|
|
||
| Since in Verona there is no subtyping between classes, we are able to check that | ||
| a pattern match is exhaustive, and furthermore matching on concrete types will | ||
| allow us to do implicit type filtering over match cases. E.g. imagine a case |
There was a problem hiding this comment.
I am not 100% sure what "implicit type filtering over match cases" means
| type Eq | ||
| type ToString | ||
|
|
||
| class HashMap[K, T] where (K <: Hashable & Eq) { // type level where clause |
There was a problem hiding this comment.
Meaning of <: not described yet?
There was a problem hiding this comment.
Do we parse K <: Hashable & Eq as K <: (Hashable & Eq) or (K <: Hashable) & Eq? :)
| if (!visited.contains(next)) { | ||
| visited.add(next); | ||
| if (next.val().equals(v)) { | ||
| Some(next) |
| set(self : Self, k : K, v : T) : T { ... } | ||
| } | ||
| ``` | ||
| In a system without method-level `where` clauses, we would need to bifurcate each |
|
|
||
| A type system is all about managing a complexity budget. Make it too complicated | ||
| and programmers will find it difficult to use and be less productive. Make it too | ||
| simple and it will give you less guarantees to lean on as a programmer. |
There was a problem hiding this comment.
|
|
||
| A type system is all about managing a complexity budget. Make it too complicated | ||
| and programmers will find it difficult to use and be less productive. Make it too | ||
| simple and it will give you less guarantees to lean on as a programmer. |
There was a problem hiding this comment.
Okay, so I added a first draft of an attempt at summarizing the verona language. At the moment it mostly contains parts which I have already talked about with some of you in the weekly type system meetings. It would be great if you have a read through and comment here.