type-inference-validation

Files (1)

• SKILL.md

SKILL.md (first lines)

# Type Inference Validation

## Core Concept

Static type validation that **rejects invalid path compositions before caching**. Every Navigator path must prove type compatibility with its input structure—this skill enforces that proof.

Works alongside Möbius filtering as a second line of defense: Möbius eliminates topological impossibilities, Type Inference eliminates structural impossibilities.

## Why Type Validation?

Consider this dangerous scenario:
```julia
data_numbers = [1, 2, 3, 4, 5]
data_dict = Dict("x" => 10, "y" => 20)

# This path makes sense for numbers
nav1 = @late_nav([ALL, pred(iseven)])  # Type ✓: Vector → Numbers → Numbers

# But what if someone mistakenly uses it on the dict?
nav_select(nav1, data_dict, x -> [x])
# => IndexError! (dicts don't support ALL enumeration this way)
```

**Type Inference Validation prevents this at compile time**, not runtime.

## Architecture

### Type System

Each Navigator carries a **type signature**:
```
Navigator{InputType, OutputType, PathSteps}
```

Examples:
```julia
nav_vector = Navigator{Vector, Vector, [ALL, pred(f)]}
nav_dict = Navigator{Dict, Vector, [keypath(k), ALL]}
nav_sexp = Navigator{SExpression, Symbol, [sexp_nth(2), SEXP_HEAD]}
```

### Type Refinement Pipeline

```
Input Type
    ↓
@late_nav(path_expr) triggers validation
    ↓
Type each step in path:
  [ALL] : Vector{T} → T
  [keypath(k)] : Dict{K,V} → V
  [pred(f)] : T → T (preserves type)
  [INDEX(i)] : Vector{T} → T
  [SEXP_HEAD] : SExpr → Symbol
    ↓
Unify step outputs with next step inputs
    ↓
Final output type computed
    ↓
Cache with type signature
    ↓
Accept or Reject
```

### Type Incompatibility Detection

| Step | Input Type | Output Type | Valid? |
|------|-----------|------------|--------|
| `[ALL]` | Vector{T} | T | ✓ |
| `[ALL]` | Dict{K,V} | ⚠️ (ambiguous) | ✗ |
| `[keypath(k)]` | Dict{K,V} | V | ✓ |
| `[keypath(k)]` | Vector{T} | ✗ | ✗ |
| `[pred(f)]` | T | T | ✓ |
| `[INDEX(i)]` | Vector{T} | T | ✓ |
| `[INDEX(i)]` | Dict | ✗ | ✗ |

## API

### Type Inference

**`infer_type(path_expr, input_type) :: Result{OutputType, Error}`**
Computes the output type of a path given an input type.

```julia
infer_type([ALL, pred(iseven)], Vector{Int})
# => Result(Int)  # outputs Int values

infer_type([keypath("x"), ALL], Dict{String, Vector{Int}})
# => Result(Int)  # navigates to x, then enumerates integers

infer_type([keypath("x")], Vector{Int})
# => Result(TypeError("Cannot apply keypath to Vector"))
```

**`validate_path(navigator::Navigator, input_type) :: Bool`**
Checks if a Navigator is compatible with a given input type.

```julia
nav = @late_nav([ALL, pred(f)])
validate_path(nav, Vector{Int})      # => true
validate_path(nav, Dict{String, Int})  # => false ✗

# Causes @late_nav to reject the Navigator before caching
```

### Type Signatures

**`navigator_signature(nav::Navigator) :: TypeSignature`**
Returns the full type signature of a cached Navigator.

```julia
nav = @late_nav([ALL, pred(iseven)])
sig = navigator_signature(nav)

# => TypeSignature(
#     input: Vector{T},
#     output: T,
#     constraints: [iseven(T)],
#     steps: [[ALL], [pred(iseven)]],

From plurigrid/asi, MIT.

More from plurigrid/asi