NEXORA, as it works today

Introduction

A program is one .nex file. It starts running at the function main. print writes a value followed by a line break.

fn main() -> Void {
    print("Hello from NEXORA")
}

Hello from NEXORA

Before running anything, NEXORA checks the whole program: names, types and whether every function returns what it promises. A program with an error is never started.

Syntax

• A statement ends at the end of its line. There are no semicolons.
• Blocks are written with braces. Indentation is free.
• A comment starts with // and runs to the end of the line.
• let declares a variable. Variables never change: there is no reassignment.
• A name can only be declared once while it is visible. There is no shadowing.
• Text is written between double quotes, on one line.

// Variables declared with let never change. The ones that do are declared with var.
fn main() -> Void {
    let name = "Ada"
    let year = 1843
    print(name)
    print(year)
    {
        // A block has its own variables, and can read the ones around it.
        let next = year + 1
        print(next)
    }
}

Ada
1843
1844

Types

The type of a variable is inferred from its value, or written after a colon. All types are known before the program runs, so a type error can never appear while it is running.

Nothing is converted implicitly. An Int and a Float are never mixed, and a number is never joined to a text. Conversions are explicit calls: to_float, to_int and to_text.

fn main() -> Void {
    let units: Int = 3
    let price = 2.5
    let total = to_float(units) * price
    print("Total: " + to_text(total))
    print(to_int(total))
}

Total: 7.5
7

Operators

Multiplication and division come before addition and subtraction, then comparisons, then and, then or. Dividing two Int gives an Int: the fractional part is dropped. Comparisons cannot be chained.

fn main() -> Void {
    print(2 + 3 * 4)
    print(7 / 2)
    print(7.0 / 2.0)
    print(3 > 2 and not (1 == 2))
}

14
3
3.5
true

Functions

Every parameter states its type, and the return type is always written. A function that returns a value must end with return on every path. if and else choose between blocks; the condition must be a Bool. A function may call itself; to repeat something many times, a loop needs no stack.

fn factorial(n: Int) -> Int {
    if n <= 1 {
        return 1
    }
    return n * factorial(n - 1)
}

fn describe(n: Int) -> Text {
    if n < 0 {
        return "negative"
    } else if n == 0 {
        return "zero"
    } else {
        return "positive"
    }
}

fn main() -> Void {
    print(factorial(10))
    print(describe(-4))
}

3628800
negative

Contracts

A function can state what it expects from its caller (requires) and what it promises (ensures, where result is the value returned). The clauses go at the start of the body. They are checked while the program runs, on every call: they are not proven in advance.

After a comma, a rule can carry its explanation. It does not change what is checked: when the rule is broken, the error shows it as the reason, so whoever broke it does not have to guess why it exists.

fn divide(a: Float, b: Float) -> Float {
    requires b != 0.0, "Dividing by zero has no result"
    return a / b
}

fn absolute(value: Int) -> Int {
    ensures result >= 0
    if value < 0 {
        return -value
    }
    return value
}

fn main() -> Void {
    print(divide(9.0, 2.0))
    print(absolute(-42))
}

4.5
42

Refined types

A refined type is a built-in type plus a rule that all its values follow. Every value of the type satisfies the rule, everywhere in the program. A value can only get the type in two ways, and both are written in the code:

• A constant, such as 15 below: it is checked before the program runs.
• An explicit check, such as Cents(...): it happens while running, and stops the program if the value breaks the rule.

type Percent = Int where value >= 0 and value <= 100, "A percentage goes from 0 to 100"
type Cents = Int where value >= 0, "An amount of money cannot be negative"

fn apply_discount(price: Cents, percent: Percent) -> Cents {
    ensures result <= price, "A discount never raises the price"
    return Cents(price * (100 - percent) / 100)
}

fn main() -> Void {
    print(apply_discount(2000, 15))
}

1700

A Percent can be used wherever an Int is expected, but not the other way round. Arithmetic on refined values gives the base type. A constant that breaks the rule is found without running:

type Percent = Int where value >= 0 and value <= 100

fn main() -> Void {
    let discount: Percent = 150
    print(discount)
}

type error[E2017]: Value outside refined type
  line 4, column 29: 150 is not a valid Percent

Loops

A variable that has to change is declared with var; let never changes, and neither do parameters. A while loop repeats its body while its condition is true, and says at the start of its body why it is correct:

• decreases: a whole number that never goes below 0 and gets smaller on every turn. It is the reason the loop ends. Every loop has exactly one.
• invariant: a condition that holds before every check of the loop condition. As many as needed.

fn sum_to(n: Int) -> Int {
    requires n >= 0, "Only natural numbers"
    ensures result == n * (n + 1) / 2
    var total = 0
    var i = 0
    while i < n {
        invariant total == i * (i + 1) / 2, "total is the sum of the numbers already added"
        decreases n - i, "Each turn moves i one step closer to n"
        i = i + 1
        total = total + i
    }
    return total
}

fn main() -> Void {
    print(sum_to(10000))
}

50005000

Both are checked on every turn while the program runs. A loop never hangs: it ends, or it stops on the turn where its measure did not get smaller, and the error says which turn and which values the variables had. A loop without a measure is found before running:

