Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add comparable typevar constraints #390

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open

Add comparable typevar constraints #390

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
3f177d3
Add constraints to the syntax and parser
ghallak Jun 11, 2022
f56eeb0
Use id() for constraints instead of keywords
ghallak Jun 11, 2022
6971303
Add constraints to typechecker, fix old tests, add new ones
ghallak Jun 13, 2022
6c17e57
Fix dialyzer warnings
ghallak Jun 14, 2022
fc08fe0
Add tests for calling constrained functions
ghallak Jun 14, 2022
2d17ce3
Add test for unknown tvar constraints
ghallak Jun 14, 2022
8e6c6d8
Add char type to the docs
ghallak Jun 14, 2022
75f2711
Update CHANGELOG
ghallak Jun 14, 2022
46ac9bf
Update the docs
ghallak Jun 14, 2022
ea98fc9
Add an example of address type to the docs
ghallak Jun 19, 2022
9d296f0
Formatting fix
ghallak Jun 19, 2022
fc28759
Make address comparable by inequality
ghallak Jun 19, 2022
4562a71
Fix the tests after changing address to ord
ghallak Jun 19, 2022
e8da0a7
Update docs/sophia_features.md
ghallak Jun 19, 2022
21cc6f2
Add constrained_t to fold
ghallak Jun 20, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
function sum(l : list(int)) : int = foldl((+), 0, l)
function logical_and(x, y) = (&&)(x, y)
```
- Add comparable typevar constraints (`ord` and `eq`)
```
lt : 'a is ord ; ('a, 'a) => bool
lt(x, y) = x < y

is_eq : 'a is eq ; ('a, 'a) => bool
is_eq(x, y) = x == y
```
### Changed
- Error messages have been restructured (less newlines) to provide more unified errors. Also `pp_oneline/1` has been added.
- Ban empty record definitions (e.g. `record r = {}` would give an error).
Expand Down
98 changes: 76 additions & 22 deletions docs/sophia_features.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -354,28 +354,29 @@ namespace C =
## Types
Sophia has the following types:

| Type | Description | Example |
|----------------------|---------------------------------------------------------------------------------------------|--------------------------------------------------------------|
| int | A 2-complement integer | ```-1``` |
| address | æternity address, 32 bytes | ```Call.origin``` |
| bool | A Boolean | ```true``` |
| bits | A bit field | ```Bits.none``` |
| bytes(n) | A byte array with `n` bytes | ```#fedcba9876543210``` |
| string | An array of bytes | ```"Foo"``` |
| list | A homogeneous immutable singly linked list. | ```[1, 2, 3]``` |
| ('a, 'b) => 'c | A function. Parentheses can be skipped if there is only one argument | ```(x : int, y : int) => x + y``` |
| tuple | An ordered heterogeneous array | ```(42, "Foo", true)``` |
| record | An immutable key value store with fixed key names and typed values | ``` record balance = { owner: address, value: int } ``` |
| map | An immutable key value store with dynamic mapping of keys of one type to values of one type | ```type accounts = map(string, address)``` |
| option('a) | An optional value either None or Some('a) | ```Some(42)``` |
| state | A user defined type holding the contract state | ```record state = { owner: address, magic_key: bytes(4) }``` |
| event | An append only list of blockchain events (or log entries) | ```datatype event = EventX(indexed int, string)``` |
| hash | A 32-byte hash - equivalent to `bytes(32)` | |
| signature | A signature - equivalent to `bytes(64)` | |
| Chain.ttl | Time-to-live (fixed height or relative to current block) | ```FixedTTL(1050)``` ```RelativeTTL(50)``` |
| oracle('a, 'b) | And oracle answering questions of type 'a with answers of type 'b | ```Oracle.register(acct, qfee, ttl)``` |
| oracle_query('a, 'b) | A specific oracle query | ```Oracle.query(o, q, qfee, qttl, rttl)``` |
| contract | A user defined, typed, contract address | ```function call_remote(r : RemoteContract) = r.fun()``` |
| Type | Description | Example |
|----------------------|---------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------|
| int | A 2-complement integer | ```-1``` |
| char | A single character | ```'c'``` |
| address | æternity address, 32 bytes | ```Call.origin``` ```ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt``` |
| bool | A Boolean | ```true``` |
| bits | A bit field | ```Bits.none``` |
| bytes(n) | A byte array with `n` bytes | ```#fedcba9876543210``` |
| string | An array of bytes | ```"Foo"``` |
| list | A homogeneous immutable singly linked list. | ```[1, 2, 3]``` |
| ('a, 'b) => 'c | A function. Parentheses can be skipped if there is only one argument | ```(x : int, y : int) => x + y``` |
| tuple | An ordered heterogeneous array | ```(42, "Foo", true)``` |
| record | An immutable key value store with fixed key names and typed values | ``` record balance = { owner: address, value: int } ``` |
| map | An immutable key value store with dynamic mapping of keys of one type to values of one type | ```type accounts = map(string, address)``` |
| option('a) | An optional value either None or Some('a) | ```Some(42)``` |
| state | A user defined type holding the contract state | ```record state = { owner: address, magic_key: bytes(4) }``` |
| event | An append only list of blockchain events (or log entries) | ```datatype event = EventX(indexed int, string)``` |
| hash | A 32-byte hash - equivalent to `bytes(32)` | |
| signature | A signature - equivalent to `bytes(64)` | |
| Chain.ttl | Time-to-live (fixed height or relative to current block) | ```FixedTTL(1050)``` ```RelativeTTL(50)``` |
| oracle('a, 'b) | And oracle answering questions of type 'a with answers of type 'b | ```Oracle.register(acct, qfee, ttl)``` |
| oracle_query('a, 'b) | A specific oracle query | ```Oracle.query(o, q, qfee, qttl, rttl)``` |
| contract | A user defined, typed, contract address | ```function call_remote(r : RemoteContract) = r.fun()``` |

