Add comparable typevar constraints #881

2022-06-14T23:23:45+09:00

ghallak commented

2022-06-14 23:23:45 +09:00

(Migrated from gitlab.com)

Fixes: #229

zxq9 commented

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

(Migrated from gitlab.com)

Created by: radrow

Good opportunity to actually give some example address here

*Created by: radrow* Good opportunity to actually give some example address here

zxq9 commented

2022-06-18 19:34:05 +09:00

(Migrated from gitlab.com)

Created by: radrow

formatting

*Created by: radrow* formatting

zxq9 commented

2022-06-18 19:35:15 +09:00

(Migrated from gitlab.com)

Created by: radrow

Where are eq_constraint_types?

*Created by: radrow* Where are eq_constraint_types?

zxq9 commented

2022-06-18 19:44:16 +09:00

(Migrated from gitlab.com)

Created by: radrow

Please write tests for type inference:

function f(x) = x == x // PASS

function g() = f(g) // FAIL

*Created by: radrow* Please write tests for type inference: ``` function f(x) = x == x // PASS function g() = f(g) // FAIL ```

zxq9 commented

2022-06-18 20:18:41 +09:00

(Migrated from gitlab.com)

Created by: radrow

I would use less "judging" language and more "factful". Also, restructured a little bit.

## Comparable types

Only certain types are allowed to be compared by equality (`==`, `!=`) and
inequality (`<`, `>`, `=<`, `>=`). For instance, while it is legal to compare
integers, comparing functions would lead to an error:

```
function f() = 
  f == f  // type error
```

The rules apply as follows:

- All types that are comparable by inequality are also comparable by equality.
- The builtin types `bool`, `int`, `char`, `bits`, `bytes`, `string`, `unit`,
  `hash`, `address` and `signature` are comparable by inequality (and thus by
  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.

In all other cases the types are not comparable.

### Type constraints

Polymorphic types are not declared as comparable by default. If the user
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
done if the type declaration is separated from the function definition. The
constraints have to be prepended to the type declaration and separated with a
semicolon:

```

function eq(x : 'a, y : 'a) = x == y  // Type error, 'a is not comparable

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

Currently only two constraints are allowed: `eq` for equality and `ord` for
inequality. Declaring a type as `ord` automatically implies `eq`.

*Created by: radrow* I would use less "judging" language and more "factful". Also, restructured a little bit. ````suggestion ## Comparable types Only certain types are allowed to be compared by equality (`==`, `!=`) and inequality (`<`, `>`, `=<`, `>=`). For instance, while it is legal to compare integers, comparing functions would lead to an error: ``` function f() = f == f // type error ``` The rules apply as follows: - All types that are comparable by inequality are also comparable by equality. - The builtin types `bool`, `int`, `char`, `bits`, `bytes`, `string`, `unit`, `hash`, `address` and `signature` are comparable by inequality (and thus by 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. In all other cases the types are not comparable. ### Type constraints Polymorphic types are not declared as comparable by default. If the user 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 done if the type declaration is separated from the function definition. The constraints have to be prepended to the type declaration and separated with a semicolon: ``` function eq(x : 'a, y : 'a) = x == y // Type error, 'a is not comparable 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 ``` Currently only two constraints are allowed: `eq` for equality and `ord` for inequality. Declaring a type as `ord` automatically implies `eq`. ````

zxq9 commented

2022-06-18 20:19:45 +09:00

(Migrated from gitlab.com)

Created by: radrow

After some thinking I think comparing addresses makes sense. It can be useful if you keep a list of addresses and want to ensure the order by sorting it

*Created by: radrow* After some thinking I think comparing addresses makes sense. It can be useful if you keep a list of addresses and want to ensure the order by sorting it

zxq9 commented

2022-06-18 20:21:11 +09:00

(Migrated from gitlab.com)

Created by: radrow

Please add versions of insert_by and sort (and possibly others) that instead of taking a comparison lambda, rely on the constraints

*Created by: radrow* Please add versions of `insert_by` and `sort` (and possibly others) that instead of taking a comparison lambda, rely on the constraints

zxq9 commented

2022-06-18 20:36:09 +09:00

(Migrated from gitlab.com)

Created by: radrow

Review: Commented

Update fold in aeso_syntax_utils

*Created by: radrow* **Review:** Commented Update fold in aeso_syntax_utils

zxq9 commented

2022-06-18 23:34:17 +09:00

(Migrated from gitlab.com)

Created by: radrow

Remember that you actually can reuse the existing definitions by just applying them with a lambda

*Created by: radrow* Remember that you actually can reuse the existing definitions by just applying them with a lambda

ghallak commented

2022-06-20 00:18:33 +09:00

(Migrated from gitlab.com)

Done here ea98fc97bb

Done here ea98fc97bbe2f8860850c1d812dd11b4b3ff8aa4

ghallak commented

2022-06-20 00:19:36 +09:00

(Migrated from gitlab.com)

Done here 9d296f04cb

Done here 9d296f04cb23d387fc0d6e3c47962ef166800591

ghallak commented

2022-06-20 00:21:40 +09:00

(Migrated from gitlab.com)

There is no such table as I didn't find a use for it, if all ids are comparable by equality, what should go in that table?

There is no such table as I didn't find a use for it, if all `id`s are comparable by equality, what should go in that table?

zxq9 commented

2022-06-20 01:11:34 +09:00

(Migrated from gitlab.com)

Created by: radrow

I don't get why there is a need for a table for ord but not for eq. Would you explain why one is needed and the other is not?

*Created by: radrow* I don't get why there is a need for a table for `ord` but not for `eq`. Would you explain why one is needed and the other is not?

ghallak commented

2022-06-20 01:53:38 +09:00

(Migrated from gitlab.com)

Since all types of the form {id, _, Id} are compared by eq, there is no need to store all of them in a table, but not all types of the above form are compared by ord so I only need to store that.

So checking if {id, _, "int"} is comparable by ord will only succeed because "int" is in the table ord_constraint_types, but checking if any other type of the form {id, _, Id} is comparable by eq will always succeed.

Since all types of the form `{id, _, Id}` are compared by `eq`, there is no need to store all of them in a table, but not all types of the above form are compared by `ord` so I only need to store that. So checking if `{id, _, "int"}` is comparable by `ord` will only succeed because `"int"` is in the table `ord_constraint_types`, but checking if any other type of the form `{id, _, Id}` is comparable by `eq` will always succeed.

ghallak commented

2022-06-20 01:55:21 +09:00

(Migrated from gitlab.com)

Done here fc2875965e

Done here fc2875965e302c75a1c02e9655beeb0c524aecee

ghallak commented

2022-06-20 01:55:45 +09:00

(Migrated from gitlab.com)

Will have to modify the tests for that.

ghallak commented

2022-06-20 01:56:14 +09:00

(Migrated from gitlab.com)