# Type System

Types are optional. If a type is declared, assignments are checked at runtime.

## Declaring Types

```baba
// Type declaration (name Type)
myValue Int;

// Assignment must match declared type
myValue : 10;       // OK (Int)
// myValue : "x";   // Error: expected Int
```

## Runtime Type Inference

Without declarations, values carry runtime type tags used by pattern matching:
- Numbers are tagged as `Int` or `Float`; `Number` is a supertype accepted in validation where numeric values are allowed
- Strings as `String`, Booleans as `Bool`
- Lists and Tables have `List`/`Table` tags

## Runtime Type Validation Semantics

- Parameter validation happens at call time for parameters with annotations only.
- Return type validation happens after body evaluation when a return type is declared.
- Untyped parameters are accepted as-is and are not validated.


## Function Return Types

```baba
add : (x: Int, y: Int) -> Int -> x + y;
```

## Typed Locals with `with`

Locals in a header can be typed exactly like globals using a declaration followed by assignment.

```baba
sumNext : (x: Int, y: Int) -> Int ->
  with (nx Int; ny Int; nx : x + 1; ny : y + 1;) -> nx + ny;
```

## Numeric Type Lattice and Widening

The numeric types form a simple lattice:

```
Int ⊂ Float ⊂ Number
```

- When a parameter expects `Float`, an `Int` is accepted (widened) implicitly.
- When a parameter expects `Number`, either `Int` or `Float` are accepted.
- When a parameter expects `Int`, `Float` is rejected.
- Many `math.` functions return `Float` for predictability.

## Typed Functions

Typed functions annotate parameters and the return value. At runtime, arguments and returns are validated.

### Multi-Parameter Typed Functions

```baba
// Parameter types and return type
add : (x: Int, y: Int) -> Int -> x + y;

// Using typed functions
result1 : add 2 3;        // OK => 5
// result2 : add 2 "3";   // Runtime error: parameter type mismatch

// Multi-parameter function takes all arguments at once
multiply : (x: Float, y: Float) -> Float -> x * y;
result : multiply 2.0 3.0;  // 6.0
```

### Curried Typed Functions

Curried functions take one parameter at a time and return functions for partial application:

```baba
// Curried function with typed first parameter and function return type
mul : (x: Float) -> (Float -> Float) -> y -> x * y;
double : mul 2.0;          // Partial application: double : (Float -> Float)
result : double 3.5;       // 7.0

// Three-parameter curried function
add3 : (x: Int) -> (Int -> (Int -> Int)) -> y -> z -> x + y + z;
add5 : add3 5;             // add5 : (Int -> (Int -> Int))
add5and3 : add5 3;         // add5and3 : (Int -> Int)
result : add5and3 2;       // 10
```

### Function Type Syntax

Function types use the syntax `(ParamType -> ReturnType)`:

```baba
// Simple function type
transform : (x: Int) -> (Int -> Int) -> y -> x + y;

// Function that returns another function
makeAdder : (x: Int) -> (Int -> Int) -> y -> x + y;
add5 : makeAdder 5;           // add5 : (Int -> Int)
result : add5 3;              // 8
```
Heads up! Complex nested parameter types like (f: (Int -> Int)) aren't implemented. The first parameter must use simple types like Int, Float, String, or Bool.

### Mixed Typed/Untyped Functions

```baba
// Mixed typed/untyped parameters (untyped are not validated)
concatIf : (flag: Bool, x, y) -> String ->
  when flag is
    true then x .. y
    _    then y .. x;

// Return type enforcement
// This will raise a runtime error if the body evaluates to a non-String
greet : (name: String) -> String -> "Hello " .. name;
```

### Backward Compatibility

All existing function syntax continues to work:

```baba
// Untyped curried function (existing)
multiply : x -> y -> x * y;

// Multi-parameter typed function (existing)
add : (x: Float, y: Float) -> Float -> x + y;

// New: Typed curried function
multiply : (x: Float) -> (Float -> Float) -> y -> x * y;
```

## Typed Tables

Table values carry the `Table` tag and can be typed via variable declarations. Currently, there is no way to create complex types that totally model the typing of the values contained within a table data structure.

```baba
// Variable type declaration (applies to subsequent assignments)
user Table;
user : { name: "Alice", age: 30 };

// Access remains the same
userName : user.name;  // "Alice"
userAge  : user.age;   // 30
```

## Result Type

`Result` encodes success (`Ok value`) or failure (`Err message`).

```baba
divide : x y ->
  when y is
    0 then Err "Division by zero"
    _ then Ok (x / y);

useDivide : when (divide 10 2) is
  Ok val then val
  Err _  then 0;
```
Pattern matching binds inner values:

```baba
// Function returning a Result
parseIntOrErr : (s: String) -> Result ->
  when (str.trim s) is
    "" then Err "Empty"
    _  then Ok 42;  // placeholder

// Consuming Result
answer : when (parseIntOrErr "  10  ") is
  Ok v  then v
  Err e then 0;
```

## Error messages

All runtime errors are thrown as plain `Error` with messages:

```
Type mismatch in function 'add': Expected Int for parameter 'y', but got String (value: "3")
Return type mismatch in function 'greet': Expected String, but got Int (value: 42)
Type mismatch for myValue: expected Int but got String (value: "x")
Division by zero
Index out of bounds: 5
Undefined variable: foo
Undefined property: age of person
Unknown operator: ^
Unexpected token: RPAREN ()) at 12:17
```
When a location is available, the CLI/REPL shows a code frame indicating `line:column`.