name
iridis - a functional language for systems programming
synopsis
iridis [--literals] [--names] [--operators] [--layout] [--control-flow] [--functions] [--pipelines] [--types] [--pattern-matching] [--errors] [--ownership] [--effects] [--modules] [--attributes] [--typestate] [--low-level-and-c] [--examples] [--where-the-ideas-come-from] [--whats-still-open]
description
iridis is a small functional language for code that would usually be written in c: kernels, drivers, firmware, file and network parsers, anything that has to care where its memory lives. source files end in .iri. it's an ml at heart, with pattern matching, variants and small functions that compose, but without the runtime that usually comes with them.
the main idea is that values move through pipelines, and their ownership moves with them. a buffer gets allocated, passes through a few steps, and ends at a step that frees it. if it never needs a name, it never gets one, and you can't forget to free something you never named.
the other rule is that the language shouldn't do anything you can't see or check. if something allocates, you can find the call that does it. if an index might be out of range, either the code doesn't compile or the check is written out. most functional languages hide costs like these behind garbage collection, boxed values, closures on the heap and deep recursion, and none of that works in an interrupt handler. iridis keeps the parts of ml i like and drops those, so it compiles to code that looks a lot like c.
this is a design draft. most of the syntax is settled and a lot of the behaviour isn't. the page goes through the language in order, from literals to complete programs. if you know c and have seen some ocaml or f#, it should be easy to follow.
literals
literals are mostly c's, with a few fixes. a number can carry its width, so 42u8 is a u8. underscores can separate digits. binary starts with 0b and octal with 0o, since c's leading-zero octal catches people out. raw strings sit between {| and |} and are taken as written, which is handy for assembly and regexes.
42u8 -1i64 2.5f32 1_000_000 0b1010 0o755 'a' "text" {|raw "text"|}
a number without a suffix takes whatever type the code around it needs, so in usize count + 1 the 1 is a usize. if nothing decides, it's an i32, or an f64 for decimals. nothing is ever converted for you.
let small: u8 = 200
let next = usize count + 1 # 1 is a usize here
let ratio = 2.5 # f64
string literals are strs, which are covered under types. comments start with # and run to the end of the line, and #* ... *# spans several lines.
# single line comment
#* multi
line comment *#
names
one rule for names
c declares different things in different ways. variables, functions, structs, typedefs, externs and macros all look different. odin noticed they're all a name and what it is, and writes them as name :: what it is. iridis does the same in ml style: every declaration is let name: type = what it is.
let x: i32 = 5 # a value
let mutable n: u32 = 0 # a mutable value
let square = fun (x: i32) -> x * x # a function
let Point: type = { x: f32; y: f32 } # a record type
let Shape: type = | Circle f32 | Empty # a variant type
let Celsius: type = distinct i32 # a distinct type
let Pair = fun (a: type) -> { first: a; second: a } # a generic type
let io = import std.io # a module
let Ord: type = { T: type; compare: (T, T) -> i32 } # a module type is a record type
let int_sorted = sorted int_ord # a functor applied
let malloc: usize -> Option rawptr = extern "malloc" # a c function
a function is just a value made with fun and named with let. a type is a name whose type is type. a module is a record, which is what import returns. a c function is a name, its type and its symbol. you can leave out : type wherever the compiler can work it out, which is most of the time for local values.
keeping one rule means generics are just functions that take and return types, and taking names out of a module is normal destructuring.
mutation
names can't change unless you say so. let mutable makes one changeable, and := stores a new value, so an assignment never looks like a declaration.
let x: i32 = 5
let mutable n: u32 = 0
n := n + 1
every symbol keeps one meaning everywhere. = means "is" and binds a name or a field. == compares, /= compares for not-equal, and := stores into something mutable. so a line with := always changes something, and a line with only = never does. in the same way, : always means "has type", -> means "maps to", and | means "or". it's all plain ascii.
naming
values and functions are snake_case, so they match the c symbols they compile to. types are Upper case, so they stand out.
operators
arithmetic and comparison are c's, with two changes. c's % keeps the sign of the left operand, which is wrong for things like wrapping a ring buffer index. so iridis has rem, which works like c's %, and mod, which gives the floored result, so -1 mod 8 is 7. not-equal is /=, which fits with =, == and :=.
logic and bit operations are words: not, and and or for booleans, and land, lor, lxor, lsl, lsr and asr for bits. that leaves & meaning address and | meaning "or". it also makes you choose between a logical and an arithmetic right shift, which c decides for you from the type.
a + b a - b a * b a / b a rem b a mod b
a == b a /= b a < b a <= b
not a a and b a or b
a land b a lor b a lxor b a lsl n a lsr n a asr n
layout
blocks are indentation. lines indented under a header belong to it, and the block ends when the indentation does. there are no braces and no ends.
the reason is a well-known ocaml problem. ocaml ignores indentation, so a match nested inside another match swallows the arms meant for the outer one. the code looks right and means something else. f# fixed it by making indentation part of the grammar, and iridis does the same.
the rules are strict so there's nothing to guess. a block opens after a line that ends in ->, =, then or else, or starts with match, while, for or with, which is roughly where c would have a {. its lines must be indented at least two spaces more than the line that opened it. a one-space step is an error, and going back out has to land on an earlier level.
any other indented line continues the line above, so long lines can be split. this comes from ante.
let total = first + second
+ third
lines starting with |>, |>? or else also continue the line above, even without extra indentation. that lets a pipeline line up under its first value, and an else under its if.
alloc 4096
|> fill 0
|> free
if ready then start ()
else wait ()
inside brackets, indentation doesn't matter, and inside { } each line is a field. a statement ends at the end of its line, and ; lets two short ones share a line.
n := 0; p^ := 1 # ; joins expressions on one line
control flow
if
if is an expression, so it can sit on the right of a let or end a function. the short form fits on one line, and the long form puts each branch on indented lines.
if c then a else b
if c then
...
else
...
loops
while loops while a condition holds, and for goes over a range or the elements of a slice or array. .. includes the end and ..< stops one before it. ..< matters with unsigned numbers: 0 .. n - 1 breaks when n is a zero usize, because n - 1 wraps around to a huge number.
while running
...
for i in 0 .. 9 # inclusive
...
for i in 0 ..< n # exclusive
...
for x in buf # every element of a slice or array
...
leaving early
return, break and continue work like in c. leaving early is safe, because defer runs its cleanup on every way out.
return e
break
continue
functions
writing a function
a function is fun, its parameters, -> and a body, named with let. the return type goes after the parameters with a : and can be left out. longer bodies go on indented lines.
let square = fun (x: i32) -> x * x # one expression
let square = fun (x: i32): i32 -> x * x # return type written
let greet = fun (name: str) -> # several lines: indent them
io.print "hello, "
io.print name
let clamp = fun (lo: i32, hi: i32, x: i32) ->
if x < lo then lo
else if x > hi then hi
else x
calling a function
in ocaml and haskell, a two-argument function is really a function that returns another function. that lets you pass some arguments now and the rest later, but every partial call creates a closure.
iridis does it the c way: one parameter list, and a call passes all of it, so every call is a normal c call. arguments go in parentheses, and a single argument doesn't need them.
clamp (0, 255, x) # a call: a list in parentheses
square 5 # one argument needs none
there's no partial application. if you want a narrower function, write another let.
lambdas that borrow
small lambdas often use nearby variables, like the limit in a filter. most languages turn that into a closure on the heap.
iridis has a simpler rule: a function you're given as a parameter can be called but not kept. since it can't outlive the call, a lambda can safely borrow local variables, and the compiler inlines it. no closure is created and nothing is allocated.
slice.map (xs, fun x -> x * 2) # the same syntax, unnamed
slice.filter (xs, fun x -> x > limit) # borrows limit; inlined, so no closure
_ is a shorthand for a lambda. it leaves an argument open, so _ > limit means fun x -> x > limit, and add3 (_, 0, _) waits for the two missing arguments. in a pattern, _ just means "ignore this".
slice.filter (xs, _ > limit) # the same lambda, shorter
let add_zero = add3 (_, 0, _) # fun (a, c) -> add3 (a, 0, c)
closures you keep
sometimes a function has to be kept, like a callback for a timer. then it can't borrow, because what it borrowed might be gone by the time it runs. a lambda stored in a name, a field or a return value becomes a closure that carries what it captured: values are copied, owners move in, and borrows keep their origin.
closures usually live on the heap, because their size depends on what they captured. iridis puts the captures in the type instead: Closure (f, env) is the function plus a record of what it captured. the size is known, so a closure can live on the stack or inside a record. a record that holds a callback is generic over that callback, so the callback's size shows up in the record's type.
let over = fun x -> x > limit # Closure (i32 -> bool, { limit: i32 })
let Timer = fun (env: type) -> { period: u32; on_tick: Closure (() -> (), env) }
a closure that captures nothing is a plain function, and only those can be passed to c as callbacks.
recursion
ml code recurses where c would loop, and on a small stack that can run out. in iridis, a function that calls itself needs let rec, so recursion is easy to spot, and each recursive call uses a stack frame like in c.
when the recursive call is the last thing a function does, the frame can be reused, which turns it into a loop. most compilers do this when they can. become makes it a promise: the frame is reused or the code doesn't compile.
let rec fact = fun (n: u64) ->
if n == 0 then 1 else n * fact (n - 1) # a frame per call, like c
let rec fact_acc = fun (n: u64, acc: u64) ->
if n == 0 then acc else become fact_acc (n - 1, acc * n) # reuses the frame
fact still has to multiply after its call returns, so it uses one frame per step. fact_acc carries the product in an argument, so become can reuse a single frame. in practice, folds and pipelines cover most of what recursion is used for.
pipelines
reading in order
nested calls read inside out: the first step is in the middle and the last one is on the left.
free (file.read_into (fill (alloc 4096, 0), f))
a pipeline reads top to bottom instead, without naming every step in between.
alloc 4096
|> fill 0
|> file.read_into f
|> free
x |> f means f x: the piped value becomes the first argument. to put it somewhere else, use _, which turns the call into a lambda that the pipe then calls.
x |> f # f x
x |> f (a, b) # f (x, a, b)
x |> f (a, _) # f (a, x): _ puts it somewhere else
the value goes first because iridis functions take one parameter list. curried languages put it last and fill in the rest with partial application, which needs closures. a pipe is just a call, so it moves or lends a value the same way a call does, which matters a lot once ownership comes in.
map, filter and fold
chaining map, filter and fold normally builds a new list at every step. haskell avoids that with an optimization that merges the steps, but then whether your code allocates depends on the optimizer.
in iridis it's part of the types. map, filter and zip return a Stream, which describes the work without doing it. nothing runs until something like fold, sum or write_into consumes it, and then it's one loop that allocates nothing.
# map, filter and zip build a Stream, a lazy view; a consumer runs it as one loop
let sum_even_squares = fun (xs: []const i32) can () ->
xs |> slice.map square |> slice.filter is_even |> slice.sum
can () says the function has no effects, which is covered later under effects. to store the results, call collect, the one step that allocates.
# collect is the only step that allocates, and you write it yourself
let squares = xs |> slice.map square |> slice.collect
types
a lot of c's quiet mistakes are type mistakes, so this is the longest section. most of it follows from one thing: a type is a name like any other.
a type is a name
types are declared with let, like everything else. since a type is just a value of type type, generics, modules and compile-time code don't need special syntax.
primitives and strings
the primitive types are c's, named by their size: fixed-width integers, two float sizes, bool, and (), which is what a function returns when it has nothing to return. u16le and u32be are integers with a fixed byte order, for binary formats.
# primitives (reserved words)
i8 i16 i32 i64 u8 u16 u32 u64 isize usize f32 f64 bool ()
u16le u32be ... # fixed byte order, for byte patterns
str # []const u8, the type of "text"
cstring # a nul-terminated ^const u8, for c
a str is a slice of bytes, so a pointer and a length. c strings are a separate type, cstring, because they need a zero byte at the end, and converting between the two is always explicit.
pointers, slices and arrays
pointers work like odin's: &n takes an address, ^u32 is a pointer to a u32, and p^ follows it. the ^ comes after the value, so long chains read left to right.
let p: ^u32 = &n
p^ := p^ * 2
in c, an array passed to a function turns into a bare pointer and loses its length. the length has to be passed separately, and the two can get out of sync. a lot of memory bugs come from that.
in iridis, a slice, []t, keeps the pointer and the length together. slicing gives you a new slice with the right length, so a function that takes a slice always knows how long it is.
let head: []u8 = buf.[0 ..< 16] # slicing; the length comes along
head.len
indexing is buf.[i], with a dot, so it can't be mistaken for calling buf on an array.
^t points to exactly one value and is never null. a pointer that can be null is Option ^t, which costs nothing extra, because None is just the null address. [n]t is a fixed-size array stored in place. const and volatile mean what they do in c.
^t # non-null pointer
^const t
^volatile t
[]t # slice: a pointer and its length together
[n]t # inline array
Option ^t # nullable; None is NULL, still one word
records
a record type uses : for its fields, and a record value uses =.
records keep their fields in the order you wrote them, laid out like the same c struct. that's guaranteed, so a record can describe a c struct or a set of hardware registers. @align sets the alignment, and @bits packs a field into a number of bits, filled from the lowest bit up.
one catch: writing a bit field through a volatile pointer reads the whole register, changes some bits and writes it all back. for registers where writing a 1 clears a bit, write the whole register yourself.
# a record type uses :, a record value uses =
@align 8
let Header: type = {
magic: u32
kind: u16 @bits 4
flags: u16 @bits 12
name: [32]u8
}
let h: Header = {
magic = 0x7f
kind = 1
flags = 0
name = zeroed
}
variants
a variant is a value that can be one of several shapes, and it's probably the most useful thing ml has for c programmers. c does this with a tag and a union, and hopes you read the right member. a variant carries its tag, and the compiler won't let you use it until every shape is handled.
each shape follows a |. constructors are called like functions, and @tag sets the size of the tag.
@tag u8
let Shape: type =
| Circle f32
| Rect (f32, f32)
| Empty
let s: Shape = Rect (2.0, 3.0)
distinct types
a distinct type has the same layout as another type but can't be mixed with it. you can't pass an i32 as a Celsius, or a Celsius as a Fahrenheit. at runtime it's just the underlying type.
let Celsius: type = distinct i32
generic types
a generic type is a function from types to a type. Pair takes a type and returns a record, and Pair i32 is a call. there are no angle brackets.
# a generic type is a function from types to a type
let Pair = fun (a: type) -> {
first: a
second: a
}
let p: Pair i32 = {
first = 1
second = 2
}
simd vectors work the same way. Simd (4, f32) is four floats, and arithmetic works on all four lanes at once.
let F32x4: type = Simd (4, f32) # simd vectors are a generic type too
let v: F32x4 = [1.0, 2.0, 3.0, 4.0]
let w = v * v + v # per-lane arithmetic
for generic functions, a lowercase name in a type is a type variable, so id works for any type.
# a lowercase name in a type is a type variable
let id = fun (x: a) -> x
tuples go in parentheses, and function types use ->.
(i32, f32)
(i32, i32) -> i32
refinements
a refinement is a type with a condition, written with where. "an index less than the length" and "a port between 1 and 65535" are both refinements.
# a refinement narrows a type with a condition
let Port: type = u16 where 1 .. 65535
let get = fun (xs: []a, i: usize where i < xs.len) -> xs.[i] # no bounds check emitted
let y = if i < xs.len then get (xs, i) else 0 # the guard proves it
get doesn't check its index, because its type says the index is in range, and every caller has to prove it. in the last line, the if is the proof.
proofs come from a short, fixed list of rules: constants, if and when conditions, simple range math, and loop bounds. if those can't prove it, the code doesn't compile until you add a check. liquid haskell uses a solver for this, which is more powerful but harder to predict. the important part is that nothing the compiler can't prove is ever left unchecked.
units of measure
numbers can carry units. units multiply and cancel, and adding metres to seconds doesn't compile. units are only checked by the compiler and disappear at runtime, which is why they're written as an attribute.
# units of measure are checked, then erased
let g: f32 @unit m/s/s = 9.81
let fall = fun (t: f32 @unit s) -> 0.5 * g * t * t # f32 @unit m
conversions
c converts between number types silently, and sometimes loses data. in iridis, calling a type converts to it, but only when nothing can be lost, like i32 to i64. conversions that can lose data have names, like truncate.
# calling a type converts to it, losslessly; lossy conversions are named
i64 x # widen
Celsius 20
truncate (x, u8) # keep the low bits
refinements help here too. converting a usize to an f32 can lose precision, but if the number is known to be small enough, the conversion is exact and allowed. the audio example uses this.
pattern matching
match
match takes a value apart. each arm is |, a pattern, -> and a result, and when adds a condition.
let area = fun (s: Shape) ->
match s
| Circle r -> 3.14 * r * r
| Rect (w, h) -> w * h
| Empty -> 0.0
match p
| None -> 0
| Some q when q^ > 0 -> q^
| Some _ -> 0
the compiler checks that every shape is covered, so adding a variant shows you every match that needs updating.
is
is checks one pattern inside an expression and returns a bool. names it binds stay available through an and chain and in the then branch, but not after or or not, since there the match might have failed.
if p is Some q and q^ > 0 then q^ else 0
let is_circle = fun (s: Shape) -> s is Circle _
byte patterns
parsing binary data in c means offsets, casts and byte swaps, which are all easy to get wrong. iridis borrows erlang's approach and matches on the bytes directly.
# byte patterns parse binary formats
match packet
| [0x7f454c46: u32be, len: u16le, body: [len]u8, ..] -> Ok body
| _ -> Error BadHeader
each field's type says how many bytes it takes and in what order. literals have to match exactly, a length can refer to an earlier field, .. matches the rest, and _ skips one item. if the data is too short, the arm just doesn't match, so nothing reads out of bounds.
errors
results
there are no exceptions. a function that can fail returns a Result, which is either Ok with a value or Error with a reason.
let? handles the common case. it takes the value if the result is Ok, and returns the error otherwise. defer still runs on that early return, so the file below gets closed either way.
let file_size = fun (path: str) ->
let? f = file.open path
defer file.close f
let? st = file.stat f
Ok st.size
failing steps in a pipeline
|>? is the pipe for steps that return a Result. it only runs the next step after an Ok, and the first Error becomes the result of the whole chain.
# |>? runs the next step only on Ok; the first Error stops the chain
path
|> file.read_all # Result ([]u8, IoError)
|>? json.parse # takes the buffer, and frees it if parsing fails
|>? config.from_json
json.parse takes ownership of the buffer, so it has to free it if parsing fails. the ownership section explains why.
error unions
different steps fail in different ways, with an IoError, a JsonError and so on. instead of making you write a wrapper type, iridis lets an error type be a union, using | for "or", and |>? and let? add each step's errors to it.
let load = fun (path: str): Result (Config, IoError | JsonError | ConfigError) ->
path |> file.read_all |>? json.parse |>? config.from_json
you can match a constructor like NotFound directly, or a whole error type with e: JsonError. if two of the types share a constructor name, put the type's name in front.
match load "app.json"
| Ok cfg -> run cfg
| Error NotFound -> run default_config
| Error (e: JsonError) -> json.report e; 1
| Error _ -> 1
ownership
every value that holds memory or another resource has an owner, and ownership can move. most of the time you don't see it, because borrowing is the default.
borrowing is the default
let b = a makes b a borrow, and a stays the owner. moving is rarer, so it's the one that gets a symbol: let c <- a moves the value, and a can't be used afterwards.
let b = a # borrow
let c <- a # move into a new name
f a # moves a if f's parameter is <-, borrows it otherwise
a |> f # exactly f a
the function decides
a function decides whether it takes ownership by marking the parameter with <-. callers don't repeat the arrow, they just call it, and the compiler checks every call. a pipe works the same way, since it's just a call.
let destroy = fun (t: <- ^Thing) -> ...
let grow = fun (buf: <- []u8, extra: usize) -> ... # owner in, bigger owner out
grow takes the buffer, makes it bigger, maybe moving it in memory, and hands back the new owner. the old name can't be used after the call.
owners in a pipeline
a buffer that only ever moves through pipes never gets a name, so there's nothing to forget.
# a buffer from allocation to free, never named
alloc 4096
|> fill 0
|> file.read_into f
|> tap (fun buf -> io.write (stdout, buf))
|> free
alloc creates the buffer. fill and file.read_into each take it and hand it back, tap lends it out to be printed, and free takes it and ends the chain. if the chain ended before free, the compiler would say the buffer has no owner. in c, the same bug is a missing free somewhere far away.
owner in, owner out
fill looks like a pure function that returns a new buffer, but it actually writes into the same one. that's safe because it owns the buffer while it runs, so nothing else can see the change.
# a step takes the owner and hands it back, or ends the chain
let fill = fun (buf: <- []u8, byte: u8) -> ... # returns buf
let free = fun (buf: <- []u8) -> ... # consumes it
<- before a parameter's type means the function takes ownership. a step either hands the owner back, like fill, or uses it up, like free.
ending with a value
often you want a result from the buffer and then want it freed. use does both: it lends the buffer to a function, frees it, and returns the function's result. tap is the same idea in the middle of a chain.
# a pipeline that ends in a value
let words =
alloc 4096
|> file.read_into f
|> use count_words # lend it to count_words, free it, return the count
count_words only borrows the buffer, so it can't keep it.
when a step fails
if a step takes ownership and then fails, the value it took still has to go somewhere. in iridis, a step that takes an owner has to pass it on, return it inside the Error so the caller can retry, or free it. the compiler checks this, so a failing step can't leak. the typestate section shows both choices.
mutable borrows are exclusive
a []const u8 borrow is read-only, and any number of them can exist at once. a []u8 borrow can write, and while it exists nothing else can touch the buffer. it's rust's rule, and it's what makes updating in place safe.
let zero = fun (buf: []u8) -> ... # a mutable borrow: exclusive while it lives
let total = fun (buf: []const u8) -> ... # a const borrow: any number can share
origins
a borrow is only valid while the thing it points into is. inside a function the compiler figures that out by itself. across functions, an origin written with $ names where a borrow came from. here, $s says the returned line comes from text and can't outlive it.
# a borrowed slice: valid while $s is
let first_line = fun (text: $s str): $s str -> ...
a record that holds a borrow takes an origin like a type parameter, so a Token can't outlive the source text it points into.
# a record holding a borrow takes the origin like a type parameter
let Token = fun ($a) -> {
text: $a str
kind: Kind
}
you only write origins where the compiler can't infer them, which is rare.
where memory comes from
there are three ways to get memory.
the first is a pipeline: memory from the default heap, never named, and freed at the end of the chain.
alloc 4096 |> fill 0 |> free # default heap, no name
the second is a scoped allocator. library code just calls alloc, and the caller picks where that memory comes from for a whole block, like odin's context.
# a scoped allocator: every alloc in the block uses it, and nothing it makes can leave
with allocator = &pool
alloc 4096 |> fill 0 |> parse
the danger with scoped allocators is memory that escapes the block and later gets freed into the wrong allocator. iridis stops that with origins: nothing allocated in a with block can outlive it, and free always gives memory back to the allocator that made it.
the third is the classic way: name the allocation and defer the free.
let buf = alloc 4096 # or name it and defer
defer free buf
linear types
locks have to be released and sockets closed, too. a @linear value has to be used exactly once, so forgetting to release a lock, or releasing it twice, is a compile error.
# linear types: owner rules for things other than memory
@linear
let Lock: type = distinct ^Mutex # must be released exactly once
let release = fun (l: <- Lock) -> ...
effects
some things about a function depend on everything it calls, like whether it allocates, panics or blocks. iridis puts them in the function's type with can, and checks them across every call. a function marked can () can't call anything that allocates, panics or blocks, all the way down. that's how you prove an interrupt handler never touches the heap.
let render = fun (scene: ^const Scene) can () -> ... # allocates, panics and blocks on nothing
let step = fun (m: ^Machine) can Alloc -> ... # may allocate; can't panic or block
let poll = fun (dev: ^Device) can (Block, Panic) -> ...
one effect needs no parentheses, several go in parentheses, and () means none. if you leave the list out, the compiler works it out from the body, so most code never mentions effects.
a function passed as a parameter brings its effects with it. slice.map allocates if the function you give it allocates, and doesn't otherwise.
you can declare your own effects with let Name: effect. a networking library might declare Net and mark its functions can Net. then any function without Net provably can't touch the network, however deep its calls go.
let Net: effect
let checksum = fun (data: []const u8): u32 can () -> ... # can't reach the network, by its type
the compiler can't see inside c, so an extern's effects are taken on trust. and unlike ante's, iridis effects have no handlers. they're only checked by the compiler and cost nothing at runtime, which keeps them usable in interrupt handlers.
modules
a module is a value
import returns a module, which you bind to a name like any other value. taking names out of it is ordinary destructuring. module names are lowercase, so io.printf reads as a namespace and then a function.
let file = import std.file
let { alloc; free } = import std.mem # take names out of a module
files, packages and visibility
each file is a module named after its path, so net/socket.iri is net.socket. the first part of an import path is a package: your own, the standard library, or one in a deps folder. nothing is downloaded while building, and there are no wildcard imports.
names are private to their package unless they're marked @public, so a package only exposes what it chooses to. that's different from @export, which gives a function a c symbol name.
# names are visible across their package; @public lets other packages use one
@public
let count_words = fun (text: str) -> ...
modules are records
ocaml has a separate mini-language for modules, with sig, struct and functors. iridis doesn't need one. an interface is a record type, a module is a record, and a functor is a function that takes and returns records. the only addition is that a record field can be a type, and later fields can refer to it.
# a module type is a record type
let Ord: type = {
T: type
compare: (T, T) -> i32
}
# a module is a record value
let int_ord: Ord = {
T = i32
compare = fun (a: i32, b: i32) -> a - b
}
# a functor is a function that returns a module
let sorted = fun (o: Ord) -> {
sort = fun (xs: <- []o.T) -> ...
}
let int_sorted = sorted int_ord
records that contain types only exist at compile time, so int_sorted.sort calls int_ord.compare directly, with no lookup at runtime. that's also why a file and a module are the same thing: a file is a record of the names it defines.
attributes
the attribute rule
attributes start with @ and apply to the declaration below them. several can share a line, and @@ applies to the whole file. the rule is that an attribute can change how code is checked or compiled, but never what it does. remove them all from a correct program and it still behaves the same.
bounded loops
@@rules bounded_loops makes every loop in a file count over a range or a slice, so the most times it can run is known up front. it's off by default.
@@rules bounded_loops # opt-in rules for the whole file
waiting for hardware needs a timeout, but a "run at most 1000 times" attribute would break the attribute rule, since it changes what the code does. so the limit goes in the loop itself, and you decide what happens when it runs out.
# under bounded_loops every loop is counted, so a wait needs its own way out
for _ in 0 ..< 1000
if ready dev then break
compile time
@comptime runs a declaration while compiling and stores the result. it's the same language, just run earlier, and it's mostly for lookup tables.
# run at compile time; types are already values, so it is the same language
@comptime
let crc_table: [256]u32 = array.init (256, crc_entry)
tests
tests are lets marked @test, kept next to the code they test. normal builds skip them, and --test runs them.
# a test is another let
@test
let counts_two_words = fun () -> assert (count_words "hi there" == 2)
typestate
many apis have rules about order. a socket has to be bound before it listens, and a file has to be open before it's read. c leaves that to the documentation.
iridis puts the state in the type. each state is an empty record, and the socket takes its state as a type parameter, so Socket Fresh and Socket Bound are different types. each step takes the old socket and returns a new one, so calling listen on an unbound socket doesn't compile, and no stale handle is left behind.
# typestate: the state is a type parameter, and a transition takes the old owner
let Fresh: type = {}
let Bound: type = {}
let Listening: type = {}
@linear
let Socket = fun (s: type) -> distinct i32
the socket is @linear too, so it has to be closed exactly once.
steps can fail, and the rule from the ownership section applies. if bind fails, it hands the socket back inside the Error, so you can try another port. if listen fails, it closes the socket itself.
# a step that takes an owner uses it up on every path: Ok passes it on, and
# Error either hands it back (bind, so you can retry) or releases it (listen)
let bind = fun (s: <- Socket Fresh, port: Port): Result (Socket Bound, (IoError, Socket Fresh)) -> ...
let listen = fun (s: <- Socket Bound): Result (Socket Listening, IoError) -> ...
since every step takes a socket and returns one, setting a socket up is a pipeline.
socket ()
|>? bind 8080 # if it fails, the Error carries the socket back
|>? listen
low level and c
c's pointer shapes
in iridis, everything with a known length is a slice or a pointer to an array. for c code that passes pointers of unknown length there's [^]t, and rawptr is c's void*. you only need these when talking to c.
# c's pointer shapes, for interop
[^]t # many-pointer, c's T* with no known length
rawptr # void*
escape hatches
anything the type system can't check, like using a fixed address as a framebuffer, goes through unsafe, so one search finds every unchecked operation.
let vga: ^[2000]volatile u16 = unsafe.ptr 0xB8000 # a pointer to an array in place
vga.[0] := 0x0F41
let addr: usize = unsafe.addr p
let f: ^f32 = unsafe.cast p
let alias = unsafe.untracked p
the vga line points at a pc's text screen: two thousand u16s that the hardware reads, hence volatile. after that one line, indexing it is normal checked indexing. unsafe.untracked makes a copy of a pointer that the ownership checker ignores.
inline assembly
inline assembly takes the instructions as a raw string, plus a list of outputs. reading the cpu's timestamp counter takes one instruction and two outputs.
let rdtsc = fun () ->
let mutable lo: u32 = 0
let mutable hi: u32 = 0
asm ({|rdtsc|}, out ("=a", &lo), out ("=d", &hi))
(u64 hi lsl 32) lor u64 lo
calling c
import_c turns a c header into externs. you can also write an extern by hand, which is the one rule again: a name, a type and a symbol.
# import a c header: its functions become externs
let libc = import_c "stdio.h"
# or write externs by hand, with ownership in the type
let malloc: usize -> Option rawptr = extern "malloc"
let free: <- Option rawptr -> () = extern "free"
let write: (fd: i32, buf: []const u8 @ptr_len) -> isize = extern "write" # crosses as (ptr, len)
hand-written externs can say who owns what, like free taking its pointer. @ptr_len lets an iridis slice be passed to c as a pointer and a length.
how iridis gets compiled isn't decided yet, but functions use the c calling convention and records use c layout, so c and iridis can call each other directly.
examples
here are five small, complete programs, each showing a different part of the language.
word count
wc.iri counts the words in a file.
let file = import std.file
let slice = import std.slice
let io = import std.io
@tag u8
let IoError: type =
| NotFound
| Denied
| ReadFailed
# a word count is not just any usize
let Words: type = distinct usize
# the state the fold carries from byte to byte
let Scan: type = {
words: Words
inside: bool
}
# the state before the first byte
let start: Scan = {
words = Words 0
inside = false
}
let is_space = fun (c: u8) -> c == ' ' or c == '\n' or c == '\t'
let step = fun (s: Scan, c: u8): Scan ->
if is_space c then {
words = s.words
inside = false
}
else if s.inside then s
else {
words = Words (usize s.words + 1)
inside = true
}
let count_words = fun (text: str) can () ->
text
|> slice.fold (start, step)
|> fun s -> s.words
@test
let counts_two_words = fun () ->
assert (count_words "hi there" == Words 2)
let count_file = fun (path: str) ->
path
|> file.read_all # Result ([]u8, IoError)
|>? use count_words # frees the buffer, keeps the count
# the entry point; its value is the exit code
let main = fun (args: []str) ->
match args
| [_, path] ->
match count_file path
| Ok n -> io.printf ("%zu\n", usize n); 0
| Error NotFound -> io.eprint "no such file\n"; 1
| Error _ -> io.eprint "read failed\n"; 1
| _ -> io.eprint "usage: wc FILE\n"; 2
Words is a distinct type, so a word count can't be mixed up with a byte count. count_words is a fold: Scan is the state carried from byte to byte, start is where it begins, and step works out the next state. there's no loop, no mutation and no allocation.
count_file reads the file, which can fail, so it uses |>?. use lends the buffer to count_words and frees it afterwards.
main gets the arguments as a slice of strings and returns the exit code. its nested match needs no parentheses, thanks to the layout rules.
a uart driver
uart.iri drives a 16550-style serial port, with no operating system underneath.
@@rules bounded_loops
# the line status register, one flag per bit, from bit 0 up
let LineStatus: type = {
data_ready: bool @bits 1
overrun: bool @bits 1
parity: bool @bits 1
framing: bool @bits 1
break_seen: bool @bits 1
tx_empty: bool @bits 1
idle: bool @bits 1
fifo_error: bool @bits 1
}
# the registers, in hardware order; a record keeps c layout
let Uart: type = {
data: u8
ier: u8
fcr: u8
lcr: u8
mcr: u8
status: LineStatus
}
let Baud: type = u32 where 50 .. 115200
let UartError: type = | Timeout
let uart0: ^volatile Uart = unsafe.ptr 0x1000_0000
let put = fun (u: ^volatile Uart, b: u8): Result ((), UartError) can () ->
for _ in 0 ..< 100_000 # counted, so bounded by construction
if u.status.tx_empty then
u.data := b
return Ok ()
Error Timeout
let write = fun (u: ^volatile Uart, s: str): Result ((), UartError) ->
for b in s
let? _ = put (u, b)
Ok ()
let init = fun (u: ^volatile Uart, baud: Baud) ->
let divisor = 115200 / baud # Baud is at least 50, so never a division by zero
u.lcr := 0x80 # expose the divisor latch
u.data := truncate (divisor, u8)
u.ier := truncate (divisor lsr 8, u8)
u.lcr := 0x03 # 8 data bits, no parity, 1 stop bit
@export "kmain" # bare metal: the boot code jumps to this c symbol
let kmain = fun (): () ->
init (uart0, 115200)
let _ = write (uart0, "hello from the kernel\n") # nowhere to report a timeout yet
LineStatus and Uart describe the hardware registers. bit fields fill from bit 0 and records keep c layout, so every field lands where the hardware expects it. uart0 points at the device through a volatile pointer.
put waits for the transmitter with a counted loop, and returns Error Timeout if the port never becomes ready. write sends a string and stops at the first timeout.
in init, baud is at least 50, so the compiler knows 115200 / baud can't divide by zero. truncate makes it clear that each register gets only eight bits of the divisor.
kmain is the entry point the boot code jumps to, and @export gives it that name. let _ drops write's result on purpose.
parsing a udp packet
udp.iri pulls a udp datagram out of a raw ipv4 packet.
let ParseError: type =
| TooShort
| NotIpv4
| NotUdp
| HasOptions
| BadHeader
let Port: type = u16 where 1 .. 65535
let Datagram: type = {
src: Port
dst: Port
body: []const u8
}
# a 20-byte IPv4 header with no options: version and length, 8 bytes, the protocol, 10 bytes
let ip_payload = fun (pkt: []const u8): Result ([]const u8, ParseError) ->
match pkt
| [0x45: u8, _: [8]u8, 17: u8, _: [10]u8, rest: []const u8] -> Ok rest
| [0x45: u8, _: [19]u8, ..] -> Error NotUdp
| [v: u8, _: [19]u8, ..] when v lsr 4 == 4 -> Error HasOptions
| [_: u8, _: [19]u8, ..] -> Error NotIpv4
| _ -> Error TooShort
# a UDP header: source, destination, the length of header and body, a checksum
let udp = fun (payload: []const u8): Result (Datagram, ParseError) ->
match payload
| [src: u16be, dst: u16be, len: u16be, _: u16be, ..]
when src /= 0 and dst /= 0
and 8 <= len and usize len <= payload.len ->
Ok {
src = Port src
dst = Port dst
body = payload.[8 ..< usize len]
}
| [_: [8]u8, ..] -> Error BadHeader
| _ -> Error TooShort
let parse = fun (pkt: []const u8) ->
pkt |> ip_payload |>? udp
@test
let rejects_tcp = fun () ->
let tcp: [20]u8 = [
0x45, 0, # version and header length, type of service
0, 20, # total length
0, 0, 0, 0, # id, flags, fragment offset
64, 6, # time to live, protocol 6 is tcp
0, 0, # checksum
10, 0, 0, 1, # source address
10, 0, 0, 2 # destination address
]
assert (parse tcp == Error NotUdp)
ip_payload accepts version 4 with a plain 20-byte header and protocol 17, which is udp. the other arms say what went wrong, and since arms are tried in order, each one only sees what the earlier ones rejected.
udp's guard checks that both ports are non-zero, which makes them valid Ports, and that the length fits inside the data, which proves the slice is in bounds. so there's no separate bounds check.
parse chains the two with |>?, and the test checks that a tcp packet is rejected as NotUdp.
an echo server
echo.iri is a tcp server that sends back whatever it receives.
let net = import std.net
let arena = import std.arena
let io = import std.io
let { Socket; Connected } = net
# one connection, one arena: everything echo allocates is freed in one go
let echo = fun (conn: <- Socket Connected) ->
defer net.close conn
let mutable pool = arena.create (64 * 1024)
defer arena.destroy pool
with allocator = &pool
match alloc 4096 |> net.recv conn |>? net.send conn
| Ok _ -> ()
| Error _ -> io.eprint "echo failed\n"
let serve = fun (port: Port) ->
let? listener =
net.socket ()
|>? net.bind port # Socket Fresh -> Socket Bound; closes it if binding fails
|>? net.listen # Socket Bound -> Socket Listening
defer net.close listener
while true
match net.accept listener # borrows the listener, returns a new connection
| Ok conn -> echo conn # moves conn: echo's parameter is <-
| Error _ -> io.eprint "accept failed\n"
serve sets up the socket as a pipeline of state changes, and let? returns early if one fails. net.bind closes the socket itself if it fails. the accept loop runs forever, which is why this file doesn't use bounded_loops. each connection is moved into echo.
echo owns its connection and closes it at the end. it allocates from an arena that's destroyed when it returns, and nothing from that arena can escape.
mixing audio
mix.iri mixes two audio tracks.
let slice = import std.slice
let array = import std.array
let F32x4: type = Simd (4, f32)
# units cancel: seconds times samples per second is a plain number
let rate: f32 @unit 1/s = 48_000.0
let block: f32 @unit s = 0.005
let frames_per_block = block * rate # 240.0, no unit
# a fade-out curve, built at compile time; i < 1024, so f32 i is exact
@comptime
let fade: [1024]f32 = array.init (1024, fun i -> 1.0 - f32 i / 1024.0)
# mix two tracks, four samples per instruction
let mix = fun (a: []const F32x4, b: []const F32x4, gain: f32, out: []F32x4) can () ->
let g = F32x4 gain # calling the type broadcasts to every lane
slice.zip (a, b)
|> slice.map (fun (x, y) -> (x + y) * g) # borrows g; inlined, so no closure
|> slice.write_into out # a stream: one loop, no buffer in between
the units check that a rate times a duration gives a plain number of frames. fade is built at compile time, and its f32 i conversion is allowed because i is known to be under 1024.
mix handles four samples at a time, and F32x4 gain copies the gain into all four lanes. zip and map build a stream, so the whole thing is one loop with no buffers in between. the lambda borrows g, which is fine because map can't keep it, and out is borrowed mutably, so nothing else can touch it while mix runs.
where the ideas come from
almost none of this is new. the work was picking pieces that fit together without a runtime.
the declaration rule, ^ pointers, slices and scoped allocators come from odin. the overall shape is ocaml's, and significant indentation is f#'s fix for ocaml's nested matches. ante is probably the closest relative, and it gave iridis the layout rules, is, _ lambdas, closures with their captures in the type, literals typed by context, the package layout, and effects in function types.
first-argument pipes come from elixir and gleam. updating in place when nothing else can see the value is koka's "functional but in place", which follows clean's uniqueness types. use is haskell's bracket, tap is elixir's, |>? is f#'s railway style, streams are like rust's iterators, and modules as records are close to 1ml.
byte patterns are erlang's, refinements are liquid haskell's without the solver, and units are f#'s. generics as functions, @comptime, tests next to the code and import_c are zig's. borrowing lambdas work like swift's non-escaping closures and kotlin's inline lambdas. exclusive mutable borrows and become are rust's, and bounded loops are rule two of nasa's power of ten.
what's still open
a lot of this is still on paper.
the refinement rules are the part i'm least sure about. they need to prove what real code needs while staying small enough to learn quickly, and i won't know where that balance is until i've written a lot of code.
scoped allocators need more thought. a library function doesn't know which with block it's called from, so the origin has to reach it without cluttering every signature. passing it implicitly is the obvious answer, but i don't know yet whether that stays simple.
the rule for owners on the error path makes some signatures long, like bind's. it probably needs a shorter way to write it.
and the language is still bigger than i'd like. most of it reuses the one rule for names, but refinements, origins and effects each take real effort to learn, and each of them has to be worth that.
see also
hecc(7), hiv(7), style-guide(7), blabbing(7), hachem(1)
author
hachem <im@hachem.wtf>