Language Guide

This guide is a quick tour of Bosatsu syntax. For installation and running code, see Getting started.

What “simple” means

Bosatsu aims to be simple, but not always easy.

Simple here means the language has a small core model:

1. structs and enums
2. creating values
3. creating functions
4. calling functions
5. matching on values to take them apart

Conceptually, this is close to the simply typed lambda calculus with algebraic data types, mapped onto a Python-like syntax. It is combined with a package system (package, from ... import, export) so code can be composed safely across libraries.

It is deliberately missing many common language features: methods, subtyping, mutable variables (or any mutation), casts, exceptions, and built-in magical hash/equals/string rendering behavior.

We want the language to be as simple as possible, but no simpler. If we relax the constraints too far, we risk losing non-negotiable properties: a sound type system we can trust, and recursion/loop forms with proven termination (so we do not admit nonsense inhabitants of types such as forall a, b. a -> b).

Bosatsu also aims for source that is easy for humans to reason about locally. The compiler may do sophisticated work such as type inference, totality checking, and recursion checking, but the logic flow should remain literal in the code. A reader should be able to see:

1. the package interface at the top of the file
2. where each non-predef name comes from
3. control flow directly from syntax rather than hidden mutation, implicit effects, or implicit currying

Quick start (5 minutes)

A tiny, complete file:

package Demo/Hello

enum Mood: Happy, Sad

def greet(m: Mood) -> String:
  match m:
    case Happy: "hello"
    case Sad: "cheer up"

test = Assertion(greet(Happy) matches "hello", "greet")

Run tests from the repo root:

./bosatsu lib test

Source files and packages

Each file declares exactly one package at the top:

package Animals/Favorites

All external names must be explicitly imported, and all values are private unless exported:

package Animals/Report

from Animals/Favorites import mammals
export most_fav

most_fav = match mammals:
  case [head, *tail]: head
  case []: "who knows?"

This is a design philosophy, not just a parser rule. A human reading a file should be able to answer:

1. which packages this file depends on
2. what values and types this package exposes
3. where each external name used below came from

Bosatsu is stricter about names than about type annotations. If source literally mentions a type from another package, import that type so the dependency stays explicit. If a foreign type appears only through inference from values you already import from a direct dependency, no extra type import is required.

Bosatsu/Predef is the standard exception: its names are available by default, though you can still import or rename predef names explicitly when that is clearer.

Literals

Signed big integers

Like Python, Bosatsu supports literal signed big integers.

x = 1
y = 42
z = -1024

Unicode strings

Bosatsu files are UTF-8 files and between " or ' characters we can create any unicode string:

message1 = 'bar'
message2 = "this has 'single quotes'"

There is string interpolation syntax:

profile = "my favorite animal is ${animal}"
first = "first letter: $.{letter}"

Where animal would be any expression that has type String, and letter has type Char.

Character literals

Characters are single Unicode codepoints written with a leading dot:

letter = .'x'

Lists and list comprehensions

Like Python, Bosatsu supports a syntax for literal lists:

favorite_animals = ["elephant", "humpback whale", "dog"]

Unlike Python, but like all of Bosatsu, lists are immutable values. In addition to ability to construct lists from items, we can also “splice” in other lists:

new_favorites = ["mammoth", *favorite_animals]

We can also build lists with comprehensions:

squares = [mul(i, i) for i in range(10)]

Just as we can build up lists literally, we can also use match to tear them down which we discuss more later:

top_animal = match new_favorites:
  case [most_fav, *rest]: most_fav
  case []: "no favorites, :("

Bindings

All bindings start with a lowercase character and do not contain whitespace.

All bindings point to immutable values, because all values are immutable in Bosatsu. Bindings, however, are almost like mutable variables due to the ability to shadow:

def increment_by_2(x):
  x = add(x, 1)
  x = add(x, 1)
  x

This is a legal program. Don’t think of x being mutated (since it isn’t if it is captured by an anonymous function). Think of each new line being a new variable that happens to have the same value.

Note this is a difference from python: in python capturing works by reference, not by value, so if the original value is changed, so is the capture. Not so in Bosatsu: lexical scope is always in play.

