Skip to content
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

Draft
wants to merge 6 commits into
base: master
Choose a base branch
from

Conversation

ln-sol
Copy link

@ln-sol ln-sol commented Dec 6, 2023

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.

@ln-sol
Copy link
Author

ln-sol commented Dec 6, 2023

Some things i need to do

  • Make sure syntax is correct in code examples
  • Add comparisons with other languages

@davidchisnall
Copy link
Contributor

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.

@ln-sol
Copy link
Author

ln-sol commented Dec 7, 2023

@microsoft-github-policy-service agree

@ln-sol
Copy link
Author

ln-sol commented Dec 7, 2023

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.

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.

Copy link

@EliasC EliasC left a 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.

Comment on lines 61 to 70
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
}
```
Copy link

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.

Copy link
Author

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?

Copy link

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).

Copy link
Author

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

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.

Comment on lines 256 to 271
###### 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
```
Copy link

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)?

Copy link

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.

Copy link
Author

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

Comment on lines 308 to 317
```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
}
```
Copy link

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.

Copy link
Author

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

Comment on lines +404 to +406
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]`.
Copy link

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))

Copy link
Member

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!

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?

Comment on lines +515 to +520
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())
}
}
Copy link

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.

Copy link
Author

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

Comment on lines +404 to +406
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]`.
Copy link
Member

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!

@mjp41
Copy link
Member

mjp41 commented Mar 1, 2024

@viewedlobster do you think you will be able to make the requested changes?


## Structural type system

A type system is all about managing a complexity budget. Make it too complicated

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 :)

Copy link
Member

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".

Copy link
Author

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
Copy link
Contributor

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>.

Copy link
Member

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?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

1.0

Copy link
Contributor

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
Copy link
Member

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?

Copy link
Member

@mjp41 mjp41 Mar 20, 2024

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 {...}
Copy link

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?

Copy link
Member

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
Copy link
Member

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`
Copy link
Member

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.

Copy link
Member

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
Copy link
Member

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.

Copy link
Member

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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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 = {
Copy link
Member

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]

Comment on lines +165 to +166
type s = A of int
B of int
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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

Comment on lines +407 to +409
type Equal[V] = {
equals(v1: V, v2: V) : Bool
}
Copy link
Member

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?

Comment on lines +418 to +420
searchGraph[V, N, E](n : N, v : V) : Option[N]
where ValueGraph[V, N, E] & (V <: Equal[V]) & (N <: Comparable[N])
{
Copy link
Member

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
Copy link
Member

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.

Copy link
Member

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.
Copy link
Member

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?

Copy link
Member

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.

Copy link
Member

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.

Copy link
Member

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

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?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copy link
Member

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
Copy link
Member

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.
Copy link
Member

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/.

Copy link
Member

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.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
Copy link
Member

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).

Copy link
Member

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.
Copy link
Member

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.

Copy link
Member

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
Copy link
Member

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 :)

Copy link

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.

Copy link
Member

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
Copy link
Member

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.

Copy link
Member

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
Copy link
Member

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.

Copy link
Member

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`
Copy link
Member

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".

Copy link
Member

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
Copy link
Member

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).

Copy link
Member

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.

Copy link
Member

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.
Copy link
Member

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
Copy link
Member

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).

Copy link
Member

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.
Copy link
Member

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.

Copy link
Member

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.
Copy link
Member

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?
Copy link
Member

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 :)

Copy link
Member

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
Copy link
Member

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
Copy link
Member

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.
Copy link
Member

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

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?

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

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

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

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

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

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?

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)

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

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.

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.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ln-sol ln-sol marked this pull request as draft March 27, 2024 15:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

9 participants