Language Guide

IRIS uses an ML-like surface syntax that compiles to SemanticGraph – the canonical program representation. The syntax is a human-friendly projection of typed DAGs with 20 node kinds.

Basics

Comments

-- This is a line comment

Let Bindings

let x = 42 in x + 1

-- With type annotation and cost
let double n : Int -> Int [cost: Unit] =
  n * 2

Recursive Functions

let rec factorial n : Int -> Int [cost: Linear(n)] =
  if n <= 1 then 1
  else n * factorial (n - 1)

Lambdas

let add = \x y -> x + y

-- Used with higher-order functions
fold 0 (\acc x -> acc + x) xs

Comparing Styles

let..in, |>, and lambdas are interchangeable ways to express the same computation. Choose whichever reads best.

Goal: take a list, keep positives, double them, sum the result.

With let..in (name each intermediate step):

let process xs : List Int -> Int =
  let positives = filter (\x -> x > 0) xs in
  let doubled = map (\x -> x * 2) positives in
  fold 0 (+) doubled

With |> (pipeline, no intermediate names):

let process xs : List Int -> Int =
  xs |> filter (\x -> x > 0)
     |> map (\x -> x * 2)
     |> fold 0 (+)

With nested application (fully inline):

let process xs : List Int -> Int =
  fold 0 (+) (map (\x -> x * 2) (filter (\x -> x > 0) xs))

All three compile to the same SemanticGraph. let..in is clearest when you need to reuse an intermediate value or give it a meaningful name. |> is clearest for linear data pipelines. Nested application works for short expressions but gets hard to read as chains grow.

Types

Primitive Types

Composite Types

Tuples are the universal container. At runtime, all sequences are Tuple(Vec<Value>) – a dynamically-sized vector. There is no separate list type. fold, map, filter, and all collection operations work on tuples:

let point = (1, 2, 3)             -- 3 elements
let xs = (10, 20, 30, 40, 50)    -- 5 elements, same type
let pair = ("hello", 42)          -- mixed types are fine
let empty = ()                    -- 0 elements (unit)

-- Access by index
let x = point.0                   -- 1
let y = point.1                   -- 2

-- Collection ops work on any tuple
let total = fold 0 (+) xs         -- 150
let big = filter (\x -> x > 20) xs  -- (30, 40, 50)

-- Tuples grow and shrink dynamically
let extended = list_append xs (60, 70)  -- (10, 20, 30, 40, 50, 60, 70)
let first3 = list_take xs 3             -- (10, 20, 30)

The type system can express fixed-arity products (Product(Vec<TypeId>)) and sized homogeneous vectors (Vec(TypeId, SizeTerm)), but at runtime the representation is the same dynamic vector. Operations like list_append, filter, and list_take return new tuples of different lengths.

A Note on Types

IRIS is dynamically typed at runtime. Type annotations are parsed but the lowerer drops them – functions accept any value type. There is no static type checker. Type annotations serve as documentation.

Cost Annotations

Every function signature can carry a cost term:

let sum xs : List Int -> Int [cost: Linear(xs)] = fold 0 (+) xs
let lookup m k : Map -> Key -> Value [cost: Log(n)] = ...
let sort xs : List Int -> List Int [cost: NLogN(xs)] = ...

Available cost terms:

Cost annotations are metadata, not enforcement. Today they serve two purposes:

1. Evolution guidance – cost is one of 5 NSGA-II Pareto fitness objectives. The evolution engine prefers lower-cost solutions when correctness is equal, so declaring cost helps steer the search.
2. Documentation – cost annotations communicate the intended complexity class to readers, similar to how Rust’s #[must_use] is advisory.

The proof kernel contains cost subsumption rules (cost_subsume, cost_leq_rule) and a cost lattice algebra, but these are not wired into proof construction. Today the declared cost is trusted, not checked against the implementation.

Control Flow

Conditionals

if n <= 1 then 1
else n * factorial (n - 1)

Pattern Matching

match expr with
  | 0 -> "zero"
  | 1 -> "one"
  | _ -> "other"

Fold (Catamorphism)

Fold is the primary iteration construct, replacing loops:

-- Sum a list
fold 0 (+) xs

-- Count elements
fold 0 (\acc x -> acc + 1) xs

-- Map via fold
fold () (\acc x -> list_append acc (f x)) xs

Unfold (Anamorphism)

Unfold generates sequences from a seed value. It’s the dual of fold – fold consumes a structure, unfold produces one.

-- Generate a range: seed=0, step produces (element, next_state)
-- Stops when the predicate returns true or the budget is exhausted
unfold (\n -> if n >= 10 then None else Some (n, n + 1)) 0
-- produces (0, 1, 2, 3, 4, 5, 6, 7, 8, 9)

The eager unfold materializes elements into a tuple with a hard cap of 1,000 elements. list_range caps at 10,000. For unbounded sequences, use lazy lists instead (see below).

For simple ranges, list_range is more convenient:

let xs = list_range 0 100    -- (0, 1, 2, ..., 99)

Lazy Lists (Infinite Streams)

IRIS supports lazy infinite lists via thunks – suspended computations that produce one element at a time without materializing the entire sequence in memory.

lazy_unfold – Create a lazy stream

lazy_unfold takes a step function and a seed, returning a Thunk. The step function receives the current state and returns (element, next_state) to produce an element, or () to signal end of stream.

-- Natural numbers: 0, 1, 2, 3, ...
let naturals n = lazy_unfold (\s -> (s, s + 1)) n

