# Types

> A comprehensive overview of the TypR type system.

This page provides a comprehensive overview of the TypR type system.

<!-- truncate -->

## Basic types

Typed R provides explicit basic (primitive) types:

| Type | Description | Example |
|------|-------------|---------|
| `int` | Integer numbers | `42` |
| `num` | Floating-point numbers | `3.14159` |
| `bool` | Boolean values | `true`, `false` |
| `char` | Character strings | `"Hello"` |
| `null` | Null value (`NULL`) | `null` |
| `na` | Missing value (R spelling: `NA`) | `na` |
| `Any` | Top type — accepts any value | (used in signatures) |
| `Empty` | Bottom type — no value satisfies it | (return type for side-effect functions) |
| `Self` | Refers to the type that implements an interface | (used in interface definitions) |

### Literal types

Literals can appear as **types** (singleton types), providing more precise type information than their base type:

```typr noplayground
let x: 3 = 3;          # x is exactly 3, not just int
let flag: true = true;  # flag is exactly true, not just bool
let name: "hello" = "hello";  # name is exactly "hello", not just char
```

---

## Composite types

### Records

Records combine named fields of different types. They are the primary way to model structured data:

```typr
type Point <- list { x: int, y: int };
type Config <- record { name: char, timeout: int };   # explicit synonym
```

Equivalent literal forms: `list{...}`, `record{...}`, `object{...}`, `:{...}`.

See [Records & Constructors](records.md) for construction, spread, and named embedding.

### Tuples

Tuples combine values of different types by position:

```typr
type Pair    <- tuple{int, char};   # explicit
type PairAlt <- Tuple[int, char];   # bracket notation
type Rest    <- Tuple[T..., U];     # variadic: T... captures a sequence of types
```

### Vectors

```typr
type Vector <- Vec[3, int];
let v <- c(1, 2, 3);
```

### Arrays

```typr
type Array <- [4, bool];
let a <- [true, false, false, true];
```

| Form | Example | Description |
|------|---------|-------------|
| `[T]` (S3 short) | `[int]` | array of integers, free size (`Any`) |
| `[#N, T]` (S3 full) | `[#N, int]` | size indexed by generic `#N` |
| `Array[N, T]` | `Array[3, int]` | named variant, fixed size = 3 |
| `Vec[T]` | `Vec[num]` | native R vector |
| `df[N]{...}` | `df[N]{ name: char, age: int }` | `df` = short alias for `dataframe` |
| `Tibble[N]{...}` | `Tibble[3]{ id: int, active: bool }` | requires a `typeconstructor` declaration |

### Dataframes

```typr
type PersonRows <- dataframe[3]{ name: char, age: int };
```

---

## Generic types

### Generics and kind sigils

```typr noplayground
let id <- fn(x: T): T { x };         # T uppercase = free generic
#N     # "index" generic (array dimension)
$T     # "label" generic (field name)
%R     # constrained: must be a Record
@I     # constrained: must be an Interface
^S     # constrained: must be a char
?B     # constrained: must be a bool
```

### Generic type definitions

```typr
type Option<T> <- .Some(T) | .None;
opaque Factor<L> <- int;             # phantom parameter: L appears only in signatures
```

---

## Function types

Functions are first-class values and have their own type syntax:

```typr
type Predicate <- (int, char) -> bool;   # anonymous function type
type Adder     <- (a: int, b: int) -> int;  # parameter names optional, ignored for typing
```

:::caution
Writing `fn(a: int) -> int` in **type position** (instead of `(int) -> int`) triggers `SyntaxError::FunctionTypeSyntax` — `fn(...)` only exists at the expression level, never in types.
:::

---

## Interfaces

```typr
type Viewable <- interface { view: (Self) -> char };   # structural capability
```

See [Interfaces & Structural Validation](interfaces.md) for details.

---

## Union types

```typr
type Shape <- .Circle(num) | .Square(num);
type Combined <- Movable & Drawable;          # intersection of interfaces
```

See [Unions, Tags & Pattern Matching](unions-patterns.md) for pattern matching.

---

## Type aliases

Type aliases give a name to an existing type:

```typr
type Person <- list {
    name: char,
    age: int
};
```

With an alias, `Person` and `list { name: char, age: int }` are interchangeable. See [Signatures](signatures.md) for `type` vs `opaque`.

---

## Refined types

A refined type is a base type narrowed by a property, written with `&`:

```typr noplayground
type Coordinates <- [num] & length(2);   # a vector of exactly two numbers
let origin: Coordinates <- [0.0, 0.0];
let n: int & (> 0) <- 3;                 # a strictly positive integer
```

