Souther

Each decision is one line the compiler checks

Invalid values have nowhere to hide

A constraint is declared next to the type it belongs to, once. Souther checks it wherever the value is constructed — a derived decoder at the boundary, or a behavior inside the domain.

The generated constructor is not public to Java, so no code path skips the check. A value of type Balance that exists is a value that satisfied value >= 0.

data AccountNo = String
    invariant String.length(value) > 0

// The withdrawal amount is non-negative.
data Amount = Int
    invariant value >= 0

// A balance never goes below zero.
data Balance = Int
    invariant value >= 0

States share their fields instead of repeating them

Draft and Submitted are distinct types. A behavior that takes a Submitted cannot be handed a Draft, and the difference between the two is the one field that actually differs.

They still share a single definition of what a trip request is. Adding a field to TripRequestFields reaches both, and a spread that collides with an existing field name is a compile error rather than a silent override.

data TripRequestFields =
    { requester: EmployeeId
    , plannedCost: Amount
    }

data Draft =
    { ...TripRequestFields
    }

data Submitted =
    { ...TripRequestFields
    , submittedAt: String
    }

The compiler says which example is missing

An example sits next to the behavior it describes and runs on every compile. A row that stops holding fails the build, so the documentation and the check are the same text.

souther examples then reads the behavior’s own rules and asks what the rows leave untested. The two rows in the hero model cover both outcomes, and the report still finds three gaps: nobody has stood on the 100000 threshold, one step past it, or on the zero that Amount allows. A gap is not a coverage number. It is the next question to ask the business.