fn main() -> Void {
    var count = 3
    while count > 0 {
        print(count)
        count = count - 1
    }
}

semantic error[E2021]: Missing loop measure
  line 3, column 5: This loop does not say why it ends

Lists

A list is written between brackets, and all its elements have the same type: List[Int], List[Text], or even List[List[Int]]. A list never changes. List.append and List.concat build a new list and leave the old one as it was. List.length, List.get and List.contains read it.

A for loop walks a list, one element per turn. It can declare invariants like a while, but it needs no decreases: it ends when the list does.

fn total(prices: List[Int]) -> Int {
    var sum = 0
    for price in prices {
        invariant sum >= 0, "Prices are never negative"
        sum = sum + price
    }
    return sum
}

fn main() -> Void {
    let prices = [120, 45, 300]
    let more = List.append(prices, 35)
    print(prices)
    print(more)
    print(List.length(more))
    print(List.get(more, 0))
    print(List.contains(more, 45))
    print(total(more))
}

[120, 45, 300]
[120, 45, 300, 35]
4
120
true
500

List.get declares which indexes it accepts, from 0 to the length minus one: any other index stops the program and says which rule was broken. An empty list says nothing about the type of its elements, so it needs one written:

fn main() -> Void {
    let empty = []
    print(empty)
}

type error[E2011]: Type mismatch
  line 2, column 17: Cannot infer the type of an empty list without an expected type

Records

A record is a type the program declares, with fields that never change: type Point = { x: Int, y: Int }. It is built by giving every field a value, by name: Point(x: 1, y: 2). The order of the fields does not matter, but each one is given once and all of them are required.

A field is read with a dot, p.x, and the fields can be chained: segment.to.x. A record never changes, so there is no way to assign to one of its fields.

Two records are different types even when they have the same fields: the identity of a record is the identity of its declaration. Two values of the same record are compared by value, field by field.

type Point = { x: Int, y: Int }
type Segment = { from: Point, to: Point }

fn main() -> Void {
    let origin = Point(x: 0, y: 0)
    let corner = Point(x: 3, y: 4)
    let segment = Segment(from: origin, to: corner)
    print(segment.to.x)
    print(segment)
    print(corner == Point(x: 3, y: 4))
}

3
Segment(from: Point(x: 0, y: 0), to: Point(x: 3, y: 4))
true

Input and files

A program can receive its arguments with args(), and read the standard input with input(), one line at a time. Both are allowed by default: they are what the program was given, not something it reaches out for.

Files are different. A program says what it needs with uses, and whoever runs it has to allow it: uses read "datos/entradas.txt" needs --allow-read=datos. The three have to be there at the same time, and the paths are checked where they really are, so a .. or a symbolic link cannot leave the folder that was allowed.

fn main() -> Void {
    let names = args()
    var total = 0
    for name in names {
        invariant total >= 0, "The count never goes down"
        total = total + Text.length(name)
    }
    print(total)
}

0

input() reads one line of the standard input, and stops the program when there is nothing left to read. In the playground there is no standard input, so a program that reads it stops with an error.

Texts

Some functions belong to a type and are called with its name: Text.length, Text.slice, Text.contains, Text.starts_with, Text.ends_with, and Int.parse and Float.parse to read a number written in a text. A character is a Unicode code point, and texts are ordered by code point with <, the same on any machine: "Z" < "a" is true.

The functions that may have no answer say when they have one, with a requires written in NEXORA. Text.slice("abc", 2, 9) does not quietly return "c", and Int.parse("12a") does not return 12: both stop the program and explain which rule was broken. Check first with Int.can_parse:

fn main() -> Void {
    let name = "Ada Lovelace"
    let length = Text.length(name)
    print(length)
    print(Text.slice(name, 0, 3))
    print(Text.contains(name, "Love"))
    print("Ada" < "ada")
    let written = "042"
    if Int.can_parse(written) {
        print(Int.parse(written) + 1)
    }
}

12
Ada
true
true
43

Diagnostics

When something is wrong, NEXORA says what kind of problem it is, where it is, and what was expected. Each problem has a stable code. This program has a type error, found without running it:

fn main() -> Void {
    let age: Int = "twenty"
    print(age)
}

type error[E2011]: Type mismatch
  line 2, column 20: Expected Int, found Text

In the playground, selecting a diagnostic shows its position in the editor.

Limitations

These do not exist yet. Using them is an error, not something the playground pretends to support:

• break and continue, and for over anything that is not a list, such as a range of numbers or a text.
• Writing xs[i], changing an element, or map, filter and sorting on lists.
• Any other compound type besides lists and records: no maps, no enums, no Option.
• Operations on text beyond the ones in Texts: no trim, upper case, split or replace.
• Reading input, files or the network: a program can only print.
• Modules: a program is a single file.
• Any integration with AI models.

Limits of the implementation:

• At most 1000 nested calls.
• Int is a 64-bit integer; going out of range stops the program.
• In the playground, a program is stopped after a time limit and if it prints too much.

The interpreter is a reference implementation: it has not been measured for speed, and NEXORA is not ready for production use.