Update the documentation and changelog to include polymorphism #887

2022-06-26T21:33:36+09:00

ghallak commented

2022-06-26 21:33:36 +09:00

(Migrated from gitlab.com)

No description provided.

zxq9 commented

2022-06-26 23:12:39 +09:00

(Migrated from gitlab.com)

Created by: radrow

Contracts can implement one or more interfaces. For that, a contract has to implement
every entrypoint declared in that interface. The implementation has to match the type of the declaration in the interface.

...does it really need to be exact? Can't it be a supertype?

*Created by: radrow* ```suggestion:-0+0 Contracts can implement one or more interfaces. For that, a contract has to implement every entrypoint declared in that interface. The implementation has to match the type of the declaration in the interface. ``` ...does it really need to be exact? Can't it be a supertype?

zxq9 commented

2022-06-26 23:14:36 +09:00

(Migrated from gitlab.com)

Created by: radrow

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.

*Created by: radrow* ```suggestion:-0+0 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. ```

zxq9 commented

2022-06-26 23:15:17 +09:00

(Migrated from gitlab.com)

Created by: radrow

defined earlier in the file (or in an included file). Therefore recursive
interface implementation is not allowed in Sophia.

*Created by: radrow* ```suggestion:-0+0 defined earlier in the file (or in an included file). Therefore recursive interface implementation is not allowed in Sophia. ```

ghallak commented

2022-07-08 01:49:34 +09:00

(Migrated from gitlab.com)

It can be a supertype, should I mention that?

zxq9 commented

2022-07-08 22:58:51 +09:00

(Migrated from gitlab.com)

Created by: radrow

Of course

*Created by: radrow* Of course

zxq9 commented

2022-07-24 00:44:16 +09:00

(Migrated from gitlab.com)

Created by: radrow

interface must have types compatible with the declarations from the parent

*Created by: radrow* ```suggestion:-0+0 interface must have types compatible with the declarations from the parent ```

zxq9 commented

2022-07-24 00:45:17 +09:00

(Migrated from gitlab.com)

Created by: radrow

Maybe format it as a list?

*Created by: radrow* Maybe format it as a list?

zxq9 commented

2022-07-24 00:46:28 +09:00

(Migrated from gitlab.com)

Created by: radrow

Something like

The following subtyping rules apply:

blablabla

...

*Created by: radrow* Something like > The following subtyping rules apply: > > - blablabla > - ...

zxq9 commented

2022-07-24 00:47:02 +09:00

(Migrated from gitlab.com)

Created by: radrow

Explain briefly variance below and link to wikipedia

*Created by: radrow* Explain briefly variance below and link to wikipedia

ghallak commented

2022-07-25 05:32:09 +09:00

(Migrated from gitlab.com)

Changed here 41c0609837

Changed here 41c0609837588db08bb611cb2c19380216381e68

ghallak commented

2022-07-25 05:46:23 +09:00

(Migrated from gitlab.com)

Done here 6c8715ea74

Done here 6c8715ea74d872471bf273816334cb14f627d19d

ghallak commented

2022-07-25 06:11:19 +09:00

(Migrated from gitlab.com)

Done here 2ea56ce7ef

Done here 2ea56ce7efd2b49fa92b4520268c704103846f0f

zxq9 commented

2022-07-26 01:25:50 +09:00

(Migrated from gitlab.com)

Created by: radrow

#### Subtyping and variance

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.

This concept plays an important role in subtyping of complex types such as tuples, `datatype`s and functions. Depending on the context, it can apply to positions in the structure of types, or type parameters of generic types. There are four kinds of variances:

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

*Created by: radrow* ````suggestion #### Subtyping and variance 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. This concept plays an important role in subtyping of complex types such as tuples, `datatype`s and functions. Depending on the context, it can apply to positions in the structure of types, or type parameters of generic types. There are four kinds of variances: - 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: ````

zxq9 commented

2022-07-26 01:32:51 +09:00

(Migrated from gitlab.com)

Created by: radrow

Review: Approved

*Created by: radrow* **Review:** Approved

zxq9 commented

2022-07-26 01:39:32 +09:00

(Migrated from gitlab.com)

Created by: hanssv

Review: Approved

*Created by: hanssv* **Review:** Approved

zxq9 commented

2022-07-26 01:47:17 +09:00

(Migrated from gitlab.com)

Merged by: radrow at 2022-07-25 16:47:17 UTC

*Merged by: radrow at 2022-07-25 16:47:17 UTC*

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: QPQ-AG/sophia#887