trip                                        measurement: complete
  submit            implemented   rows 2    pending 0
    signature   out specified 2/2  observed 2/2  verified 2/2
    partition   axes 1   equivalence partitions 2/2
    border      borders 2   obligations 3/5
      ! no row is at the ON point (comparison@15:37)
          · read as submit/request.plannedCost: = 100000
      ! no row is at the OFF point (comparison@15:37)
          · read as submit/request.plannedCost: = 100001
    branch      2/2
    decision    rules 2   taken 2
  declarations   obligations 0/1
  Amount
      ! no row is at the ON point value = 0 (invariant Amount #1)

adequacy: not satisfied
3 gaps marked `!`: what a strict build refuses over.

The gaps drive the model

--generate writes the missing rows with the inputs filled in and the answer left as <?>. Filling one in means asking what the rule says at 100000 exactly, and at 0. Sometimes the answer is a value. Sometimes it is a new outcome the model did not have, a state that needs its own type, or a threshold the business has never written down.

That loop is how a Souther model is built: write the operations you know, write the examples you have, read what the report says is missing, and refine the types until every row is answered. The tutorial grows a whole approval workflow this way, and --strict turns the last report into a build that refuses to ship with a question open.

souther examples trip.sou --generate

example submit
    | (DraftRequest { plannedCost = Amount(100000) }, "x") -> <?>
    | (DraftRequest { plannedCost = Amount(100001) }, "x") -> <?>
    | (DraftRequest { plannedCost = Amount(0) }, "x")      -> <?>

A rejection is domain data, not an exception

Everything a withdrawal can end up as is listed in its type. InsufficientFunds is ordinary data: no Result wrapper, no error base class, no exception, no marker distinguishing it from the success case.

Which of these is a “failure” is not decided here. It is decided by what the next stage in a pipeline accepts — so the same case can be a failure in one composition and a normal outcome in another.

data Withdrawn =
    { account: AccountNo
    , newBalance: Balance
    }
data InsufficientFunds = { shortfall: Int }
data NoAccount

behavior withdraw : (request: WithdrawRequest)
    -> Withdrawn | InsufficientFunds | NoAccount

Who is allowed to create this value

A behavior’s construction authority is explicit. A behavior with a let may state the data it builds in constructs; if it omits the clause, Souther infers the set from its body. When the clause is written, building an undeclared value is E1002 and declaring a value it never builds is E1006. An injected behavior must declare its construction set.

Both directions are checked, so an explicit clause is an accurate account of what a behavior brings into existence and what it merely passes through. Combined with non-public constructors, the set of places a Submitted can come from is a list you can read.

behavior submit : (request: Draft, submittedAt: String)
    -> Submitted | Rejected
    constructs Submitted, Rejected

-- INSUFFICIENT CONSTRUCTION AUTHORITY  E1002 -member.sou:4:1

4| behavior changeEmail : (name: String) -> Member | Rejected
   ^

Behavior `changeEmail` constructs `Member` but does not declare `constructs Member`.
Hint: Add `constructs Member` to `changeEmail`, or stop constructing Member here.

A guard names the outcome it produces

guard states the condition for continuing and says what the behavior becomes when it does not hold. There is no early-return convention to learn and no exception to catch.

It also carries information forward. Below the guard, the compiler knows the balance covers the amount, and that discharges Balance’s invariant value >= 0 on the next line. The invariant is still checked at construction time; an unguarded violation is a model bug and aborts rather than producing a business outcome.

let withdraw (request, currentBalance, updateBalance) =
    match currentBalance(request.account) with
        | NoAccount          -> NoAccount
        | Balance as current -> {
            guard current.value >= request.amount.value
                else InsufficientFunds {
                    shortfall = request.amount.value - current.value
                }
            updateBalance(
                request.account,
                Balance(current.value - request.amount.value))
          }

Illegal states are not representable

An address is either activated or not, and notifications may only go to an activated one. Written as a boolean flag, that rule lives in whoever remembers to check it. Written as a sum, it lives in the argument type of notify, and an unactivated address cannot be passed at all.

match is exhaustive. Add a third case to Email and every match over it stops compiling with E1201, naming the case you have not handled.

data Activated = EmailAddress
data Unactivated = EmailAddress
data Email = Activated | Unactivated

behavior notify : (to: Activated, subject: String) -> Sent
    constructs Sent

// Nested newtypes are destructured in one step.
let addressOf (m: Email) =
    match m with
        | Activated(EmailAddress(s))   -> s
        | Unactivated(EmailAddress(s)) -> s

There is no null

Absence is a field written with ?, opened with Option. Writing null is E1301, not a runtime surprise.

Recursion over an optional field is how a self-referential model is walked: manager is Employee?, so the chain terminates at the person who has none. The compiler accepts the recursion because each step goes strictly inward.

data Employee =
    { id: EmployeeId
    , manager: Employee?
    }

// How many approval levels sit above this person.
let approvalDepth (e: Employee): Int =
    e.manager
        |> Option.map(m -> approvalDepth(m) + 1)
        |> Option.withDefault(0)

error E1301:
`null` is not part of the language. Use an optional field with `?`.

A module boundary is a contract

The public part of a module is stated with exposing, and imports name every dependency they use. For a composed behavior, its public output cases are declared too. This prevents a change inside one module from silently changing the contract seen by another module or by Java.

The model therefore has a deliberate boundary before it reaches application code: implementations may evolve, but a public business contract changes only when its declaration changes.

module example.order exposing (
    placeOrder : OrderPlaced | InsufficientStock
)

import example.stock ( reserve )

behavior placeOrder = reserve >-> recordOrder

Serialization is derived, not written

From the data declaration Souther derives decoders for bare maps, JSON and database rows, plus the matching encoder. You do not write them, and they cannot drift from the model.

The invariant runs during decode, so malformed input from outside the boundary becomes a Result failure with the path that broke — not a bad value that entered the domain and surfaced three layers later.

// generated for an exposed data
public static Decoder<Map<String,Object>, Member> decoder()
public static Decoder<JsonNode, Member>          jsonDecoder()
public static Decoder<Record, Member>            recordDecoder()
public static Encoder<Member, Map<String,Object>> encoder()

// a newtype encodes to a bare scalar
public static Encoder<MemberId, String> encoder()

Dependencies on the outside world are declared, not implemented

A behavior with no let has no implementation in Souther. Java supplies one. depends on names every injected dependency a behavior uses, and over-declaring is E1603 just as under-declaring is an error.

So which functions touch the database is read from the declaration rather than inferred from a package name. This is the part usually left to a layering convention; here it is a clause the compiler checks.

// injected: implementation comes from Java
behavior currentBalance : (account: AccountNo)
    -> Balance | NoAccount

behavior updateBalance : (account: AccountNo, newBalance: Balance)
    -> Withdrawn
    constructs Withdrawn

behavior withdraw : (request: WithdrawRequest)
    -> Withdrawn | InsufficientFunds | NoAccount
    depends on currentBalance, updateBalance

Composition routes by type

>-> passes a stage only the cases the next stage can accept. Everything else leaves the mainline and is collected into the composition’s output, skipping the remaining stages.

Nothing is marked as an error. Which case departs is decided by what the next stage takes, so the same sum composes one way here and another way there. The compiler folds the result and tells you the output type of the whole pipeline.

behavior lookupAndFormat = findMember >-> formatMember

f : A -> B | R     g : B -> C          f >-> g : A -> C | R
f : A -> B | R     g : B -> C | S      f >-> g : A -> C | S | R
f : A -> B1 | B2   g : B1 | B2 -> C    f >-> g : A -> C

Java receives a shape it can exhaust

An output such as -> Member | NoMember | CorruptRecord becomes a sealed interface, so Java switches over it and the compiler catches a missing case.

The Java implementation of an injected behavior extends a generated abstract class and builds failure cases through inherited protected factories. The data constructor stays non-public, so Java can read a Member it has no way to forge — and a platform failure such as a dropped connection stays an exception, distinct from a business outcome.

public final class JdbcFindMember extends FindMember {
    @Override
    public FindMemberResult apply(MemberId id) {
        // ...
        return switch (Member.decoder().decode(raw)) {
            case Ok<Member>(var member) -> member;
            // an inherited protected factory
            case Err<Member> _ -> CorruptRecord();
        };
    }
}

The business speaks its own language, and so can the model

Identifiers are Unicode. When the rule is discussed in Japanese, the type can be named 金額 and the behavior 提出する. The name reaches the class file as it was written, so Java code calls 提出する by that name.

The point is not the character set. It is that the term in the rulebook and the term in the type system are the same string, so there is no glossary mapping 予定費用 to plannedCost for someone to get wrong.

data 金額 = Int
    invariant value >= 0

data 却下 = { 理由: String }

behavior 提出する : (申請: 申請準備中, 提出日時: String)
    -> 提出済み | 却下
    constructs 提出済み, 却下

let 提出する (申請, 提出日時) = {
    guard 申請.予定費用.value <= 100000
        else 却下 { 理由 = "high_cost" }
    提出済み { ...申請, 提出日時 = 提出日時 }
}

The domain cannot reach the outside world

Not “should not” — cannot. There is no syntax for reading a clock, opening a socket or mutating a field. A Java class named in an expression is not a JVM call; it is a name that is not in scope, E1023.

Everything that touches the world arrives as an injected behavior named in depends on. A domain computation therefore depends on its inputs and nothing else, which is what makes an example evaluable at compile time in the first place.

Absent from the language:

  mutable variables      files
  field assignment       network
  static mutable state   threads
  random                 exceptions
  current time           reflection
  environment variables  arbitrary JVM calls

The failures are designed

Each compile error has a stable code that identifies it independently of language, with the prose rendered in the locale you select with --lang. --format json emits the same diagnostic as structured data for tooling, and the same diagnostics appear inline in the editor.

The catalogue is part of the specification rather than a by-product of the implementation. E1002 and E1006 are what keep constructs honest; E1603 does the same for depends on.

-- NON-EXHAUSTIVE MATCH  E1201 ----------------trip.sou:8:5

8|     match r with
       ^^^^^

This `match` on data `TripRequest` does not cover every case.
Hint: Add a case for: PreApproved

-- USE OF NULL  E1301 ------------------------employee.sou:5:46

5| let top (id) = Employee { id = id, manager = null }
                                                ^^^^

`null` is not part of the language. Use an optional field with `?`.

{"severity":"error","code":"E1201","file":"trip.sou",
 "region":{"startLine":8,"startCol":5,"endLine":8,"endCol":10},
 "message":"This `match` on data `TripRequest` does not cover every case.",
 "hints":[{"message":"Add a case for: PreApproved"}]}

A narrow language, a firm boundary

Souther has immutable data, algebraic alternatives, constraints, pattern matching and behavior composition. It intentionally omits null, mutable state, exceptions and arbitrary JVM calls. The result is a domain model whose construction paths, business outcomes and dependencies remain visible.

Souther compiles to JVM class files by default. Generated data and behavior types are designed to be used from Java, while Java remains responsible for infrastructure and integration. Souther requires Java 25 or later for both compilation and integration. The same checked program can also be compiled to a WebAssembly module for the browser and other wasm hosts, or to a native shared library with bindings for PHP, Rust and Go.

Business outcomes, invalid boundary input, model bugs, and platform failures remain distinct. A rejection such as InsufficientFunds is a case in a behavior’s output; malformed input is reported by a decoder’s Result; an invariant violation inside the domain aborts; and a database outage is an exception handled at the Java integration boundary. Keeping these categories separate prevents an infrastructure failure or a programming defect from being mistaken for a business decision.

Tooling

Everything is open source: the compiler, the runtime, the command line, the language server, the VS Code extension, and the Maven and Gradle plugins.

Start with a single self-contained file. souther run decodes JSON input, runs a behavior, and prints JSON output. souther examples reports which inputs, boundaries and decision rules the example rows beside a behavior cover, and writes rows for the gaps. souther fmt formats sources to a single layout. When the model is ready to integrate, souther init writes a Maven or Gradle project, and the build plugin compiles .sou files before Java sees them.

The souther binary also answers questions about the language itself. souther doc reads the specification the compiler was built from, souther api prints the standard library’s signatures, and souther mcp serves both to coding agents over the Model Context Protocol.

Built for the part of software that must stay true

Use Souther when a rule deserves more than a comment: prices that cannot be negative, requests that must follow a state transition, or decisions whose outcomes should be understood by the rest of the system.

Install Souther·Follow the tutorial·Browse the examples·View the source on GitHub