Language Zero

Define anything. Exactly.

A total, dependently typed language where compilation is normalization — and runtime errors are impossible by construction.

Get in touch Examples

Zero keywords

No keywords at all — structure alone disambiguates. Nothing is reserved in English, so the language itself is localizable.

Fibonacci.zero

// Structural recursion on the inductive type Nat.
fibonacci(Nat) -> Nat {
    .zero: 0
    .suc(m): m {
        .zero: 1
        .suc(k): add(fibonacci(m), fibonacci(k))
    }
}

$ zero eval 'fibonacci(1000)'
4346655768693745643568852767504062580256466051737178040248172908953655417949051890403879840079255169295922593080322634775209689623239873322471161642996440906533187938298969649928516003704476137795166849228875 (209 digits)

Zero-cost abstractions

Compilation is normalization — abstractions evaluate away to the optimized result. Write against the interface; every instance inherits it.

Optional.zero

// An example Monad conformance — Optional:
Monad<Optional>(
    bind: { opt -> { f ->
        opt {
            .none: .none
            .some(x): f(x)
        }
    }}
)

$ zero eval '.some(3).bind({ x -> .some(multiply(x, 10)) })'
(some 30)

Zero runtime errors

Bad values are ruled out during typechecking.

Text.zero

tag: LowercaseText = "errorLess"

error: 'L' is not lowercase
  tag: LowercaseText = "errorLess"
                             ^
  LowercaseText admits 'a' … 'z' only.

Inside

Dependent types Inductive families Totality Compilation = normalization E-graph normalization Slotted e-graphs Exact arithmetic Real numbers Reflection Levitation Ornaments Type descriptions Quotient types Type-directed compilation Custom representations Effects in types Linearity Metaprogramming Self-representation Language-oriented programming Structural equality Universe hierarchy Keyword-free syntax

Contact

Language Zero is in closed beta. If you build compilers, care about correctness, or want a look inside — reach out.

Enquire