QPQ-AG/sophia
11
0
Fork 0
Code Issues 43 Pull Requests 7 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
+522 -42
ghallak commented 2022-06-14 23:23:45 +09:00 (Migrated from gitlab.com)
Copy Link
Copy Source

Fixes: #229

Fixes: #229
zxq9 commented 2022-06-18 19:07:11 +09:00 (Migrated from gitlab.com)
Copy Link
Copy Source

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)
Copy Link
Copy Source

Created by: radrow

formatting

*Created by: radrow* formatting
zxq9 commented 2022-06-18 19:35:15 +09:00 (Migrated from gitlab.com)
Copy Link
Copy Source

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)
Copy Link
Copy Source

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)
Copy Link
Copy Source

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)
Copy Link
Copy Source

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)
Copy Link
Copy Source

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)
Copy Link
Copy Source

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)
Copy Link
Copy Source

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)
Copy Link
Copy Source

Done here ea98fc97bb

Done here ea98fc97bbe2f8860850c1d812dd11b4b3ff8aa4
ghallak commented 2022-06-20 00:19:36 +09:00 (Migrated from gitlab.com)
Copy Link
Copy Source

Done here 9d296f04cb

Done here 9d296f04cb23d387fc0d6e3c47962ef166800591
ghallak commented 2022-06-20 00:21:40 +09:00 (Migrated from gitlab.com)
Copy Link
Copy Source

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)
Copy Link
Copy Source

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)
Copy Link
Copy Source

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)
Copy Link
Copy Source

Done here fc2875965e

Done here fc2875965e302c75a1c02e9655beeb0c524aecee
ghallak commented 2022-06-20 01:55:45 +09:00 (Migrated from gitlab.com)
Copy Link
Copy Source

Will have to modify the tests for that.

Will have to modify the tests for that.
ghallak commented 2022-06-20 01:56:14 +09:00 (Migrated from gitlab.com)
Copy Link
Copy Source

Check this commit that made address comparable by ord fc2875965e.

Check this commit that made `address` comparable by `ord` fc2875965e302c75a1c02e9655beeb0c524aecee.
ghallak commented 2022-06-20 02:08:26 +09:00 (Migrated from gitlab.com)
Copy Link
Copy Source

Fixed the tests here 4562a7166c

Fixed the tests here 4562a7166cfe7ddac65a940508a8266a0e7034f8
This pull request has changes conflicting with the target branch.
  • CHANGELOG.md
  • docs/sophia_features.md
  • src/aeso_ast_infer_types.erl
  • src/aeso_ast_to_fcode.erl
  • src/aeso_parser.erl
  • src/aeso_pretty.erl
  • src/aeso_scan.erl
  • src/aeso_syntax.erl
  • src/aeso_syntax_utils.erl
  • test/aeso_compiler_tests.erl
View command line instructions

Checkout

From your project repository, check out a new branch and test the changes.
git fetch -u origin ghallak/229:ghallak/229
git checkout ghallak/229
Sign in to join this conversation.
Reviewers
No Reviewers
Labels
Clear labels
WIP
bug
consensus-breaking
dependencies
documentation
duplicate
effort: high
effort: low
effort: medium
effort: trivial
enhancement
good first issue
help wanted
invalid
maintenance
question
task/feature
todo-in-rewrite
wontfix
bug
Something is not working
 duplicate
This issue or pull request already exists
 enhancement
New feature
 help wanted
Need some help
 invalid
Something is wrong
 pig lipstick
Muggle-facing enhancements
 question
More information is needed
 wontfix
This won't be fixed
No Label
Milestone
No items
No Milestone
Projects
Clear projects
No project
Assignees
Clear assignees
Dagadunn Pickmick dimitar.p.ivanov flambard (Markus Flambard) gchewy hans_sv pharpend spivee (Jarvis Carroll) thescientress (Cecille de Jesus) uwiger (Ulf Wiger) zxq9 (Craig Everett)
No Assignees
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: QPQ-AG/sophia#881
Delete Branch "ghallak/229"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?