Bosatsu enforces that shadowing for let bindings and match pattern bindings within a def, and within the body of a top-level binding, keeps the same type. def and lambda parameters may always start a new shadow.

Naming style

For consistency across the bosatsu compiler repository, prefer these naming conventions:

1. Bindable names (defs, values, parameters, locals) use lowercase with underscore separation.

2. Type and constructor names use UpperCamelCase.

3. If a bindable name includes a type name, put the full type name at the end after an underscore.

Examples:

# preferred bindable names
def fold_left_Tree(t: Tree[a], init: b, fn: (b, a) -> b) -> b: ...
def one_of(ps: List[Parser[a]]) -> Parser[a]: ...
def string_to_Int(s: String) -> Option[Int]: ...
eq_TreeList_Int = eq_TreeList(eq_Int)

# avoid
def foldTree(...): ...     # camelCase bindable
def Tree_fold(...): ...    # type name in first position
def fold_T(...): ...       # partial/abbreviated type name

This convention keeps names readable and searchable, especially when multiple implementations of a common operation exist for different types.

Block expressions

You can group a sequence of bindings and defs in parentheses to produce a value. The last expression is the result:

result = (
  x = 1
  y = x.add(1)
  (x, y)
)

Left-Apply Syntax

Left-apply (<-) is syntax for continuation-style bindings inside blocks.

A line pat <- expr appends the continuation lambda (pat -> ...) to the outermost function application in expr:

p <- foo(a, b)              # foo(a, b, p -> ...)
p <- foo(a)(b)              # foo(a)(b, p -> ...)
p <- x.await()              # await(x, p -> ...)
p <- x.await().map(f)       # map(await(x), f, p -> ...)

This is the Bosatsu form of await-style code, monadic-do notation, and Scala for-comprehensions.

Await-style example:

def await(p, fn): p.flat_map(fn)

main = (
  args <- read_env.await()
  _ <- println("args = ${args}").await()
  pure(0)
)

List flat_map example:

pair_sums = (
  x <- [1, 2, 3].flat_map()
  y <- [x, x.add(10)].flat_map()
  [add(x, y)]
)

Option helper example:

def if_Some(opt: Option[a], fn: a -> Option[b]) -> Option[b]:
  flat_map(opt, fn)

sum_if_both_some = (oa: Option[Int], ob: Option[Int]) -> (
  a <- oa.if_Some()
  b <- ob.if_Some()
  Some(add(a, b))
)

Functions

As we have seen in above examples, each function returns a single value which is the final expression in the function block. The reason for this difference with Python is that in Bosatsu, there are no side-effects. There is no reason to compute something if it is not going to be returned, and as such, the last line of every def is the return value. Like Python chooses to omit return in lambda expressions, we remove return entirely from Bosatsu.

Bosatsu has 32 function arities (Fn1..Fn32). A def with N parameters defines an FnN, and each arity is a distinct type. There is no automatic currying. If you want a function that returns a function, write that explicitly with a lambda.

So, we can write:

def add_with_three(x, y):
  add(add(x, y), 3)

Bosatsu has anonymous function syntax. The above is almost exactly the same as:

add_with_three = (x, y) -> add(add(x, y), 3)

A few forms to know:

inc = x -> add(x, 1)                 # Fn1
add2 = (x, y) -> add(x, y)           # Fn2
add_curried = x -> y -> add(x, y)    # Fn1 returning Fn1
add_tuple = ((x, y)) -> add(x, y)    # Fn1 taking a tuple

Note the distinction between (x, y) -> ... (Fn2) and ((x, y)) -> ... (Fn1 that takes a tuple).

Bosatsu also supports Python-style zero-arg function sugar for Unit -> a:

def later():
  compute()

value = later()

These are equivalent to:

def later(()):
  compute()

value = later(())

The corresponding function type is still written as () -> a.

Function parameters are patterns, so you can destructure arguments directly:

def fst((a, _)): a
sum = ((x, y)) -> add(x, y)

Scope difference for defs

Unlike normal bindings, defs ARE in scope in their body. However, in order to prevent unbounded loops there are strict rules on accessing defs inside themselves. If you don’t intend to write a recursive def, then you can never reuse or access the def’s name anywhere inside the body. Specifically, shadowing the def name is not allowed. To write a recursive def see the section on recursive functions below.

