From 4a652d53c10543ea8b585f0b734eda9e1ce3da5f Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Fri, 17 Jun 2022 14:14:18 +0400 Subject: [PATCH 01/10] Update CHANGELOG --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 218866c..623197a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 function sum(l : list(int)) : int = foldl((+), 0, l) function logical_and(x, y) = (&&)(x, y) ``` +- Contract interfaces polymorphism ### Changed - Error messages have been restructured (less newlines) to provide more unified errors. Also `pp_oneline/1` has been added. - Ban empty record definitions (e.g. `record r = {}` would give an error). -- 2.30.2 From 9163718a4763b00cb3310b75cba753830e567d70 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 26 Jun 2022 16:29:18 +0400 Subject: [PATCH 02/10] Docs: first part --- docs/sophia_features.md | 57 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index aa9e229..7b205e3 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -134,6 +134,63 @@ main contract IntHolderFactory = In case of a presence of child contracts (`IntHolder` in this case), the main contract must be pointed out with the `main` keyword as shown in the example. +### Contract interfaces and polymorphism + +Contracts can implement one or multiple interfaces, the contract has to define +every entrypoint from the implemented interface and the entrypoints in both +the contract and implemented interface should have the exact same type. + +``` +contract interface Animal = + entrypoint sound : () => string + + contract Cat : Animal = + entrypoint sound() = "Cat sound" +``` + +Contract interfaces can extend other interfaces, the extended interface has to +declare all the entrypoints from the parent interface, and it can have +additional entrypoints added to it. All the declarations in the extended +interface must match (have the same type) with the declarations from the parent +interface. + +``` +contract interface II = + entrypoint f : () => unit + +contract interface I : II = + entrypoint f : () => unit + entrypoint g : () => unit + +contract C : I = + entrypoint f() = () + entrypoint g() = () +``` + +It is only possible to implement (or extend) an interface that has been already +defined earlier in the file (or in an included file), and therefore recursive +interface implementation is not allowed in Sophia. + +``` +// The following code would show an error + +contract interface X : Z = + entrypoint x : () => int + + contract interface Y : X = + entrypoint x : () => int + entrypoint y : () => int + + contract interface Z : Y = + entrypoint x : () => int + entrypoint y : () => int + entrypoint z : () => int + + contract C : Z = + entrypoint x() = 1 + entrypoint y() = 1 + entrypoint z() = 1 +``` ## Mutable state -- 2.30.2 From d59498914bd1d9aadab76ed269e74bfccb1606b6 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 27 Jun 2022 19:13:16 +0400 Subject: [PATCH 03/10] Docs: first part (subtyping) --- docs/sophia_features.md | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index 7b205e3..b0bfa95 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -192,6 +192,38 @@ contract interface X : Z = entrypoint z() = 1 ``` +A function type `(Args1) => Ret1` is a subtype of `(Args2) => Ret2` when `Ret1` +is a subtype of `Ret2` and each argument type from `Args2` is a subtype of its +counterpart in `Args1`. + +A list type `list(A)` is a subtype of `list(B)` if `A` is a subtype of `B`. + +An option type `option(A)` is a subtype of `option(B)` if `A` is a subtype of `B`. + +A map type `map(A1, A2)` is a subtype of `map(B1, B2)` if `A1` is a subtype +of `B1`, and `A2` is a subtype of `B2`. + +An oracle type `oracle(A1, A2)` is a subtype of `oracle(B1, B2)` if `B1` is +a subtype of `A1`, and `A2` is a subtype of `B2`. + +An oracle_query type `oracle_query(A1, A2)` is a subtype of `oracle_query(B1, B2)` +if `A1` is a subtype of `B1`, and `A2` is a subtype of `B2`. + +A user-defined datatype `t(Args1)` is a subtype of `t(Args2)` + +When a user-defined type `t('a)` is covariant in `'a`, then `t(A)` is a +subtype of `t(B)` when `A` is a subtype of `B`. + +When a user-defined type `t('a)` is contravariant in `'a`, then `t(A)` is a +subtype of `t(B)` when `B` is a subtype of `A`. + +When a user-defined type `t('a)` is binvariant in `'a`, then `t(A)` is a +subtype of `t(B)` when either `A` is a subtype of `B` or when `B` is a subtype +of `A`. + +When a user-defined type `t('a)` is invariant in `'a`, then `t(A)` can never be +a subtype of `t(B)`. + ## Mutable state Sophia does not have arbitrary mutable state, but only a limited form of state -- 2.30.2 From 1514cb29498afaf3e46a908735af3423b0a3742e Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Thu, 7 Jul 2022 20:28:59 +0400 Subject: [PATCH 04/10] Update docs/sophia_features.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Radosław Rowicki <35342116+radrow@users.noreply.github.com> --- docs/sophia_features.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index b0bfa95..1a64037 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -168,7 +168,7 @@ contract C : I = ``` It is only possible to implement (or extend) an interface that has been already -defined earlier in the file (or in an included file), and therefore recursive +defined earlier in the file (or in an included file). Therefore recursive interface implementation is not allowed in Sophia. ``` -- 2.30.2 From 66f56a0eb2436ee2c24bfdb84e3733883322fbde Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Thu, 7 Jul 2022 20:30:07 +0400 Subject: [PATCH 05/10] Update docs/sophia_features.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Radosław Rowicki <35342116+radrow@users.noreply.github.com> --- docs/sophia_features.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index 1a64037..dc227fc 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -148,10 +148,9 @@ contract interface Animal = entrypoint sound() = "Cat sound" ``` -Contract interfaces can extend other interfaces, the extended interface has to -declare all the entrypoints from the parent interface, and it can have -additional entrypoints added to it. All the declarations in the extended -interface must match (have the same type) with the declarations from the parent +Contract interfaces can extend other interfaces. An extended interface has to +declare all entrypoints from every parent interface. All the declarations in the extended +interface must have the same type as the declarations from the parent interface. ``` -- 2.30.2 From 2dd461b2b0b9a397ac5aff27b0e94c209dc1ca5b Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 25 Jul 2022 00:28:58 +0400 Subject: [PATCH 06/10] Update docs/sophia_features.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Radosław Rowicki <35342116+radrow@users.noreply.github.com> --- docs/sophia_features.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index dc227fc..04a9147 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -150,7 +150,7 @@ contract interface Animal = Contract interfaces can extend other interfaces. An extended interface has to declare all entrypoints from every parent interface. All the declarations in the extended -interface must have the same type as the declarations from the parent +interface must have types compatible with the declarations from the parent interface. ``` -- 2.30.2 From 41c0609837588db08bb611cb2c19380216381e68 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 25 Jul 2022 00:31:36 +0400 Subject: [PATCH 07/10] Change "the same type" to "compatible types" --- docs/sophia_features.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index 04a9147..3d8b99d 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -138,7 +138,7 @@ contract must be pointed out with the `main` keyword as shown in the example. Contracts can implement one or multiple interfaces, the contract has to define every entrypoint from the implemented interface and the entrypoints in both -the contract and implemented interface should have the exact same type. +the contract and implemented interface should have compatible types. ``` contract interface Animal = -- 2.30.2 From 6c8715ea74d872471bf273816334cb14f627d19d Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 25 Jul 2022 00:38:44 +0400 Subject: [PATCH 08/10] Formatting for subtyping rules --- docs/sophia_features.md | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index 3d8b99d..f79c531 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -191,36 +191,38 @@ contract interface X : Z = entrypoint z() = 1 ``` -A function type `(Args1) => Ret1` is a subtype of `(Args2) => Ret2` when `Ret1` +The following subtyping rules apply: + +- A function type `(Args1) => Ret1` is a subtype of `(Args2) => Ret2` when `Ret1` is a subtype of `Ret2` and each argument type from `Args2` is a subtype of its counterpart in `Args1`. -A list type `list(A)` is a subtype of `list(B)` if `A` is a subtype of `B`. +- A list type `list(A)` is a subtype of `list(B)` if `A` is a subtype of `B`. -An option type `option(A)` is a subtype of `option(B)` if `A` is a subtype of `B`. +- An option type `option(A)` is a subtype of `option(B)` if `A` is a subtype of `B`. -A map type `map(A1, A2)` is a subtype of `map(B1, B2)` if `A1` is a subtype +- A map type `map(A1, A2)` is a subtype of `map(B1, B2)` if `A1` is a subtype of `B1`, and `A2` is a subtype of `B2`. -An oracle type `oracle(A1, A2)` is a subtype of `oracle(B1, B2)` if `B1` is +- An oracle type `oracle(A1, A2)` is a subtype of `oracle(B1, B2)` if `B1` is a subtype of `A1`, and `A2` is a subtype of `B2`. -An oracle_query type `oracle_query(A1, A2)` is a subtype of `oracle_query(B1, B2)` +- An oracle_query type `oracle_query(A1, A2)` is a subtype of `oracle_query(B1, B2)` if `A1` is a subtype of `B1`, and `A2` is a subtype of `B2`. -A user-defined datatype `t(Args1)` is a subtype of `t(Args2)` +- A user-defined datatype `t(Args1)` is a subtype of `t(Args2)` -When a user-defined type `t('a)` is covariant in `'a`, then `t(A)` is a +- When a user-defined type `t('a)` is covariant in `'a`, then `t(A)` is a subtype of `t(B)` when `A` is a subtype of `B`. -When a user-defined type `t('a)` is contravariant in `'a`, then `t(A)` is a +- When a user-defined type `t('a)` is contravariant in `'a`, then `t(A)` is a subtype of `t(B)` when `B` is a subtype of `A`. -When a user-defined type `t('a)` is binvariant in `'a`, then `t(A)` is a +- When a user-defined type `t('a)` is binvariant in `'a`, then `t(A)` is a subtype of `t(B)` when either `A` is a subtype of `B` or when `B` is a subtype of `A`. -When a user-defined type `t('a)` is invariant in `'a`, then `t(A)` can never be +- When a user-defined type `t('a)` is invariant in `'a`, then `t(A)` can never be a subtype of `t(B)`. ## Mutable state -- 2.30.2 From 2ea56ce7efd2b49fa92b4520268c704103846f0f Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 25 Jul 2022 01:10:00 +0400 Subject: [PATCH 09/10] Note about type variance --- docs/sophia_features.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index f79c531..50851bf 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -191,7 +191,15 @@ contract interface X : Z = entrypoint z() = 1 ``` -The following subtyping rules apply: +#### Subtyping + +The subtyping rules below, mention the variance of a type, which is defined in [Wikipedia](https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)) as follows: + +>Variance refers to how subtyping between more complex types relates to subtyping between their components. + +You can refer to the Wikipedia page for further understanding of type variance. + +In Sophia, the following subtyping rules apply: - A function type `(Args1) => Ret1` is a subtype of `(Args2) => Ret2` when `Ret1` is a subtype of `Ret2` and each argument type from `Args2` is a subtype of its -- 2.30.2 From 136f96a422cb7cd4b046e8f6577d64774ff64789 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 25 Jul 2022 20:31:28 +0400 Subject: [PATCH 10/10] Update docs/sophia_features.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Radosław Rowicki <35342116+radrow@users.noreply.github.com> --- docs/sophia_features.md | 59 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 55 insertions(+), 4 deletions(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index 50851bf..1092201 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -191,15 +191,66 @@ contract interface X : Z = entrypoint z() = 1 ``` -#### Subtyping +#### Subtyping and variance -The subtyping rules below, mention the variance of a type, which is defined in [Wikipedia](https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)) as follows: +Subtyping in Sophia follows common rules that take type variance into account. As described by [Wikipedia](https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)), >Variance refers to how subtyping between more complex types relates to subtyping between their components. -You can refer to the Wikipedia page for further understanding of type variance. +This concept plays an important role in complex types such as tuples, `datatype`s and functions. Depending on the context, it can apply to positions in the structure of a type, or type parameters of generic types. There are four kinds of variances: -In Sophia, the following subtyping rules apply: +- covariant +- contravariant +- invariant +- bivariant + +A type is said to be on a "covariant" position when it describes output or a result of some computation. Analogously, position is "contravariant" when it is an input, or a parameter. Intuitively, when a part of the type is produced by values of it, it is covariant. When it is consumed, it is contravariant. When a type appears to be simultaneously input and output, it is described as invariant. If a type is neither of those (that is, it's unused) it's bivariant. Furthermore, whenever a complex type appears on a contravariant position, all its covariant components become contravariant and vice versa. + +Variance influences how subtyping is applied. Types on covariant positions are subtyped normally, while contravariant the opposite way. Invariant types have to be exactly the same in order for subtyping to work. Bivariant types are always compatible. + +A good example of where it matters can be pictured by subtyping of function types. Let us assume there is a contract interface `Animal` and two contracts that implement it: `Dog` and `Cat`. + +```sophia +contract interface Animal = + entrypoint age : () => int + +contract Dog : Animal = + entrypoint age() = // ... + entrypoint woof() = "woof" + +contract Cat : Animal = + entrypoint age() = // ... + entrypoint meow() = "meow" +``` + +The assumption of this exercise is that cats do not bark (because `Cat` does not define the `woof` entrypoint). If subtyping rules were applied naively, that is if we let `Dog => Dog` be a subtype of `Animal => Animal`, the following code would break: + +```sophia +let f : (Dog) => string = d => d.woof() +let g : (Animal) => string = f +let c : Cat = Chain.create() +g(c) // Cat barking! +``` + +That is because arguments of functions are contravariant, as opposed to return the type which is covariant. Because of that, the assignment of `f` to `g` is invalid - while `Dog` is a subtype of `Animal`, `Dog => string` is **not** a subtype of `Animal => string`. However, `Animal => string` **is** a subtype of `Dog => string`. More than that, `(Dog => Animal) => Dog` is a subtype of `(Animal => Dog) => Animal`. + +This has consequences on how user-defined generic types work. A type variable gains its variance from its role in the type definition as shown in the example: + +```sophia +datatype co('a) = Co('a) // co is covariant on 'a +datatype ct('a) = Ct('a => unit) // ct is contravariant on 'a +datatype in('a) = In('a => 'a) // in is invariant on 'a +datatype bi('a) = Bi // bi is bivariant on 'a +``` + +The following facts apply here: + +- `co('a)` is a subtype of `co('b) when `'a` is a subtype of `'b` +- `ct('a)` is a subtype of `ct('b) when `'b` is a subtype of `'a` +- `in('a)` is a subtype of `in('b) when `'a` is equal to `'b` +- `bi('a)` is a subtype of `bi('b) always + +That altogether induce the following rules of subtyping in Sophia: - A function type `(Args1) => Ret1` is a subtype of `(Args2) => Ret2` when `Ret1` is a subtype of `Ret2` and each argument type from `Args2` is a subtype of its -- 2.30.2