QPQ-AG/sophia
10
0
Fork 0
Code Issues 41 Pull Requests 5 Actions Packages Projects Releases 16 Wiki Activity

Docs: first part (subtyping)

Browse Source
This commit is contained in:
Gaith Hallak 2022-06-27 19:13:16 +04:00
parent 9163718a47
commit d59498914b
1 changed files with 32 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
docs/sophia_features.md
View File

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