Method syntax

Bosatsu does not have methods, only functions, it does however have method syntax.

form1 = add(x, y)
form2 = x.add(y)

The above two forms are equivalent. foo.bar means pass foo as the first argument to bar. This scales to more arguments:

form3 = f(x, y, z)
form4 = x.f(y, z)

Operators

Operators are just functions whose names are written with the operator prefix, and infix expressions call those functions:

def operator +(a, b): a.add(b)
operator == = eq_Int

x = 1 + 2
y = 1 == 1

You can also import or rename operators:

from Bosatsu/Predef import add as operator +

Recursive functions

Bosatsu supports recursion through recur and loop, but only in forms the compiler can prove terminate. A simple structural example:

def len(lst):
  recur lst:
    case []: 0
    case [_, *tail]: len(tail).add(1)

Tail-recursive style is common:

def len(lst):
  def loop(acc, lst):
    loop lst:
      case []: acc
      case [_, *tail]: loop(acc.add(1), tail)

  loop(0, lst)

loop enforces that all recursive self-calls are in tail position. recur keeps the same termination checks but allows valid non-tail recursion.

recur can also follow trusted delayed-value projections. If a branch binds th: () -> T or l: Lazy[T], then th() and trusted Bosatsu/Lazy.get_Lazy(l) are treated like smaller children of the current value. Those facts compose through let bindings and nested match destructuring.

enum Stream[a]:
  End
  More(next: () -> Stream[a])

def consume(s: Stream[a]) -> Stream[a]:
  recur s:
    case End:
      End
    case More(th):
      next = th()
      consume(next)

Tuple recursion targets are also supported and checked lexicographically in the target order:

def ack(n: Nat, m: Nat) -> Nat:
  recur (n, m):
    case (Zero, _): Succ(m)
    case (Succ(n_prev), Zero): ack(n_prev, Succ(Zero))
    case (Succ(n_prev), Succ(m_prev)): ack(n_prev, ack(n, m_prev))

In recur (a, b, ...), a recursive call is accepted when the first target position that changes is smaller; earlier target positions must stay equal.

For full recursion rules and advanced patterns (fuel, divide-and-conquer with a size bound, string recursion, trees, Ackermann-style nested recursion), see Recursion in Bosatsu.

Loops (with recur and loop)

Bosatsu has no while or for. Loops are recursive defs using recur or loop. In practice this is stricter than loops in most languages users have seen: we allow loops, but only when the compiler can prove they terminate. That restriction is what preserves type-system soundness.

Most loops are either:

1. structural recursion on subvalues (like a list tail or tree branch), or
2. explicit fuel recursion on a decreasing Nat.

Choose loop when you want the compiler to require tail recursion. Choose recur when the algorithm is terminating but not tail-recursive.

See Recursion in Bosatsu for detailed examples from test_workspace.

Pattern Matching

Bosatsu has powerful pattern matching. You can match on literal values, strings and lists in addition to user defined types as discussed later. Use case in every match branch.

Here are some examples:

result0 = match "foo":
  case "baz":
    "we matched baz"
  case "foo":
    "we matched foo"
  case _:
    "hmmm, didn't match"

result1 = match "foo":
  case "f${rest}":
    "we start with f followed by ${rest}"
  case _:
    "hmmm, didn't match"

result2 = match ["foo", "bar"]:
  case ["f${rest}", "baz"]:
    "this won't match"
  case ["f${rest}", *_]:
    "we start with f followed by ${rest}"
  case _:
    "hmmm, didn't match"

result3 = match [False, True, True]:
  case [*_, True, *_]: "at least one is true"
  case _: "all items are false, or the list is empty"

result4 = match [False, True, True]:
  case [*_, True, *tail]:
    match tail:
      case []: "True with tail empty"
      case [True]: "True with tail == [True] (this branch matches)"
      case _: "True with something else"
  case _: "all items are false, or the list is empty"

Match and recur branches can also have guards:

result5 = match Some(1):
  case Some(v) if v.eq_Int(0): "zero"
  case Some(v): "non-zero ${int_to_String(v)}"
  case None: "none"

