Souther

Model the rule, not its accidental implementation

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
    }

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

error E1002:
Behavior `changeEmail` constructs `Member`
but does not declare `constructs Member`.

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 `?`.

Examples make rules executable—and reveal what is missing

An example sits next to the behavior it describes and is evaluated during compilation. If the behavior stops agreeing with it, the build fails. souther examples additionally reports coverage gaps. The example is executable documentation rather than a separate test model that can drift from the rule.

They are written where the rule is, so the threshold that decides PricedCart from EmptyCart is readable beside the code that implements it — the documentation and the check are the same text. Its report also identifies untested output cases, decision boundaries, and partitions. A gap is not just a coverage number: it is the next question to ask of the domain.

example quote
    | "all lines valid -> a priced cart" :
        (Cart { open = true, items =
            [ LineItem { sku = Sku("apple"), quantity = 2, unitPrice = 150 } ] })
        -> PricedCart { items =
            [ LineItem { sku = Sku("apple"), quantity = 2, unitPrice = 150 } ]
            , total = 300, highValue = false }
    | "a closed cart -> empty" :
        (Cart { open = false, items =
            [ LineItem { sku = Sku("apple"), quantity = 2, unitPrice = 150 } ] })
        -> EmptyCart

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, Path.ROOT)) {
            case Ok<Member> ok   -> ok.value();
            case Err<Member> err -> CorruptRecord();  // inherited factory
        };
    }
}

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 backend generates legal Java identifiers underneath.

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, and calling an arbitrary JVM method is E1401.

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. --format json emits the same diagnostic as structured data for tooling.

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.

error E1001:
Data `Email` cannot be constructed directly.
Use `Email.decoder` or a behavior declared with `constructs Email`.

error E1201:
Non-exhaustive match for data `TripRequest`.
Missing case: PreApproved

error E1302:
Exceptions are not supported.
Return a failure case in the output sum.

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. 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.

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

The compiler, runtime, CLI, language server and VS Code extension are open source. The extension gives semantic highlighting, hover, go-to-definition and inline diagnostics over the same diagnostics the CLI emits, and souther-fmt formats sources to a single layout.

Start with a single self-contained file: souther run decodes JSON input, runs an exposed behavior with no external dependencies, and prints JSON output. When the model is ready to integrate, souther compile generates Java 25 class files; Java supplies the database, clock, HTTP client, and other infrastructure through declared behaviors.

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.

View the source on GitHub·See the business trip example