The language

Values and types

Every value in Brine has one static type, known at compile time, and Brine never converts between types for you: an int times a float is an error until you write float(n). Values are values: assigning or passing one makes a copy (a cheap one), so changing a copy never changes the original.

The types

struct Point:
    x: int
    y: int

fn main():
    let n = 42                       # int (64-bit signed)
    let small: u8 = 200              # the literal adapts to u8
    let ratio = 0.75                 # float (64-bit)
    let ok = true                    # bool
    let name = "brine"               # str (UTF-8)
    let xs = [1, 2, 3]               # [int]
    let ages = {"ann": 31, "bob": 27}  # {str: int}
    let pair = (1, "one")            # (int, str)
    let p = Point(x=1, y=2)          # a struct
    print(n, small, ratio, ok, name)
    print(xs, ages, pair, p)
    print(pair.0, pair.1, p.x)

42 200 0.75 true brine
[1, 2, 3] {"ann": 31, "bob": 27} (1, "one") Point(x=1, y=2)
1 one 1

Type	What it is	Literals
`int`	64-bit signed integer (the same type as `i64`)	`42`, `-7`, `1_000_000`, `0xff`
`i8` `i16` `i32` `i64` `i128`	signed integers of that many bits	any integer literal that fits
`u8` `u16` `u32` `u64` `u128`	unsigned integers	any integer literal that fits
`float`	64-bit IEEE float (the same type as `f64`)	`3.14`, `1e-9`, `2.5e3`
`f32`	32-bit IEEE float	any number literal, in an `f32` context
`bool`	`true` or `false`	`true`, `false`
`str`	immutable UTF-8 text	`"hi\n"`, `f"x = {x}"`
`[T]`	array of `T`	`[1, 2, 3]`, `[0.0] * n`, `[i * i for i in 0..n]`
`{K: V}`	map from `K` to `V`, in insertion order	`{"ann": 31}`
`(A, B, ...)`	tuple	`(1, "one")`; fields are `t.0`, `t.1`
structs	your own record types	`Point(x=1, y=2)` or `Point(1, 2)`
enums	tagged unions, including `Option[T]` and `Result[T, E]`	`Shape.Circle(1.0)`, `Some(3)`, `Ok(x)`

Arrays, strings and maps have their own pages: arrays, strings and maps. Structs and enums are covered in structs and enums and match.

Tuples are indexed with a number after a dot (pair.0), not with brackets, and you can unpack them: let (n, s) = pair (see bindings).

Literals

fn main():
    print(1_000_000, 0xff, 0o17, 0b1010)
    print(3.14, 1e-9, 2.5e3, 1.0)
    let b: u8 = 0b1111_0000
    let f: f32 = 1
    let big: i128 = 10_000_000_000_000_000_000_000
    let max: u128 = 340282366920938463463374607431768211455
    print(b, f, big, max)
    print("tab\there", "quote: \"", "brace: \{", "\u{e9}")

1000000 255 15 10
3.14 1e-09 2500.0 1.0
240 1.0 10000000000000000000000 340282366920938463463374607431768211455
tab  here quote: " brace: { é

Integers may use _ separators anywhere between digits, and the prefixes 0x (hex), 0o (octal) and 0b (binary).
A number with a . or an exponent is a float: 1.0, 1e-9.
String escapes: \n \t \r \0 \\ \" \' \{ \} and \u{XXXX}. The braces need escaping because any string can become an f-string; see strings.

Literals adapt to context

A literal has no fixed type of its own. It takes the type the context expects, so let b: u8 = 200 is a u8 and let f: f32 = 1 is an f32 (an integer literal can become a float). With no context, an integer literal is an int and a float literal is a float.

The compiler checks that the literal fits:

fn main():
    let b: u8 = 300
    print(b)

error[E0315]: literal `300` is out of range for `u8`
 --> main.br:2:17
  |
2 |     let b: u8 = 300
  |                 ^^^ `u8` holds 0..=255
  = run `brine explain E0315` for more about this error
error: could not compile due to 1 error

Integer literals go up to u128’s maximum, 2^128 - 1. A literal above i128’s maximum fits only in a u128.

No implicit conversions

Brine never converts a value to another type on its own, not even i32 to int or int to float. Mixing types is a compile error that tells you what to write:

fn main():
    let count = 3
    let price = 2.5
    print(count * price)

error[E0305]: cannot multiply `int` and `float`
 --> main.br:4:11
  |
4 |     print(count * price)
  |           ^^^^^^^^^^^^^ `*` with mismatched operands
  |
  = help: brine never converts numbers implicitly; use `float(x)` or `int(x)`
  = run `brine explain E0305` for more about this error
error: could not compile due to 1 error

The same goes for two integer types:

fn main():
    let small: i32 = 5
    let n: int = small
    print(n)

error[E0301]: mismatched types
 --> main.br:3:18
  |