Guards run after the pattern matches, in the same scope as the pattern bindings. The guard expression must have type Bool. If the guard is False, matching continues with the next branch. This works the same way in recur blocks. For totality checking, only unguarded branches count as covering cases, so guarded branches still need an unguarded fallback. Syntax note: write at least one space between the pattern and if.

A common shorthand for checking if something matches is:

long = match ["foo", "bar"]:
  case ["foo", *_]: True
  case _: False

short = ["foo", "bar"] matches ["foo", *_]

matches can also take a guard:

is_even = x -> x.mod_Int(2).eq_Int(0)
contains_even = [1, 2, 3] matches [*_, x, *_] if is_even(x)

Any names bound by the pattern are only in scope inside that guard. They are not available after the matches expression itself.

This also works with ternary syntax without extra parentheses:

result = xs matches [*_, x, *_] if pred(x) else fallback

This is equivalent to True if (xs matches [*_, x, *_] if pred(x)) else fallback, so names from the pattern are available in pred(x) but not in fallback. If the guard itself is another guarded matches, add parentheses around the inner expression to make the grouping explicit.

Patterns can bind the matched value with as:

case Some(v) as whole: whole
case [*_, 4 as four]: four

Patterns can also be annotated with types using pattern: Type:

case (_: Int) as last: last

These annotations only guide type inference; they are not runtime checks. Bosatsu has no runtime type checks—types are fully determined at compile time.

In string patterns, ${name} binds a substring and $.{name} binds a single Char. Use _ to ignore the matched part:

case "${_}$.{c}": c

List patterns support “globs” using *. *_ matches any (possibly empty) sublist, and *name binds that sublist. Globs can appear anywhere in the list:

case [*_, True, *_]: "contains True"

A key feature of Bosatsu pattern matching: at least one branch must match. The compiler will check this and fail to compile any code that could fail to match at runtime. The error will list the branches that are not covered.

Custom Data Types

All type names start with an uppercase character. We can think of a definition as two things:

1. defining a new type
2. defining a set of constructor functions to create that type

Structs

In the case of a struct, there is a single constructor function that can take a number of arguments which we can think of as fields to the struct. The constructor function has the same name as the type for structs.

struct HashResult(as_string: String)

struct File(name: String, modified_time: Int, size: Int, hash: HashResult)

There are two ways to create a struct or enum value: by treating it as a function or as a named record. The analogy you can think of is that structs are either named tuples, or named dictionaries

my_file = File("readme.txt", 1540951025, 10240, HashResult("b9f32037daab5a0aff8e437ff1dd0f0d"))

# same using record syntax
my_file_rec = File {
  name: "readme.txt",
  modified_time: 1540951025,
  size: 10240,
  hash: HashResult("b9f32037daab5a0aff8e437ff1dd0f0d")
}

You can only use one syntax: all unnamed tuple-like, or all names dict-like.

Struct and enum constructors may declare default values on fields:

struct Rec(a: Int, b: Int = 10)

Defaults are only applied when using record syntax (Rec { ... }), and only for omitted fields. Positional constructor calls (Rec(...)) do not fill defaults.

Two rules apply to constructor defaults:

1. A field with a default must have an explicit type annotation.
2. A default expression may only reference imports, or top-level values defined earlier in the same file (including earlier defaults). It may not reference constructor parameters, including earlier parameters.

If all required fields are defaulted, Rec {} is valid and means “construct using defaults.” This is different from Rec by itself: bare Rec refers to the constructor value (and only behaves like a zero-argument construction for truly zero-argument constructors). Rec() is not constructor syntax.

Like Rust, if a value is already in scope matching a field name, we can omit the colon:

name = "readme.txt"
size = 10240
hash = HashResult("b9f32037daab5a0aff8e437ff1dd0f0d")

my_file_rec = File { name, modified_time: 1540951025, size, hash }

Record syntax also supports updates from an existing value:

base = File {
  name: "readme.txt",
  modified_time: 1540951025,
  size: 10240,
  hash: HashResult("b9f32037daab5a0aff8e437ff1dd0f0d"),
}

smaller = File { size: 4096, ..base }

In File { size: 4096, ..base }, explicitly listed fields override values from base, and omitted fields are copied from base.

Rules for record updates:

