Separation between Felt, Binary, and Integer types
- Lingua principale
- Rust
- Stelle
- 96
- Fork
- 39
- Metriche di merge delle PR
- Nessuna PR unita negli ultimi 30g
Descrizione
Currently, as far as the user is concerned, there is only one base type in AirScript: field element (and we can have vectors and matrixes of field elements). However, it would be good to have a slightly more sophisticated type system. Specifically, I'm thinking of having 3 base types:
1. Field element - any value in our base field.
2. Binary value - a field element which is either $0$ or $1$.
3. Integer - which is a regular integer - maybe fixed to `u32` type.
## Binary value
Being able to determine if an element is a binary value is useful because some statements are only valid for binary values. Specifically:
- Selectors for `enf match` statement can involve only binary values.
- Logical operators `!`, `&`, and `|` can involve only binary values.
To specify that values in some column `x` can only be binary, we need to enforce the following constraint:
```
enf x^2 = x
```
It may be beneficial to add a "built-in evaluator" so that a user could do something like this:
```
enf is_binary(x)
```
Once we know that values are binary, any logical operators on them yield binary values. But if an expression involves a regular field element, the result would be a field element. For example, let's say we have columns `x`, `y`, and `z`:
```
enf is_binary(x)
enf is_binary(y)
let a = x & y # a is binary
let b = x | !y # b is binary
let c = x * z # c is a field element
let d = x + z # d is a field element
```
We should also probably introduce keywords `felt` and `binary` for function parameters and return types. For example, instead of:
```
fn foo(a: vector[2], b: scalar) -> vector[4]
```
We could do something like this:
```
fn foo(a: binary[2], b: felt) -> binary[4]
```
## Integers
Currently, there are a few places where we implicitly assume that values are integers. For example, in something like:
```
let x = sum([a^i for (a, i) in (xyz, 0..5)
```
`i` is an integer.
More generally, I'm thinking integers would be used for:
1. Iterable ranges.
2. Indexing into vectors/matrixes.
3. Exponents in exponentiation expressions.
If we limit the size of integers to `u32` we can coerce any integer into a field element. However, we can't convert a field element into an integer.
Guida per i contributori
Apri la guida per i contributori
Valutazione
Questa issue non è ancora stata valutata.