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

Add comparable typevar constraints #881

Open
ghallak wants to merge 15 commits from ghallak/229 into master
pull from: ghallak/229
merge into: QPQ-AG:master
Conversation 18 Commits 15 Files Changed 15 +38 -46
1 changed files with 38 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit e8da0a7cfe - Show all commits

84
docs/sophia_features.md
View File

@ -502,66 +502,58 @@ function
Guards cannot be stateful even when used inside a stateful function. Guards cannot be stateful even when used inside a stateful function.
## Constrainted type variables ## Comparable types
Comparing types by equality (using `==` and `!=`) or by inequality Only certain types are allowed to be compared by equality (`==`, `!=`) and
(using `<`, `>`, `<=`, `=<`, and `>=`) only makes sense by some types. inequality (`<`, `>`, `=<`, `>=`). For instance, while it is legal to compare
For example, it is possible to compare two `int`s by inequality integers, comparing functions would lead to an error:
(e.g. `1 < 2`), but it would not make sense to compare two instances of
a contract by inequality.
``` ```
contract C = ... function f() =
contract Main = f == f // type error
function f(x : C, y : c) = x > y // this is wrong
``` ```
This is solved in Sophia by adding type variable constraints The rules apply as follows:
(`ord` and `eq`) to limit what can be passed to the binary comparison
operators.
The type of the equality comparison operators is `'a is eq ; ('a, 'a) => bool` - All types that are comparable by inequality are also comparable by equality.
and of the inequality comparison operators is `'a is ord ; ('a, 'a) => bool` - The builtin types `bool`, `int`, `char`, `bits`, `bytes`, `string`, `unit`,
which means that these operators can only accept types that are comparable by `hash`, `address` and `signature` are comparable by inequality (and thus by
equality or by inequality respectively. equality).
- The composite types `list`, `option`, and tuples are comparable by
equality/inequality if their type parameters are comparable by
equality/inequality.
- The composite types `map`, `oracle`, and `oracle_query` are comparable by
equality if their type parameters are comparable by equality.
- User-defined records and datatypes are comparable by equality if their type
parameters are comparable by equality.
- Smart contracts are comparable by equality.
- User-declared type variables are comparable according to the [type
constraints](#type-constraints) given in the function signature.
The builtin types `bool`, `int`, `char`, `bits`, `bytes`, `string`, `hash`, In all other cases the types are not comparable.
and `signature` are comparable by inequality (and equality) while the types
`address`, `event` are only comparable by equality.
The composite types `list`, `option`, and `tuple` are comparable by inequality ### Type constraints
if and only if their type argmuments are comparable by inequality.
The composite types `map`, `oracle`, and `oracle_query` are comparable by Polymorphic types are not declared as comparable by default. If the user
equality if and only if their type arguments are comparable by equality. specifies the type signature for a function, they need to manually declare type
constraints in order to allow the variables to be compared. This can only be
All user-defined records and datatypes are comparable by equality if their done if the type declaration is separated from the function definition. The
type arguments are also comparable by equality. In addition to that, all constraints have to be prepended to the type declaration and separated with a
user-defined contracts are comparable by equality. semicolon:
Anonymous functions (or lambda functions) are not comparable neither by
equality nor by inequality.
All types that are comparable by inequality are also comparable by equality.
In other words, if a type has `ord` constraint, that implies that it also
have `eq` constraint.
The type variable constraints can be specified in the type signature of any
function.
``` ```
// Comparison with < is only allowed because 'a has the constraint ord
lt : 'a is ord ; ('a, 'a) => bool
lt(x, y) = x < y
// Multiple constraints can be specified function eq(x : 'a, y : 'a) = x == y // Type error, 'a is not comparable
ord_and_eq : 'a is ord, 'b is eq ; ('a, 'a, 'b, 'b) => bool
ord_and_eq(x, y, p, q) = x > y && p == q function
eq : 'a is eq ; ('a, 'a) => bool
eq(x, y) = x == y // Compiles
function eq(x, y) = x == y // Compiles as the constraints are inferred
``` ```
If the constraints are not mentioned, the type variable is assumed to Currently only two constraints are allowed: `eq` for equality and `ord` for
have no constraints, and calling any equality or inequality operation inequality. Declaring a type as `ord` automatically implies `eq`.
on it will cause an error.
## Lists ## Lists