-
Notifications
You must be signed in to change notification settings - Fork 167
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
Adding language motivation document #649
base: master
Are you sure you want to change the base?
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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a really useful document to have! I have added some comments and questions, and also opened a pull request with spelling fixes.
docs/motivation.md
Outdated
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yeah, i agree, i'll see if i have time to write something before the meeting
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"syntactic sugar" ==> "can also be understood as"
I think our readers do not care about syntactic sugar.
docs/motivation.md
Outdated
###### 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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Compared to the previous example, it is the ToString
trait that implements print
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nitpick: I'm not sure it is all about this! But I morally agree :)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The Java equivalent of this is Object<Number, ToString>
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I didn't know that, which version of Java added that?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
1.0
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
typo 'mereley'
``` | ||
|
||
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Might need the introduction of this notation to be a bit more gentle.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not sure that bounded polymorphism is the right phrase here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Predicated polymorphism.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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]) | ||
{ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is method level where
.
``` | ||
|
||
### Type predicates | ||
Type predicates allow us to describe assumptions about subtyping. These can be |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Newspaper style... important first, and less important as you go.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
``` | ||
|
||
#### Explicit nullability | ||
We can easily encode nullability with a class `None` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nominal comes with baggage from nominal subtyping, so avoid the baggage.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This can be removed. Language docs aren't the right place to have design discussions.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
They already can. Also, questions are for other docs :)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we even have inheritance?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: has not is
|
||
#### 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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Some broken language here
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Meaning of <: not described yet?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should there be a return
here?
set(self : Self, k : K, v : T) : T { ... } | ||
} | ||
``` | ||
In a system without method-level `where` clauses, we would need to bifurcate each |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great!
|
||
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
|
||
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.