# 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.

```vyrn
// 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
}
```

Built output:

```
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](https://vyrn-lang.github.io/docs/std/strings.html) has the rest: split, join, trim, case, search, pad.

```vyrn
// 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
}
```

Built output:

```
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](https://vyrn-lang.github.io/guide/generators.html#reflection) turns the same declaration into a JSON Schema document.

```vyrn
// 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
}
```

Built output:

```
ok 30
admitted at 25
refused at 5
```

---

From https://vyrn-lang.github.io/guide/values.html — generated by `site/export.vyrn` from the Vyrn repository.