1. They are written with ..expr in record construction syntax.
2. ... is only for patterns (not construction).
3. You must explicitly set at least one field.
4. At least one field must be copied from the base expression.
5. Updates are supported on single-constructor types (for example, structs).

There are no methods in Bosatsu, only functions. We cannot define methods on structs or enums. The only thing we can do with a struct or enum is match it:

nm = match my_file:
  case File(name, _, _, _): name

# same as the above but ignoring trailing fields
nm = match my_file:
  case File(name, ...): name

# same as the above but using records
nm = match my_file:
  case File { name: n, ... }: n

# same, but omit the colon to bind the field name
nm = match my_file:
  case File { name, ... }: name

All matches in Bosatsu are total: one of the branches must match. We support destructuring style syntax when matches are total:

File(nm, ...) = my_file

# or using record syntax to bind the name to nm
File { name: nm, ... } = my_file

# or using short record syntax binding name below this call
File { name, ... } = my_file

as a synonym for the above code.

In the above we have added a type annotation for each field. If we omit a type annotation, we assume any type will do so we create a new type parameter. If we need to have alignment in two type parameters, we need to explicitly name them:

# Here is a Tuple with 2 items of *any* type
struct Tuple2(fst, snd)

num_str = Tuple2(1, "1")

# Here is a Pair: both have the same type:
struct Pair(fst: a, snd: a)

neg = Pair(1, -1)

Sometimes it is important to assign type parameters in a specific order. In those cases we can manually write them:

# put the right side type parameter first, otherwise, we would have gotten b
# first in left to right order.
struct Tuple[a, b](fst: b, snd: a)

Types are assigned left to right when they are omitted.

Limited Recursion in Custom Data Types

Types must form a directed acyclic graph (DAG) with the exception that they may refer to themselves in covariant positions (i.e. not in the inputs to functions).

An example of a type that does not refer to itself in a covariant position is:

struct W(fn: W[a, b] -> a -> b)

Here W is in scope inside the definition of W. The types, like packages, must form an acyclic graph. If we allow types like the above, we open the door to recursion at the value level since we allow the Y-combinator to be typed. By banning some recursive types, the type of fix-point combinators becomes infinite, and thus ill-typed. This restriction is currently required to preserve totality in Bosatsu (a more advanced language can allow more recursion that it can prove does not violate totality).

An important recursive type we can write is List. In Predef we will find a standard linked list:

enum List:
  EmptyList, NonEmptyList(head: a, tail: List[a])

Data-structures have two simple rules:

1. they must form a DAG
2. if they refer to themselves, they do so in covariant positions (roughly, not as inputs to functions).

Tuples

A built-in family of structs are tuples, which you can think of as either lists with potentially a different type in each position and a statically known size, or as an anonymous struct. We write and match them exactly as you might imagine:

x = (1, "2", ["three"])
# this match is total, so we can do a destructuring assignment:
(a, b, c) = x
# or we can use match syntax if that is more appropriate
match x:
  case (x, y, z): do_something(x, y, z)

The 0-arity tuple is written () and has type Unit. Tuples are also real predef types and can be named explicitly as Tuple1 up to Tuple32 (there is no Tuple0; Unit fills that role), with fields item1, item2, and so on. That lets you select parts of a tuple using record-style patterns:

Tuple3 { item2, ... } = (1, 2, 3)
# now item2 = 2

This pattern is handy when you only need specific tuple positions.

Enums

While struct represents a named tuple or product type, an enum represents a named sum type. This is something similar to union in C, sealed trait subclasses in Scala, or its namesake enum from Rust. Perhaps the most famous example is below:

enum Option:
  None, Some(get)

In this example, we have omitted the type for get, so it can be any type. There is thus one type parameter on Option because Some requires it.

Consider if we want a type to be the same on two branches: we just use the same type parameter name. There is only one namespace per enum for such variables:

enum GoodOrBad:
  Bad(bad: a), Good(good: a)

In the above example, GoodOrBad has a single type parameter a. So Bad(1) and Good(1) are of the same type.

Pattern Matching on Custom Types

