diff --git a/docs/motivation.md b/docs/motivation.md new file mode 100644 index 000000000..81e49c0a4 --- /dev/null +++ b/docs/motivation.md @@ -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. +These are fundamentally new abstractions in language design and are covered separately. +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 +of the type system that are independent from both the concurrency model and +reference capabilities. + +## Structural type system + +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. + +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. +This allows us to spend this complexity elsewhere, e.g. introducing reference +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 +classes. + +### 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 +implementing a `toString` method as +```verona +type ToString = { + toString(self: Self): String +} +``` +A type describing numbers implementing addition and subtraction can be described with +```verona +type Number = { + add(self: Self, other: Number): Number + sub(self: Self, other: Number): Number +} +``` +Traits also support default implementation as described below in section [Trait Inheritance](#trait-inheritance). + + +### Conjunction types +We can easily combine traits using conjunctions, so if we, e.g., want to describe +something implementing both `ToString` and `Number`, this can be written as +```verona +type ToStringNumber = ToString & Number +``` + +This gives us a flexible way to define combinations of types on the fly, with an +intuitive syntax. For example, if we want to describe the type signature of a function +`f` printing two numbers and then returning the result of adding them +together, this would be +```verona +f(n1: Number & ToString, n2: Number & ToString) : Number +``` +or equivalently +```verona +f(n1: ToStringNumber, n2: ToStringNumber) : Number +``` + +In contrast, in a nominal system like Java, we would have to define a new +interface `ToStringNumber` that extends both `Number` and `ToString`: +```java +interface ToStringNumber extends Number, ToString { ... } + +class C { + static Number f(ToStringNumber n1, ToStringNumber n2) { ... } +} +``` +Furthermore we would have to change the definition of every class that we want +to implement this new trait. + +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. For example, 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 +} +``` + +#### 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 +depending on the viewpoint. For example, a reference with capability `mut` allows us to +read and mutate the object, while a capability `iso` is unique and opaque to all +read/write operations. + +The conjunction type operator plays well together with capabilities, allowing us +to express capability tags as part of the regular type system. For example, given a class +`C` we can express the type of a reference to an object of class type `C` with +reference capability `mut` as +```verona +type CMut = C & mut +``` + +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` +can simply be instantiated with a type like `C & mut`. The method types of `A` +are then able to express further restrictions on `T` that allow us to define +operations for each instantiation. +```verona +type A[T] = { + withImm(v : T & imm) : A[T] & imm // immutable A[T] created with immutable T + withMut(v : T & mut) : A[T] & mut // mutable A[T] created with mutable T +} +``` + +* TODO: compare with + - objective c: categories + - ruby: open classes + - C#: extension methods + +### Disjunction types +Verona also includes disjunction types. Assuming two types `C` and `D` we can +define the new type +```verona +type COrD = C | D +``` +This describes the union of the two types. + +If we assume `C` and `D` above are classes, we can furthermore write pattern +matches to distinguish between the two types dynamically. + +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 +match like this +```verona +// C, D, E are classes + +f(x : C | D | E, g : (D | E) -> S) : S { + match x with { + (y : C) => { // y : C + ... + } + _ => { // x : D | E + g x + } + } +} +``` +We are able to implicitly filter the type of `x` in the default case. + +In a language like ML, the corresponding code would look like +```ocaml +type t = C of c + | D of d + | E of e + + +f (x : t) (g : t -> s) = + match x with + C y => ... + _ => g x +``` +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 +```ocaml +type s = A of int + B of int +``` +A corresponding Verona type might look like +```verona +type S = I32 | I32 +``` +but it is now impossible to discriminate between the two cases. This is however +easily fixed by defining `S` instead as +```verona +class A { var i : I32 } +class B { var i : I32 } + +type S = A | B +``` + +#### Explicit nullability +We can easily encode nullability with a class `None` +```verona +type A +class None {} + +f(x : A | None) : S { + match x with { + (y: A) => { // y : A + ... + } + _ => { // x : None + ... + } + } +} +``` + +### Subtyping and inheritance +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. +For example, given the definitions +```verona +class C { + equal(self: C, other: C): Bool {...} +} + +class D { + equal(self: D, other: D): Bool {...} +} + +type Eq = { + equal(self: Self, other: Self) : Bool +} + +``` +both `C` and `D` are subtypes of `Eq`, but neither `C` or `D` are subtypes of +the other. + +#### Inheritance +There are two forms of inheritance in +Verona. One between classes and one between class and trait. + +##### Class inheritance +Inheritance between classes works as you would expect in a language like +Java, with the exception that it does not imply subtyping. As an example, +consider +```verona +class C { + equal(self: C, other: C): Bool {...} + f(...) : ... {...} +} + +// 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 {...} + g(...): ... { ... f(...) ... } +} +// 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 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. + +##### Trait inheritance +Traits can be used for inheritance with their default methods. +```verona +type ToString = { + toString(s: Self) : String + print(s: Self) : Unit { + sys.print(s.toString()) + } +} + +class C : ToString { + toString(s: C) : String { + ... + } +} +// here C will inherit the default implementation of print +``` +Here, the definition `ToString` contains a default implementation for the print +method. + +* Question: Should traits be allowed to define default fields? + +###### 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 ToString together with its default print method +class C : ToString +``` + + +#### 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 +instantiation of this class type itself: +```verona +class C { + m1(self: Self) : Self + m2(self: C) : C + // in verona, these two method signatures are equivalent up to method name. +} +``` + +For trait types, Self acts as as a reference to the underlying concrete type of the instantiation. This allows us to write e.g. +```verona +type Collection[T] = { + add(self: Self, e: T) : Self +} +``` +where the `add` method returns something of the concrete type, e.g. +`list.add(x)` returns the type `List[T]` rather than `Collection[T]`. + + +## Dynamic and static dispatch +Method calls can be dynamically or statically dispatched based on the type of +the receiver. If the receiver is a concrete class type, the compiler will +produce a static dispatch. If on the other hand, it is something more complex, e.g., a +disjunction type or a trait type, the method call will be dispatched +dynamically. The compiler will of course try to optimize if the complex type is +simple enough, e.g., `C | D` in the example below, but this happens on a case by +case basis and the language specification will promise no such thing. +```verona +// classes C and D has method toString +let x : C = C::create() +let s = x.toString() // static dispatch, since C is a concrete (closed) type + +let y : C | D = if (...) { C::create() } else { D::create() } +let t = y.toString() // dynamic dispatch, since C | D is a complex (albeit closed) type +// it could however be optimized into something like this, since C | D is a closed world type +let t = match y with { + C => y.toString() // allows method call inlining since call is now static + D => y.toString() +} + +let z : ToString = if (...) { C::create() } else { D::create() } +let u = z.toString() // dynamic dispatch, since ToString is an open type +``` + +### Type predicates +Type predicates allow us to describe assumptions about subtyping. These can be +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. + +In verona these predicates can be added to types and method signatures using the +keyword `where`. Here are a couple of examples: +```verona +type Hashable +type Eq +type ToString + +class HashMap[K, T] where (K <: Hashable & Eq) { // type level where clause + ... +} + +type StringStream = { + put[T](self: Self, o : T) : Unit where (T <: ToString) // method level where clause + ... +} +``` + +#### Type-level `where` clauses +As mentioned above, type predicates on type level are useful when we have to +describe bounds on type parameters. As an example, consider the class of +red-black tree: +```verona +class LT {} +class EQ {} +class GT {} + +type Ord = LT | EQ | GT + +type Comparable[T] = { + compare(self: Self, other: T): Ord +} + +class RBTree[T] where (T <: Comparable[T]) { ... } +``` + +The constraint `T <: Comparable[T]` is exactly the constraint that would be +present for the corresponding definition of a red-black tree in a system with +F-bounded polymorphism. + +Also consider a polymorphic type describing a graph: +```verona +type GNode[E] = { + edges(self: Self) : Iterable[E] +} + +type GEdge[N] = { + src(self: Self) : N + dst(self: Self) : N +} + +type Graph[N, E] = (N <: GNode[E]) & (E <: GEdge[N]) +``` +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]`. + +Continuing we can describe a graph where each node contains a value: +```verona +type Container[V] = { + val(self: Self) : V +} + +type Equal[V] = { + equals(v1: V, v2: V) : Bool +} + +type ValueGraph[V, N, E] = Graph[N, E] & (N <: Container[V]) +``` +Note that we can simply combine the previous definition of `Graph[N, E]` with a +new constraint describing the new constraint on nodes. + +We can write a simple search algorithm that is polymorphic in the type of nodes and edges. +```verona +searchGraph[V, N, E](n : N, v : V) : Option[N] + where ValueGraph[V, N, E] & (V <: Equal[V]) & (N <: Comparable[N]) +{ + let visited = Set[N]::create(); + let pending = Queue[N]::create({n}); + + while (!pending.empty()) { + let next = pending.dequeue(); + + if (!visited.contains(next)) { + visited.add(next); + if (next.val().equals(v)) { + Some(next) + } + else { + for (edge : next.edges()) { + pending.enqueue(edge.dst()); + } + } + } + } + + None +} +``` + +#### Method-level `where` clauses +Adding type constraints to methods, we can condition the existence of a method +depending on the specific type parameters. Going back to the red-black tree +example above, we can add a `print` method that will exist only when the +type parameter to `RBTree` implements the `Printable` trait: +```verona +class RBTree[T] where (T <: Comparable[T]) { + ... + print(self: Self) : Unit where (T <: Printable) { + ... + } +} +``` + +##### `where` clauses and capabilities +Another use for method-level `where` clauses is to restrict which methods can be +called depending the capabilities of type parameters. +```verona +class Ref[T] { + var val : T + get(self: Self) : T where T <: mut | imm // i.e. not iso + { + val + } + set(self: Self, v : T) : T { val = v } +} + +class Array[T] { + // uses Ref[T] internally + ... + get(self: Self, idx : U32) : T where T <: mut | imm // i.e. not iso + { + ... + } + set(self: Self, idx : U32, v : T) : T { ... } +} + +class HashMap[K, T] { + ... // built on top of Array[T] + get(self : Self, k : K) : T where T <: mut | imm // i.e. not iso + { + ... + } + set(self : Self, k : K, v : T) : T { ... } +} +``` +In a system without method-level `where` clauses, we would need to bifurcate each +class on whether the class should be able to handle iso values or not, e.g., +having to define both `IsoRef[T]` and `Ref[T]`. Furthermore, `where` clauses on +methods are very intentional, and allows us to give better error messages. For example, +"`Ref[iso & A]::get()` not available since `iso & A