Soliton

A compiler that argues back.

Soliton is a small statically-typed language that compiles to native machine code through LLVM. It has ownership and moves, generics and modules — and it will not let you add metres to seconds.

trip.sn
unit meters;
unit seconds;

pub fn speed(distance: float<meters>, elapsed: float<seconds>)
        -> float<meters/seconds> uses nothing
    requires elapsed > 0.0<seconds>
{
    return distance / elapsed;   // the unit falls out of the division
}

pub fn main() {
    let total = 1500.0<meters> + 300.0<seconds>;
}
the compiler's reply
$ soliton check trip.sn
error: cannot apply `+` to `float<meters>` and `float<seconds>`
 --> trip.sn:12:17
  |
12 |     let total = 1500.0<meters> + 300.0<seconds>;
  |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the operands have different types
  = note: `+` needs the same unit on both sides (§10.2)

error: aborting due to 1 previous error

Get it

Download and run. Nothing else to install.

The compiler carries its own linker and ships every archive it links against, so it works on a machine with no compiler, no LLVM and no MSYS2 on it. The programs it produces import nothing Windows does not already have.

Download for Windows 56 MB · zip
Soliton 0.1.0 · Windows 10 or later, 64-bit. Unzip anywhere and run bin\soliton.exe.
Checksums are on the release page.

What is unusual about it

Three things the type checker knows that most do not.

The rest of Soliton is deliberately ordinary — structs, methods in impl blocks, generics by monomorphization, ownership with moves and no garbage collector. These three are the reason to look.

§10.1 — Contracts

What a function expects, in its signature

A precondition is what the caller owes; a postcondition is what the function owes back, with result naming the value on its way out. Both are checked at run time, and a violation names the clause rather than returning a wrong answer that surfaces an hour later.

pub fn divide(a: int, b: int) -> int
    requires b != 0
    ensures result != 0 || a == 0
{ return a / b; }

$ soliton run divide.sn
soliton: requires contract violated in `divide`: b != 0
  --> divide.sn:2:5

§10.2 — Units of measure

Metres are not seconds, and the compiler agrees

+ and - require the same unit on both sides. * and / combine them algebraically, so dividing a distance by a time produces a speed without anyone declaring one. It costs nothing at run time: a float<meters> is a double, and the generated code is identical to the same program written without units.

let rate: float<meters/seconds^2> = d / t / t;  // an acceleration
let back: float<meters>           = speed * t;  // and back again
let ratio: float                 = d / d;      // cancels to a number

§10.3 — Effects

What a function is allowed to do

uses nothing means a function may not print, and the check is transitive — calling something that prints counts, however many calls away. A function with no clause has no bound, which is why adding effects to an existing program breaks nothing.

pub fn quiet(w: int) uses nothing { println(w); }

error: `io` is not permitted here
 --> effects.sn:1:33
  |
1 | pub fn quiet(w: int) uses nothing { println(w); }
  |                                     ^^^^^^^^^^ this performs `io`
  = note: `quiet` is declared `uses nothing`

Before you build on it

What Soliton does not do.

Soliton is one person's language at version 0.1. It compiles real programs and the test suite is thorough, but it has sharp edges that are documented rather than hidden.

References are unchecked. There is ownership and there are moves, but no borrow checker — a &T outliving what it points at is a use-after-free that nothing diagnoses. That is a deliberate design choice, not a bug queue.

  • No GCOwnership and moves, with drops inserted by the compiler.
  • No borrow checkerSee above. This is the one to weigh.
  • Self-hostingNot yet — the compiler is C++20 and LLVM.
  • Everything elseThe known limitations list runs to fifteen entries, each with its reasoning.