Values and types

Numbers state their width. Text is UTF-8 bytes. A type can carry the rule that makes a value valid, and the compiler checks the rule where it can.

Numbers

Every number type states its width: Int8, Int16, Int32, Int64, the unsigned pairs, Float32 and Float64. There is no unsized Int, because its width would then depend on the machine.

A conversion is written. Int64(x) widens, and nothing widens on its own.

site/guide/numbers.vyrnBuilt

// Every number type states its width. There is no unsized `Int`.
import { joinWith } from "std/strings"

export fn demo() -> String {
    let small: Int8 = 100
    let count: Int64 = 9007199254740993
    let ratio: Float64 = 0.1 + 0.2
    let flag = 7 > 3

    // A conversion is written, never implied.
    let widened = Int64(small) + 1

    return joinWith([
        "small  \{small}",
        "widened \{widened}",
        "count  \{count}",
        "ratio  \{ratio}",
        "flag   \{flag}",
    ], "\n")
}

fn main() -> Int64 {
    print(demo())
    return 0
}

// Every number type states its width. There is no unsized `Int`.
import { joinWith } from "std/strings"

export fn demo() -> String {
    let small: Int8 = 100
    let count: Int64 = 9007199254740993
    let ratio: Float64 = 0.1 + 0.2
    let flag = 7 > 3

    // A conversion is written, never implied.
    let widened = Int64(small) + 1

    return joinWith([
        "small  \{small}",
        "widened \{widened}",
        "count  \{count}",
        "ratio  \{ratio}",
        "flag   \{flag}",
    ], "\n")
}

fn main() -> Int64 {
    print(demo())
    return 0
}

small 100 widened 101 count 9007199254740993 ratio 0.300000 flag true

Text

A String is UTF-8 bytes. byteLength is a field and counts bytes; charCount() walks the string and counts characters. The two agree on ASCII and disagree everywhere else, and the names say which one you asked for.

std/strings has the rest: split, join, trim, case, search, pad.

site/guide/text.vyrnBuilt

// A String is UTF-8 bytes. `byteLength` counts bytes, `charCount()` counts
// characters, and the two differ the moment the text leaves ASCII.
import { joinWith, toUpper, split } from "std/strings"

export fn demo() -> String {
    let name = "Ada"
    let mixed = "naïve"
    let parts = split("a,b,c", ",")
    let rejoined = joinWith(parts, " + ")

    return joinWith([
        "upper     \{toUpper(name)}",
        "bytes     \{mixed.byteLength}",
        "chars     \{mixed.charCount()}",
        "parts     \{parts.length}",
        "rejoined  \{rejoined}",
    ], "\n")
}

fn main() -> Int64 {
    print(demo())
    return 0
}

// A String is UTF-8 bytes. `byteLength` counts bytes, `charCount()` counts
// characters, and the two differ the moment the text leaves ASCII.
import { joinWith, toUpper, split } from "std/strings"

export fn demo() -> String {
    let name = "Ada"
    let mixed = "naïve"
    let parts = split("a,b,c", ",")
    let rejoined = joinWith(parts, " + ")

    return joinWith([
        "upper     \{toUpper(name)}",
        "bytes     \{mixed.byteLength}",
        "chars     \{mixed.charCount()}",
        "parts     \{parts.length}",
        "rejoined  \{rejoined}",
    ], "\n")
}

fn main() -> Int64 {
    print(demo())
    return 0
}

upper ADA bytes 6 chars 5 parts 3 rejoined a + b + c

Validated types

A where clause is part of the type. Age(30) is proven while the file compiles, so no check is emitted. Age(5) is refused by the compiler, in the same way a type error is refused.

Input from outside the program is not a constant, so it gets the total form. Age?(n) answers Option<Age>: Some when the rule holds, None when it does not. Nothing traps, and you cannot forget a check you never wrote.

The rule is readable by the compiler as well as by you. Chapter 9 turns the same declaration into a JSON Schema document.

site/guide/validated.vyrnBuilt

// A `where` clause is part of the type. The compiler proves a constant or
// refuses it, and `Age?(n)` is the total form for input nobody controls.
import { joinWith } from "std/strings"

type Age = Int64 where value >= 18

fn admit(n: Int64) -> String {
    return match Age?(n) {
        Some(a) => "admitted at \{a}",
        None => "refused at \{n}",
    }
}

export fn demo() -> String {
    let ok = Age(30) // proven while it compiles, so no check is emitted
    // let bad = Age(5) // the compiler refuses this line
    return joinWith(["ok \{ok}", admit(25), admit(5)], "\n")
}

fn main() -> Int64 {
    print(demo())
    return 0
}

// A `where` clause is part of the type. The compiler proves a constant or
// refuses it, and `Age?(n)` is the total form for input nobody controls.
import { joinWith } from "std/strings"

type Age = Int64 where value >= 18

fn admit(n: Int64) -> String {
    return match Age?(n) {
        Some(a) => "admitted at \{a}",
        None => "refused at \{n}",
    }
}

export fn demo() -> String {
    let ok = Age(30) // proven while it compiles, so no check is emitted
    // let bad = Age(5) // the compiler refuses this line
    return joinWith(["ok \{ok}", admit(25), admit(5)], "\n")
}

fn main() -> Int64 {
    print(demo())
    return 0
}

ok 30 admitted at 25 refused at 5