## Literals
| Type | Constant/Literal example(s) |
Expand Down Expand Up @@ -501,6 +502,59 @@ function

Guards cannot be stateful even when used inside a stateful function.

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

## Lists

A Sophia list is a dynamically sized, homogenous, immutable, singly
Expand Down
8 changes: 5 additions & 3 deletions priv/stdlib/List.aes
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,11 @@ namespace List =
[] => abort("drop_last_unsafe: list empty")


function contains(e : 'a, l : list('a)) = switch(l)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

[] => false
h::t => h == e || contains(e, t)
function
contains : 'a is eq; ('a, list('a)) => bool
contains(e, l) = switch(l)
[] => false
h::t => h == e || contains(e, t)

/** Finds first element of `l` fulfilling predicate `p` as `Some` or `None`
* if no such element exists.
Expand Down
4 changes: 3 additions & 1 deletion priv/stdlib/Option.aes
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,9 @@ namespace Option =
None => abort(err)
Some(x) => x

function contains(e : 'a, o : option('a)) = o == Some(e)
function
contains : 'a is eq; ('a, option('a)) => bool
contains(e, o) = o == Some(e)

function on_elem(o : option('a), f : 'a => unit) : unit = match((), f, o)

Expand Down
5 changes: 3 additions & 2 deletions priv/stdlib/String.aes
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,7 @@ namespace String =
Some(ix)

private function
is_prefix : (list(char), list(char)) => option(list(char))
is_prefix([], ys) = Some(ys)
is_prefix(_, []) = None
is_prefix(x :: xs, y :: ys) =
Expand All @@ -98,10 +99,10 @@ namespace String =

private function
to_int_([], _, x, _) = Some(x)
to_int_(i :: is, value, x, b) =
to_int_(i :: ints, value, x, b) =
switch(value(i))
None => None
Some(n) => to_int_(is, value, x * b + n, b)
Some(i) => to_int_(ints, value, x * b + i, b)

private function ch_to_int_10(ch) =
let c = Char.to_int(ch)
Expand Down
Loading