| Property | Applies to | Meaning |
|---|---|---|
| `length(n)` | vectors | exactly `n` elements. `[int] & length(5)` is the same type as `[5, int]`. |
| `(> c)`, `(< c)` | `int`, `num` | every value is greater / less than the constant `c` |
| `(>= c)`, `(<= c)` | `int`, `num` | every value is at least / at most `c` |
| `length(> n)`, `length(>= n)`, `length(< n)`, `length(<= n)` | vectors | the number of elements lies in that range: `[int] & length(> 0)` is a non-empty vector |

Properties combine: `int & (> 0) & (< 10)`. Order and repetition do not matter, and a
combination that no value can satisfy is a compile error:

```typr compile_fail
let a: int & (> 10) & (< 5) <- 7;
```

Applying a property to a base that does not support it (`int & length(5)`, `chr & (> 0)`) is
also an error.

### Where the check happens

A refinement is proven at compile time whenever the compiler can, and checked once, at run time,
when it cannot. The check sits at the boundary, where a value enters a refined type: a `let`
annotation, a function argument, a return value.

```typr noplayground
let read_point <- fn(): [num] { [3.0, 4.0] };
let p: [num] & length(2) <- read_point();   # length unknown here: checked at run time
let q: [num] & length(2) <- [1.0, 2.0];     # proven by the literal: no check
```

The first `let` becomes a call to a small helper from the generated prelude:

```r
p <- typr_refine_length(read_point(), 2L, "TypR/main.ty:2")
```

If the length is wrong, R stops with
`Type refinement violation at TypR/main.ty:2: expected length 2, got 3`.
Inside the function, the refined parameter is trusted: nothing is re-checked.

### Narrowing by a condition

Inside an `if`, the condition is itself a proof. The compiler reads it and refines the variables
it mentions, in the `then` branch for the condition and in the `else` branch for its negation, so
no run-time check is needed there:

```typr noplayground
let first <- fn(v: [#N, T] & length(> 0)): T { v[1] };
let safe_first <- fn(v: [int]): int {
  if (length(v) > 0) { first(v) } else { 0 }
};
let sqrt_pos <- fn(x: num & (> 0)): num { x };
let clamp <- fn(x: num): num {
  if (x > 0) { sqrt_pos(x) } else { 0.0 }
};
```

In the `then` branches, `v` is known to be non-empty and `x` to be positive. Without the `if`, the call `first(v)` would check `length(v) > 0` at run time instead.

The compiler understands these conditions:

| Condition | Refines |
|---|---|
| `length(x) <op> n` | the length of the vector `x` |
| `x <op> c` | the scalar `x` (`int` or `num`) |
| `!cond` | swaps the two branches |
| `(a) && (b)`, `(a) & (b)` | both hold in the `then` branch |
| `(a) \|\| (b)` | both are false in the `else` branch |

where `<op>` is one of `>`, `<`, `>=`, `<=`, `==`. Anything else is ignored: the branch is still
valid, it just gets no extra information. The narrowing stays inside its branch and is gone after
the `if`. Parenthesize each side of `&&` and `||`.

### Generic bases

A refinement can sit on a generic base. The generics are unified as usual; the refinement is
decided against each argument at the call:

```typr noplayground
let first <- fn(v: [#N, T] & length(> 0)): T { v[1] };
let sized <- fn(v: [3, char]): char { first(v) };   # length 3 proves length > 0: no check
let unknown <- fn(v: [int]): int { first(v) };      # unproven: checked at run time
```

```typr compile_fail
let first <- fn(v: [#N, T] & length(> 0)): T { v[1] };
let empty <- fn(v: [0, char]): char { first(v) };   # length 0 can never be > 0
```

The same three outcomes apply as for concrete types: proven (no check), unproven (a run-time
check on the argument), refuted (no signature matches).

Operations that keep the property (`x + 1` on a `[5, int]`) keep the type. Functions the
compiler knows nothing about return their declared type, without the refinement.

---

## Type inference

Typed R features **type inference** — explicit annotations are not always required. The compiler infers types from:

- literal values
- expressions
- function bodies
- usage context

Explicit types can be added incrementally where clarity or safety is critical.

---

## Summary of type constructors

| Kind | Syntax | Example |
|------|--------|---------|
| Vector | `Vec[n, T]` | `c(1, 2, 3)` |
| Array | `[n, T]` | `[true, false, true]` |
| Record | `list { field: T, ... }` | `list(a = 3, b = false)` |
| Tuple | `tuple{T1, T2}` | `:{1, "hello"}` |
| Function | `(T1, T2) -> T3` | `fn(a: int): bool { true }` |
| Interface | `interface { f: (T) -> T, ... }` | no default constructor |
| Refined | `T & length(n)`, `T & (> c)` | `[num] & length(2)` |
| Union | `T1 \| T2` | no default constructor |
| Tagged | `.Tag(T) \| .Tag2` | `.Some(42)`, `.None` |
| Alias | `type Name = T` | `type Person = list { ... }` |