3 |     let n: int = small
  |                  ^^^^^ expected `int`, found `i32`
  |
  = help: convert explicitly with `int(...)` (checked at runtime)
  = run `brine explain E0301` for more about this error
error: could not compile due to 1 error

Why so strict: implicit conversions are where precision is lost and signs flip without anyone noticing. In Brine every conversion is visible in the code, and every narrowing one is checked.

Explicit conversions

Convert by calling the type’s name like a function:

fn main():
    let i = 7
    let x = 2.9
    print(float(i) / 2.0)         # int to float
    print(int(x), int(-x))        # float to int: truncates toward zero
    let small: i32 = i32(i)       # checked: panics if out of range
    print(small, int(small))
    print(str(i) + "!", str(x))   # anything printable to str
    print(int("42") + 1, float("2.5") * 2.0)  # parse text

Conversion	Behavior
`float(n)`, `f32(n)`	integer to float
`int(x)`, `i32(x)`, …	float to integer, truncating toward zero; panics if the value is out of range or NaN
`i32(n)`, `u8(n)`, `int(n)`, …	integer to integer; panics if the value doesn’t fit
`str(v)`	any printable value to its text, as `print` shows it
`int(s)`, `float(s)`	parse a `str`; panics on bad input, so check text from outside first (`s.is_digit()`)

Panics: overflow, division by zero, bounds

Integer overflow, an out-of-range conversion, division (or %) by zero and an out-of-bounds index all stop the program with a clear message and exit code 101. This is a panic.

fn main():
    var level: u8 = 250
    for _ in 0..10:
        level += 1
    print(level)

panic: integer overflow in addition
  --> overflow.br:4:9

fn main():
    let xs = [10, 20, 30]
    let i = len(args()) + 3     # 3 when the program gets no arguments
    print(xs[i])

panic: index 3 is out of bounds for an array of length 3
  --> bounds.br:4:11

These checks are always on, in every build, and there is no flag to turn them off. Instead, the compiler removes each check it can prove can never fail. In for i in 0..len(xs): total += xs[i] the index is always in range, so that bounds check is gone from the program. brine check --report lists the checks that remain, and contracts let you give the prover the facts it needs to remove more.

Floats don’t panic: they follow IEEE rules, so 1.0 / 0.0 is inf and 0.0 / 0.0 is nan.

Integer division and remainder

Integer / rounds down, toward negative infinity, like Python’s //. % takes the sign of the right-hand side, so a == (a / b) * b + a % b always holds.

fn main():
    print(7 / 2, 7 % 2)
    print(-7 / 2, -7 % 2)
    print(7 / -2, 7 % -2)
    print(float(7) / float(2))

3 1
-4 1
-4 -1
3.5

For a fractional result, convert first: float(a) / float(b). There is no // and no **; use / and pow(x, y). Bitwise operators work on integers: &, |, ^, ~, << and >>.

Value semantics

Assigning a value or passing it to a function makes a copy. Changing the copy never changes the original, for every type: numbers, arrays, strings, maps, tuples, structs and enums.

struct Point:
    x: int
    y: int

fn main():
    let a = [1, 2, 3]
    var b = a            # a copy (cheap: shared until one side changes)
    b.push(4)
    b[0] = 100
    print(a, b)

    let p = Point(x=1, y=2)
    var q = p
    q.x = 10
    print(p, q)

[1, 2, 3] [100, 2, 3, 4]
Point(x=1, y=2) Point(x=10, y=2)

Copies are cheap. Arrays, strings and maps are reference counted and copy-on-write: var b = a shares the data, and only the first change to b copies it. A function that only reads its argument never copies it.

When you want a function to change the caller’s variable, say so with ref, at both ends (see functions). Because nothing is shared behind your back, there is no aliasing to reason about, and par can run code in parallel without data races.

i128 and u128

i128 and u128 work like the other integer types, with two caveats:

They need a 64-bit target (they’re a GCC/Clang feature in the generated code).
The prover can’t remove their overflow checks, so those checks always run.

fn main():
    let big: i128 = 170141183460469231731687303715884105727
    let huge: u128 = 2 * u128(big) + 1
    print(big, huge)
    let wide = i128(9_223_372_036_854_775_807) * 4
    print(wide)

170141183460469231731687303715884105727 340282366920938463463374607431768211455
36893488147419103228

Summary

Types: int (= i64), i8..i128, u8..u128, float (= f64), f32, bool, str, [T], {K: V}, tuples, structs and enums.
Literals adapt to the expected type and must fit in it.
No implicit conversions. Convert with float(n), int(x), i32(n), str(v), int(s); narrowing ones are checked.
Overflow, division by zero, bad conversions and bad indexes panic, unless the compiler proved they can’t happen.
Integer / rounds down; % has the sign of the right side.
Everything is a value. Copies are cheap; ref shares on purpose.