-- Fibonacci sequence: 0, 1, 1, 2, 3, 5, 8, ...
let fibs = lazy_unfold (\s -> (s.0, (s.1, s.0 + s.1))) (0, 1)

-- Powers of 2: 1, 2, 4, 8, 16, ...
let powers_of_2 = lazy_unfold (\s -> (s, s * 2)) 1

-- Finite stream: countdown from n to 1
let countdown n = lazy_unfold (\s -> if s > 0 then (s, s - 1) else ()) n

-- Constant stream: repeat a value forever
let repeat x = lazy_unfold (\s -> (s, s)) x

Creating a lazy_unfold is O(1) – it returns a Thunk immediately without computing any elements.

lazy_take – Materialize elements

lazy_take n stream forces the first n elements from a lazy stream, returning them as a tuple. If the stream ends before n elements, you get however many were produced.

lazy_take 10 (naturals 0)        -- (0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
lazy_take 10 fibs                -- (0, 1, 1, 2, 3, 5, 8, 13, 21, 34)
lazy_take 8 powers_of_2          -- (1, 2, 4, 8, 16, 32, 64, 128)
lazy_take 1000 (countdown 5)     -- (5, 4, 3, 2, 1)  -- stream ends at 5 elements

lazy_map – Transform a lazy stream

lazy_map f stream applies a function to each element lazily, producing a new lazy stream. No elements are computed until the result is forced with lazy_take or fold.

-- Even numbers: 0, 2, 4, 6, 8, ...
let evens = lazy_map (\x -> x * 2) (naturals 0)
lazy_take 5 evens                -- (0, 2, 4, 6, 8)

-- Squares: 0, 1, 4, 9, 16, ...
let squares = lazy_map (\x -> x * x) (naturals 0)
lazy_take 5 squares              -- (0, 1, 4, 9, 16)

thunk_force – Manual stepping

thunk_force advances a thunk by one step, returning (element, next_thunk). This is the low-level primitive that lazy_take is built on.

let stream = naturals 0
let step1 = thunk_force stream    -- (0, <thunk>)
let step2 = thunk_force step1.1   -- (1, <thunk>)
let step3 = thunk_force step2.1   -- (2, <thunk>)

Composing with fold

fold is thunk-aware – when given a lazy stream (after lazy_take), it processes the materialized elements normally:

-- Sum first 100 natural numbers = 5050
fold 0 (+) (lazy_take 100 (naturals 1))

-- Sum of squares 0² + 1² + ... + 9² = 285
fold 0 (+) (lazy_take 10 (lazy_map (\x -> x * x) (naturals 0)))

Pipeline style

Lazy streams compose naturally with |>:

let sum_of_even_squares n =
  naturals 0
  |> lazy_map (\x -> x * x)
  |> lazy_map (\x -> x * 2)
  |> lazy_take n
  |> fold 0 (+)

Pipe Operator

xs |> filter (\x -> x > 0) |> map (\x -> x * 2)

Operators

Arithmetic

+, -, *, /, %, neg, abs, min, max, pow

Comparison

==, !=, <, >, <=, >=

Logic

&&, ||, !

Bitwise

and, or, xor, not, shl, shr, rotl, rotr, popcount, clz

Graph Introspection

IRIS programs can inspect and modify their own representation. Every program is a typed DAG – these opcodes let you walk, edit, and evaluate that DAG at runtime:

-- Capture your own program as a value
let me = self_graph ()

-- Walk the graph: get the root, then inspect it
let root = graph_get_root me              -- NodeId
let kind = graph_get_kind me root         -- 0x00=Prim, 0x02=Lambda, etc.

-- Modify: change the root's opcode from add (0x00) to mul (0x02)
let modified = graph_set_prim_op me root 0x02

-- Build new structure: add a Lit node (kind=5) with arity 0
let new_node = graph_add_node_rt me 5 0
graph_connect me root new_node 0          -- wire it as child at slot 0

-- Evaluate the modified graph with inputs (10, 20)
let result = graph_eval modified (10, 20) -- returns 200 if mul

This is how IRIS programs improve themselves – by manipulating their own graph representation.

Effects and I/O

Side effects are explicit and controlled via the Effect node kind:

-- File operations
let fd = file_open "data.txt" "r"
let contents = file_read_bytes fd 4096
file_close fd

-- TCP networking
let conn = tcp_connect "example.com" 80
tcp_write conn request
let response = tcp_read conn 65536
tcp_close conn

-- Time and environment
let now = clock_ns
let val = env_get "HOME"

Capability-Based Security

Control what effects a program can perform:

allow [FileRead, FileWrite "/tmp/*", TcpConnect "api.*"]
deny [ThreadSpawn, MmapExec, NetworkListen]

Capabilities are checked at runtime before executing Effect nodes. This prevents privilege escalation in evolved code.

Modules and Imports

Imports are content-addressed by BLAKE3 hash (the #hex... literal). This is how IRIS packages work: a hash identifies a specific, immutable fragment; there is no path-based resolution or central registry.

import #abc123def456... as math
import #789fead00123... as list

The hash refers to the BLAKE3 content hash of the imported fragment. Use iris store list or your package registry to look up hash values for published fragments.

Keywords Reference

let, rec, in, val, type, import, as, match, with, if, then, else, forall, true, false, requires, ensures, allow, deny, fold, lazy_unfold, lazy_take, lazy_map, thunk_force