nac3-spec/README.md

# NAC3 Specification

Specification and discussions about language design.

A toy implementation is in [`toy-impl`](./toy-impl), requires python 3.9.


## Referencing Host Variables from Kernel
Host variable to be accessed must be declared as `global` in the kernel
function.  This is to simplify and speed-up implementation, and also warn the
user about the variable being global. (prevent calling the interpreter many
times during compilation if there are many references to host variables)

Kernel cannot modify host variables, this would be checked by the compiler.
Value that can be observed by the kernel would be frozen once the kernel has
been compiled, subsequence modification within the host would not affect the
kernel.

Only types supported in the kernel can be referenced.

## Class and Functions
* Instance variables must be annotated: (Issue #1)
    ```python
    class Foo:
        a: int
        b: int
        def __init__(self, a: int, b: int):
            self.a = a
            self.b = b
    ```
* Three types of instance variables: (Issue #5)
  * Host only variables: Do not add type annotation for it in the class.
  * Kernel Invariants: Immutable in the kernel and in the host while the kernel
    is executing. Type: `KernelInvariant(T)`. The types must be immutable.
    (use tuple instead of list in the host, but the type annotation should still
    be list?)
  * Normal Variables: The host can only assign to them in the `__init__`
    function. Not accessible afterwards.
* Functions require full type signature, including type annotation to every
  parameter and return type.
  ```python
  def add(a: int, b: int) -> int:
    return a + b
  ```
* RPCs: optional parameter type signature, require return type signature.
* Function default parameters must be immutable.
* Function pointers are supported,  and lambda expression is not supported
  currently. (maybe support lambda after implementing type inference?)

## Built-in Types
* Primitive types include:
    * `bool`
    * `byte`
    * `int32`
    * `int64`
    * `uint32`
    * `uint64`
    * `float`
    * `str`
    * `bytes`
* Collections include:
    * `list`: homogeneous (elements must be of the same type) fixed-size (no
      append) list.
    * `tuple`: inhomogeneous immutable list, only pattern
      matching (e.g. `a, b, c = (1, True, 1.2)`) and constant indexing is
      supported:
      ```
      t = (1, True)
      # OK
      a, b = t
      # OK
      a = t[0]
      # Not OK
      i = 0
      a = t[i]
      ```
    * `range` (over numerical types)

### Numerical Types
* All binary operations expect the values to have the same type.
* Casting can be done by `T(v)` where `T` is the target type, and `v` is the
  original value. Examples: `int64(123)`
* Integers are treated as `int32` by default. Floating point numbers are double
  by default.
* No implicit coercion, require implicit cast.
  For integers that don't fit in int32, users should cast them to `int64`
  explicitly, i.e. `int64(2147483648)`.  If the compiler found that the integer
  does not fit into int32, it would raise an error. (Issue #2)
* Only `uint32`, `int32` (and range of them) can be used as index.

## Generics
We use [type variable](https://docs.python.org/3/library/typing.html#typing.TypeVar) for denoting generics.

Example:
```python
from typing import TypeVar
T = TypeVar('T')

class Foo(EnvExperiment):
    @kernel
    # type of a is the same as type of b
    def run(self, a: T, b: T) -> bool:
        return a == b
```

* Type variable can be limited to a fixed set of types.
* Type variables are invariant, same as the default in Python. We disallow
  covariant or contravariant. The compiler should mark as error if it encounters
  a type variable used in kernel that is declared covariant or contravariant.
* Code region protected by a type check, such as `if type(x) == int:`, would
  treat `x` as `int`, similar to how [typescript type guard](https://www.typescripttutorial.net/typescript-tutorial/typescript-type-guards/) works.
  ```python
  def add1(x: Union[int, bool]) -> int:
    if type(x) == int:
        # x is int
        return x + 1
    else:
        # x must be bool
        return 2 if x else 1
  ```
* Generics are instantiated at compile time, all the type checks like
  `type(x) == int` would be evaluated as constants. Type checks are not allowed
  in area outside generics.
* Type variable cannot occur alone in the result type, i.e. must be bound to the
  input parameters.

Questions:
* Should we support things like optional type? (like the one in rust)
* Would it be better to assert on the type variable directly instead of
  `type(x)` for type guards?

## Lifetime
Probably need more discussions...