As we have already seen examples of, Bosatsu features powerful pattern matching. Literal values, such as integers or strings, as well as lists and tuples can appear in pattern matches. Patterns can be nested and combined in unions. There is a special wildcard term that can appear in a pattern match that is written as _. The wildcard matches everything but introduces no new bindings.

One restriction is that all match expressions in Bosatsu must be complete matches. It is a compilation error if a pattern match can fail. Remember, Bosatsu is a total language, so we must check for match totality in order to preserve totality of our functions.

Here are some examples of pattern matches:

enum Either: Left(a), Right(b)

match x:
  case Left(Left(Left(_)) | Right(_)): 0
  case Left(Left(Right(_))): 1
  case Right(_): 2

match y:
  case Left(Left(x)) | Right(x):
    # here we require that the bindings in the left and right sides of
    # the union are the same and that they have the same type
    Some(x)
  case Left(Right(_)): None

# if we can write a match in a single arm, we can write it as a binding:
Left(x) | Right(x) = y

Types

Type variables are all lower case. There is an explicit syntax for function types: a -> b for Fn1. For higher arities, use tuple-style argument lists: (a, b) -> c for Fn2, (a, b, c) -> d for Fn3, and so on.

To write a function that takes a tuple as its single argument, use an extra layer of parentheses in both values and types. For example:

# Fn1 taking a tuple
add_tuple: ((Int, Int)) -> Int = ((x, y)) -> add(x, y)

There is support for universal quantification sometimes called generic values or generic functions: forall a. a -> List[a].

Kinds and variance annotations

You can annotate type parameters with kinds and variance. * is the kind of value types, and * -> * (or higher) are type constructors. Variance markers +* and -* mark covariant and contravariant parameters:

enum NEList[a: +*]: NEOne(head: a), NEMore(head: a, tail: NEList[a])
struct Box[a: *](value: a)
def map[f: * -> *, a, b](fa: f[a], fn: a -> b) -> f[b]: ...
def wrap2[shape: (* -> *) -> *](s: shape[List]) -> shape[List]: s

For struct/enum definitions, kinds are inferred. For functions, kinds are not currently inferred; unannotated type parameters are assumed to be *.

Existential types

Bosatsu also supports existential quantification to hide a type parameter chosen by the producer of a value. The syntax is exists a. ..., and you can quantify multiple variables with commas, e.g. exists a, b. ....

Here is a simple example that stores an internal type but keeps it opaque in the public constructor:

enum Build[a: *]:
  Mapped(consume: exists b. (Build[b], b -> a))
  Map2(consume: exists b, c. (Build[b], Build[c], (b, c) -> a))

When you pattern match on a constructor that contains an existential, the hidden type is scoped to that branch, so the parts that depend on it stay consistent:

enum FreeF[a]:
  Pure(a: a)
  Mapped(tup: exists b. (FreeF[b], b -> a))

def run[a](fa: FreeF[a]) -> a:
  recur fa:
    case Pure(a): a
    case Mapped((prev, fn)):
      fn(run(prev))

When to use existentials:

• To hide intermediate types in data constructors while still allowing later consumption (e.g. Mapped/Map2 store an internal b or c plus functions that know how to use them).

• To model heterogeneous or stateful structures where the internal type varies but is not part of the public API (e.g. existential tails in custom list-like structures, or continuations with hidden state).

• To return or store values that must remain opaque to callers while keeping internal consistency inside a match branch.

The Bosatsu Predef

The predef includes Int, String, List, Option, Either types and some associated functions. It also defines the built-in test types Assertion and TestSuite.

Packages

All names are private unless exported. All names from external packages must be imported. There can be no cycles in the dependency graph of Bosatsu packages.

package Animals/Favorites
export mammals, birds

mammals = ["elephant", "whale", "dog"]

birds = ["African grey parrot", "macaw"]

In some other package:

package Animals/Report

from Animals/Favorites import mammals
export most_fav

most_fav = match mammals:
  case [head, *tail]: head
  case []: "who knows?"

You can group imports/exports with parentheses and rename with as:

from Bosatsu/Predef import (foldl_List as foldl, add as operator +)
export (foldl)

We export types slightly differently. We can export just the type, or the type and the constructors. To export the type and the constructors use Type() whereas Type exports only the type to be visible.

package Great/Types

export ClearOption(), OpaqueOption, foldO, noneO, someO

enum ClearOption:
  CNone, CSome(get)

enum OpaqueOption:
  ONone, OSome(get)

noneO = ONone
def someO(a): OSome(a)

def foldO(oo, if_none, if_some):
  match oo:
    case ONone: if_none
    case OSome(a): if_some(a)

Here ClearOption exports all its constructors so they can be pattern matched upon. In the OpaqueOption example, we export functions to create the opaque option, and a fold function to tear it down, but we can’t explicitly pattern match on the types.

Sometimes such opacity is useful to enforce modularity.

Value usage requirements

Bosatsu requires top-level values to be used. A top-level value must be transitively reachable from at least one of these roots:

1. an exported value
2. the package main value (the last top-level value in the package)
3. the package test entry:

• if no Bosatsu/Prog::ProgTest exists, the last top-level Bosatsu/Predef::Test
• if one or more ProgTest values exist, the last top-level ProgTest

If a top-level value is not reachable from any of those roots, compilation fails with an unused-value error.

This rule is intentional. Unused names are often caused by typos, mistaken refactors, or dead code that is no longer needed. Requiring explicit reachability adds a small amount of friction that catches these issues early.

When you intentionally want to evaluate/check something and then discard it, bind it to _:

_ = some_expression

That makes the intent explicit to readers and to the compiler.

Type-check-only todo

When iterating on larger changes, you may know the arguments you need but not yet know the final implementation. In check-only mode, Bosatsu includes:

def todo[a](a: a) -> forall b. b

todo consumes a value (often a tuple of values you plan to use) and can stand in for any return type so the rest of your code can still typecheck:

def big_hard_function(a: Arg1, b: Arg2) -> Result:
  todo((a, b))

This is useful for an “always-be-compiling” workflow: keep moving from one typechecking state to the next, then remove placeholders incrementally.

todo is intentionally unsound, so it is only available in check-only commands (tool check and lib check). Commands that emit or execute outputs (show/json/eval/build/transpile/test) do not include todo, so those commands fail until all todo calls are removed.

Testing

Bosatsu supports two test entrypoint styles:

1. Plain tests as values of type Bosatsu/Predef::Test
2. Effectful tests as Bosatsu/Prog::ProgTest

Bosatsu/Predef defines:

1. Assertion(value: Bool, message: String)
2. TestSuite(name: String, tests: List[Test])

Common patterns in test_workspace/*.bosatsu:

1. A single assertion:

   test = Assertion(eq_Int(add(1, 1), 2), "1 + 1 == 2")
   

2. A suite of assertions:

   tests = TestSuite("math tests", [
     Assertion(eq_Int(add(1, 2), 3), "1 + 2"),
     Assertion(eq_Int(mul(3, 4), 12), "3 * 4"),
   ])
   

3. Nested/composed suites, including generated tests:

   tests = TestSuite("all tests", [
     unit_tests,
     TestSuite("generated", [mk_test(i) for i in range(10)]),
   ])
   

Bosatsu/Prog defines:

1. ProgTest(test_fn: List[String] -> forall e. Prog[e, Test])

Test discovery rules (tool test and lib test) are:

1. If no ProgTest exists, run the final top-level Test value in source order.
2. If one or more ProgTest values exist, run the final top-level ProgTest value in source order.
3. If any plain Test value appears after that selected ProgTest, test discovery fails for that package with an ordering error.

Current argument behavior: runners pass [] into ProgTest.test_fn.

From the repo root, run tests with:

./bosatsu lib test

When iterating, you can run only matching package tests with a regular expression filter:

./bosatsu lib test --filter "MyLib/.*"

--filter matches package names and can be provided more than once.

Purity, Effects, and Prog

Bosatsu expressions are pure: evaluating Bosatsu code does not directly read stdin, write stdout, mutate state, or throw exceptions.

Instead, effectful behavior is represented as data using Prog[env, err, a]. When you write I/O-heavy code, you are building a program description inside Bosatsu. That description can be transformed and composed (for example with map, flat_map, or await-style syntax), but it is not executed by Bosatsu itself.

Execution happens only when a runtime is given a Main program entrypoint. In other words, Bosatsu builds the effectful program, and the runtime executes it.

This is the same core idea used in pure functional programming (for example, Haskell IO or Scala cats.effect.IO): represent effects explicitly and keep core language evaluation pure. Bosatsu goes further by not exposing a general in-language escape hatch to “unsafely run” a Prog immediately.

You can think of Bosatsu as a pure language for constructing executable programs with effects at the boundary. The goal is practical usability with strong safety: if pieces typecheck, they can be composed with confidence.

For benchmarks, Bosatsu/Prog also exposes:

1. observe[a](a: a) -> forall err. Prog[err, Unit]

observe is an effectful consume barrier. It only runs when sequenced into an executed Prog (for example inside Main or ProgTest via await/flat_map). If you call observe but never execute that Prog, it has no effect.

Bosatsu/Prog also exposes Var[a] for effectful mutable cells. Allocate a cell with new_var, read with get, transform atomically with update, and write with either set or swap. The return values differ:

1. set(v, next) stores next and returns ().
2. swap(v, next) stores next and returns the previous value.

External functions and values

There is syntax for declaring external values and functions, but regular Bosatsu library code cannot define new externals today.

At the moment, external defs are only allowed in trusted libraries implemented inside the bosatsu compiler repository. This is intentional: Bosatsu is designed for safe composition, and if any dependency could hide unsafe behavior, that safety story gets much weaker.

So “use with caution” mostly applies to maintainers of trusted runtime/predef code, not to ordinary Bosatsu library authors.

Bosatsu allows recursion on Int when the recursion checker can prove that on recursive paths (for example under cmp_Int(int_v, 0) matches GT), the next recursive argument is still non-negative and strictly smaller than the current value. For tail recursion, use loop:

def int_loop(int_v: Int, state: a, fn: (Int, a) -> (Int, a)) -> a:
  loop int_v:
    case _ if cmp_Int(int_v, 0) matches GT:
      (next_i, next_state) = fn(int_v, state)
      if cmp_Int(next_i, 0) matches GT:
        if cmp_Int(next_i, int_v) matches LT:
          int_loop(next_i, next_state, fn)
        else:
          next_state
      else:
        next_state
    case _:
      state

External values and types work exactly like internally defined types from any other point of view.

External defs are only supported in libraries implemented inside the compiler repo. The functions must be implemented in the C runtime, and there is currently no provision for providing external implementations from outside the compiler repo. This restriction is intentional to preserve totality, and we do not expect to lift it any time soon.

Because these externals are trusted code, each external def included with the compiler is reviewed and tested carefully to avoid breaking sound typing. This is the central safety goal: if a program typechecks, running it should not produce a value that violates its type.

In the future, we may consider an explicit unsafe boundary (similar in spirit to Rust unsafe) where external defs and calls are marked and that annotation is propagated through callers. That would make the safety/power trade-off explicit. Our bias is strongly toward safety; if you want maximum unrestricted power, this is likely not the right language.

Note on Totality

Totality is an interesting property that limits a language from being turing complete, however, it is not obvious if that is much of a practical limit. People often criticize fully general languages for configuration, but it is not clear that non-termination or partial functions are the problems.

One can easily argue that total languages are still too big. For instance imagine a function with type a -> Either[a, b] which takes an a and either returns a final b value or the next step a that we should call again. If we have a non-total language we could repeatedly call the function when we have left to build a -> b. In a total language, we could build a

def repeat(n: Int, fn: a -> Either[a, b]) -> (a -> Either[a, b])

to repeat n times the fn unless we find a b and build a function of the same type that loops more times. By repeatedly applying this function: repeat(1000, repeat(1000, ... repeat(1000, fn)... we can make an exponentially large number of attempts. So we could easily build a function that would take 2^128 attempts which would take longer than the life of the sun to complete. Is this meaningfully different from an infinite loop?

Our view is that the first goal is a sound type system we can trust. Totality is one important tool for that goal: it helps ensure evaluation produces values of the declared type instead of getting stuck in partial behavior. Termination by itself is not a performance guarantee, since terminating programs can still be exponentially expensive. Therefore, the only possible runtime failure for well-typed pure Bosatsu code is exhausting memory, which is a risk in virtually every programming language.