GoForge — Build | Test | Ship | Collaborate GoForge — Build | Test | Ship | Collaborate
v0.146.0

Go+

Richer abstractions, portable Go

$ go install goforge.dev/goplus/cmd/goplus@latest
Source repository pkg.go.dev

Go+ is a language for authoring richer abstractions while emitting portable, idiomatic Go. It is a strict superset of Go: every valid Go file is a valid Go+ file (.gp), and every Go+ construct has a specific Go lowering. Generated packages compile with the standard Go toolchain and are distributed and consumed without Go+ — the interoperability story Kotlin, Scala, and Clojure have with Java.

Current releases — Go+ v0.158.0 / stdlib v0.213.2

The toolchain is at v0.158.0 — the largest release since goml itself. It opens Stage C of the dependent-typing roadmap, dependent matching, gives the railway a single-track sibling in std/option, and closes goml’s surface lag in one tranche. The standard library is at v0.213.2: std/vec now states the impossibility it has always relied on, and its generated Go is byte-identical for it.

Impossible arms (grammar v0.19.0) make pruning statable. Since v0.7.0, a match whose scrutinee’s index rules out a variant has simply not required that arm — correct, and silent. The arm can now be written:

func First[T any](0 n nat, v Vec[T, n+1]) T {
	match v {
	case Cons(h, t):
		_ = t
		return h
	case Nil():
		impossible
	}
}

The claim is checked against the same pruning the checker already performs — index clash under hypotheses, GADT incompatibility — then dropped, so the generated Go is byte-identical to the omitted-arm form: impossible is an assertion, never an instruction. An arm the checker cannot rule out is a compile error naming what could still match. In goml it is a reserved word: | Nil => impossible.

Guards (v0.20.0) arrive in both surfaces at once — case Cons(h, t) if h > limit: and | Cons h t if h > limit =>. A guard is evaluated after its pattern’s bindings, in arm order, and false falls through. The coverage policy is deliberate: a guarded arm contributes nothing to exhaustiveness — the checker does not read your boolean — so a match that leans on guards still names its fallback. Decider-checked guard coverage is scheduled (Stage C continues), not missing.

Literal patterns (v0.21.0) land where they can be checked: scalar scrutinees. And coverage is the decider’s judgment — the same judgment that prunes an impossible variant:

func Name(n nat, 0 p Lt[n, 3]) string {
	match n {
	case 0:
		return "zero"
	case 1:
		return "one"
	case 2:
		return "two"
	}
}

No fallback arm: Lt[n, 3] in scope proves three literals total. Without such a hypothesis the match demands a binder or _ arm; the literals must cover 0..k-1 contiguously, because the decider proves bounds, not disjunctions; and the generated Go still polices the erasure boundary with a panic, because hypotheses are static and plain-Go callers are not. Guards compose with literals, and a duplicate literal is an unreachable-arm error. Literals inside constructor arguments are next in the stage; the diagnostic meanwhile spells the workaround (case Cons(x, t) if x == 0:).

std/option joins the railway. Result has had track-aware pipelines since v0.4.0; Option now gets the single-track version of the same table:

n := option.Some(16) |> half |> strconv.Itoa |> .UnwrapOr("none")

T → Option[U] binds, T → (U, ok) adapts through option.Of, T → U maps, and None bypasses everything. There is deliberately no Tee — an Option carries no error to observe on the side, so a tee stage is refused by name rather than silently skipped. Recognition is nominal, not structural: a type gets railway semantics by being std/option.Option, not by coincidentally naming a method Bind.

goml closes its surface lag — everything the core could do that goml could not spell, plus the ML ergonomics a reader of OCaml, Idris, or Lean expects:

  • Named prop declarations — type InRange (i : Nat) (n : Nat) := prop { And (Le 0 i) (Lt i n) } lowers to the v0.156.0 form, so a goml signature states the precondition by name.
  • Interface declarations — type Clock := interface { Now : Unit -> time.Time; io.Closer } lowers to a native Go interface, and @[delegate] consumes it — a package no longer needs a .gp file just to declare its contract.
  • Conversions, make, record update — Int64 n, make (Chan Int) 4, and { s with Port = p }, which copies then assigns however complex the base expression, evaluated once.
  • Expected types — a signature now threads into its body, so unannotated lambdas (fun x => x * 2) and list literals ([2, 3, 4]) need no spelled types where the signature already says them. A spaced [ is a list, a glued one indexes — ML’s rule.
  • where helpers — where loop (k : Int) (acc : Int) : Int := … lowers to a closed package-private function beside its owner.
  • open result exposing (Ok, Err) — unqualified constructors in expressions and patterns. Only capitalized names may be exposed, and goml binders are lowercase, so shadowing is impossible by construction.
  • User infix operators — infixl 5 <+> := Combine declares precedence and associativity; every use rewrites to an ordinary call at parse time, so the generated .gp — and the differential gate that keeps the two surfaces honest — never sees an operator.

These land under a recorded program: spec/gap-program-design.md in the repo sequences the road from here to the Idris2/Lean4 feature set — dependent matching (now open), totality widening, automation, codata, and the kernel that will make the “dependently typed” claim earnable.

The stdlib’s v0.213.1 told Stage B’s consumer story: its first real consumer is std/vec, whose AtIndex and Set take an ordinary number and carry the bound as a proposition rather than as Fin[n] evidence.

func AtIndex[T any](i nat, 0 n nat, 0 p Lt[i, n], values Vec[T, n]) T

The bound is proved at the call and then erased, so there is no Fin to build and the generated function is an ordinary walk — func AtIndex[T any](i int, values Vec[T]) T — with a boundary guard for plain-Go callers. An out-of-range index is a compile error: cannot prove 7 < 3 at this call to AtIndex. Fin[n] remains the right tool where the evidence is already in hand.

v0.157.0 pays back the ergonomic cost of mandatory proofs and closes a generation bug that let an unfinished artifact reach disk.

An index can be inferred; a proof cannot. Erased arguments were nevertheless omitted as a group, so naming the mandatory proof forced spelling every index beside it. A call may now omit exactly the inferable erased arguments and still name its proofs:

return AtIndex(i-1, n-1, decide, t)   // before
return AtIndex(i-1, decide, t)        // now

Nothing is waved through — the index is inferred, then the proposition is checked against it, so AtIndex(7, decide, v) on a Vec[int, 3] is still cannot prove 7 < 3. The fix was in inference, not in the rule: unifying a parameter’s Vec[T, n] against a caller’s Vec[int, 3] clashes at T — a type parameter rather than a dependent variable — and used to abandon the whole instantiation there, losing n, the one position it wanted. That is exactly why a recursive step worked and a call site did not. std/vec is written in the shorter form, and the generated Go is byte-identical.

v0.157.0 also refuses to write an artifact that resolution never finished. Pass 1 does not lower a construct to Go; it lowers it to a skeleton plus a carrier that resolution consumes — a match becomes case nil: heads whose bodies are //goplus:pattern comments. That needs type information, so it needs a module, and without one the skeleton was written out as the finished artifact: unbound binders, duplicate arms, no return, from a command that exited 0. The file parses as Go, which is how it went unnoticed. Generation now checks for those carriers before writing and refuses instead. Go+ that needs no resolution still generates outside a module, so a single .gp file remains usable as a script.

v0.156.0 added named propositions, and with them completed Stage B of the dependent-typing roadmap. prop names a proposition, so a precondition is stated once and used by name:

type InRange[i nat, n nat] prop { And[Le[0, i], Lt[i, n]] }

func At[T any](0 i nat, 0 n nat, 0 p InRange[i, n], v Vec[T, n]) T

A name is an abbreviation, not a new kind of fact: a use unfolds into its body, and everything downstream then sees the relations it always saw — discharge, hypotheses, match refinement, the boundary guard, and the assume audit record all work unchanged. Propositions may name other propositions, and unfolding is bounded, so a self-referential declaration is refused rather than looping.

The declaration erases completely — it names facts, never values — so nothing reaches generated Go but a //goplus:prop marker, which is what lets a consumer unfold a use in their own package. Diagnostics read the use as you wrote it: cannot prove InRange[5, 3].

v0.155.0 adds conjunction. The common precondition is one — indexing wants 0 <= i and i < n — and saying that took two proof parameters and two witnesses. And[P, Q] says it in one:

func At[T any](0 i nat, 0 n nat, 0 p And[Le[0, i], Lt[i, n]], v Vec[T, n]) T

For the fourth time in this sequence the decider needed no new power: Decide already takes a list of facts, and a conjunction is exactly that. As a goal each part is proved in turn; in scope each becomes a hypothesis, so Lt[i, n] still prunes the impossible Nil arm. A failure names which half failed — cannot prove Le[0, 5] and Lt[5, 3].

v0.154.0 is where a bound refines a match. A proposition in scope became a hypothesis for the decider in v0.152.0, so bounds compose at a call — but it was still inert for matching: Lt[0, n] did not tell an exhaustiveness check that n is non-zero, so Vec[T, n] demanded a Nil arm that could never be taken.

func Head[T any](0 n nat, 0 p Lt[0, n], v Vec[T, n]) T {
	match v {
	case Cons(h, t):   // Nil is impossible: the bound says n is positive
		_ = t
		return h
	}
}

For the third time in this sequence the decider needed no new power — impossibility was decided by sign analysis, which cannot use facts, and now falls back to proving a strict inequality. The generated boundary guard agrees, so a plain-Go caller passing the impossible variant panics by name. It stays conservative: Le[0, n] does not prune, because a natural may be zero.

v0.153.0 fixes a soundness bug: a proof could be skipped.

Cast(v) — a call to a function with a proof parameter, with the erased arguments left out — was accepted with no proof, no assume, and no audit record, so a dependent guarantee was bypassable by accident and in silence. It reproduces against v0.146.0, so it long predated the recent proposition work.

The cause: a proof argument is deleted by the same pass that discharges it, so a call that never had one is textually identical to a call whose argument has already been erased. The checker could not tell “never proved” from “proved and erased”, and assumed the second. Obligations are now settled on the first resolve iteration, where the text is still exactly what you wrote, so the two are distinguishable with certainty rather than by heuristic.

A proof-carrying function may also only be used in a direct call — f := Cast, Cast >>> g, v |> Cast, and partial application all reached generated Go with no proof, so closing the omission alone would have relocated the bypass rather than shut it. A dependent function with no proposition is unaffected, and ordinary erased indices keep their inference.

v0.152.0 makes a bound in scope actually mean something. A proposition in scope is now a hypothesis: the enclosing function’s proof parameters are given to the decider, so bounds compose — under Lt[1, n], both Le[1, n] and Lt[1, n+1] follow with no new proof. And an erased index may now be forwarded to a call, without which the composition was unreachable: a quantity-0 name could not be written in any argument position, so an index could only ever be a literal.

func Forward(0 n nat, 0 p Lt[1, n]) int {
	return NeedsLe(1, n, decide)   // n forwarded; 1 <= n from the bound
}

Investigating this release surfaced a bug that predates it, now documented rather than hidden: omitting a proof argument skips its obligation. Cast(v), with the erased arguments left out, is accepted with no proof and no recorded assumption. The cause is architectural — such a call is textually identical to one whose arguments a previous pass already erased — and closing it means settling the obligation while the call site is still pristine. It is the highest-priority item on the dependent-typing roadmap.

v0.151.0 made a bound statable. Eq[a, b] was the only proposition a signature could state, so the most common dependent obligation — an index below a length — could not be written down, and the programs that most want dependent types could not express their real precondition. Le[a, b] and Lt[a, b] complete the set:

func At[T any](0 i nat, 0 n nat, 0 p Lt[i, n], v Vec[T, n]) T { … }

At(1, 3, decide, v)   // the decider discharges 1 < 3
At(5, 3, decide, v)   // cannot prove 5 < 3 at this call to At

The decider needed no new power — inequalities were decidable long before they were sayable. refl means reflexivity, so it discharges Eq alone; decide is the general witness and covers every proposition. A proposition is not yet a hypothesis: Lt[i, n] in scope does not tell a match that n is non-zero. That, user-declared predicates, and conjunction are the remaining Stage B work.

v0.150.0 makes assumptions cross the module boundary. goplus assumptions read the .gp source, so it stopped where trust matters most: you could audit what you assumed, not what your dependencies assumed — and a consumer receives committed Go, never the .gp. An assumption now travels in the artifact the way every other cross-package fact in Go+ does, as a //goplus:assume marker on the declaration containing the call, and goplus assumptions reports a dependency’s alongside your own. The marker carries no source position deliberately: generated files are committed and gen -checked, so a position would churn the artifact whenever an unrelated line moved.

v0.149.0 added assume.

The arithmetic decider is sound but incomplete, and until now a proposition outside its fragment had no discharge at all — the surrounding program was simply unwritable. At a proof parameter assume now stands where refl would: refl means the decider proved it, assume means you assert it. It performs no check and erases identically, so it never reaches generated Go.

Cast(1+1, 2, refl, v)     // the decider proved it
Cast(n*2, 2*n, assume, v) // you assert it

Because an assumption is the one place a dependent guarantee rests on a claim rather than a proof, every use is recorded and goplus assumptions lists them. It is deliberately not a diagnostic — that would block generation and defeat the point — so it is discoverable the way a Go reviewer finds unsafe: by asking. What a false assumption costs is bounded and worth knowing: it surfaces as a panic at the erasure boundary, never a wrong answer, because a quantity-0 index cannot reach runtime and every impossible-variant conclusion is backed by a generated guard. This opens Stage B of the dependent-typing roadmap.

v0.148.0 makes goplus lsp serve .goml buffers: the server runs the goml pipeline, so an unsaved buffer is transpiled in memory and its diagnostics — typed-hole goals included — come back positioned and spelled in goml. Hovering a ?name in a .goml file shows its goal. Delegated hover, definition, and completion stay .gp-only, because a .goml file’s Go is generated from its transpiled .gp text and a direct source-to-output line map would be meaningless. It also fixes editor registration that never matched: the Neovim and Zed clients keyed on a .goplus suffix — the language’s name rather than its file extension — so neither activated on a real .gp file. All three clients now register .gp and .goml.

v0.147.0 added typed holes, and v0.147.1 makes goml report their goals in goml’s own notation — Vec a (n + 1) rather than Vec[a, n+1], Slice String rather than []string, Int -> String rather than func(int) string. A goal you have to translate before you can use it is doing half its job. ?name stands where code is not written yet, and generation answers with the goal: the type that belongs there — in its un-erased dependent spelling where the position is dependent — together with the bindings in scope, including the quantity-0 indices that the generated Go no longer mentions:

func Rest[T any](0 n nat, v Vec[T, n+1]) Vec[T, n] {
	return ?rest
}

// main.gp:9:10: hole ?rest : Vec[T, n]
//   erased: Vec[T]
//   in scope:
//     n : nat (erased, quantity 0)
//     v : Vec[T, n+1]

Holes work in both surfaces and in every expression position, including a package-level initializer. ? in operand position claims a hole while the v0.4.0 postfix ? still claims the suffix; the two never compete, because a hole’s name is attached to its ? (a?b is (a?) b, a ?b applies a to a hole). Generation refuses to write while any hole remains, so a committed *_gp.go never contains one. In the editor, goals arrive as Information-severity diagnostics and hovering a ?name shows the goal — answered natively, since a hole is exactly why there is no generated Go to forward a hover to.

The goml REPL grows :holes, and :type now reports the declared signature rather than the erased Go type: a named binding prints in the goml spelling you wrote, indices intact, with no pipeline run at all.

goml> :type First
First : Vec a (n + 1) -> a
  elaborated: First[a any](0 n nat, v Vec[a, n+1]) a

Expressions, unannotated values, and imported names still report the erased Go type, which is now the only place the erasure caveat appears. A declaration containing a hole prints its goal and is not retained — each evaluation replays the whole session — and :holes recalls the goals while you work.

v0.146.0 grew goml’s Go-interop surface: &x and *p, indexing xs[i], channel send and receive outside select, imported constructors in patterns (result.Ok v), and if as a statement inside loop bodies. It also fixed two lowerings that produced wrong code rather than refusing — a void function’s if/else fell through and ran both arms, and a match binder used only inside a record literal or do block was blanked. Writing two networked services in goml was the forcing case for all of it.

v0.145.0 added the goml REPL and made a nullary goml let bind a value; v0.145.1 fixed the REPL’s output on a terminal.

goml repl evaluates goml interactively, and there is no interpreter behind it: every input transpiles the accumulated session, generates Go through the ordinary pipeline, and runs it, so the REPL agrees with the compiler by construction. Declarations skip the run entirely — the pipeline’s type check is the one the compiler performs — so they land in about a tenth of the time an expression takes. Because each evaluation compiles and runs the whole session, retained bindings re-execute every time; expression results are never retained, so a bare effectful call runs exactly once, and a binding that looks effectful is flagged when you define it.

goml now also follows ML’s rule for bindings: binders present means a function, none means a value. let Port : Int := 8080 lowers to var Port int = 8080, so bindings compose (let Next : Int := Port + 1); previously every let became a function, which made that a type error. A nullary function takes the unit binder, exactly as OCaml spells it: let main () := do { ... }.

goml itself — an ML-family (SML/OCaml/Idris2/Lean4-flavored) second surface for the same semantic core. A .goml source transpiles to .gp and generates through the unchanged pipeline, emitting committed ordinary Go (<file>_gml.go, same //goplus: markers): one core, two surfaces, one output. The v1 surface spans sums and GADTs, refinement comprehensions, classes/instances/laws, the dependent core (implicit binders, QTT quantities, propositional equality, constructor and total-call indices), let* monadic bind, do blocks, and select with lowered to native Go select; pipeline diagnostics map back to .goml lines. Writing a full worked tutorial against the first goml release closed three further gaps in v0.144.1: type-indexed GADT headers (type Expr : Type -> Type where), record literals (Settings { Port = p }), and logical negation. Its design and parity map live in the repo’s spec/goml-design.md, with executable-spec twins under features/goml/. v0.143.0 moved Java artifact production behind goplus build --target java (primary/sources/Javadoc JARs plus a deterministic goplus.java.build/v2 manifest), with publication belonging to assayxport’s ax publish.

Go remains the default target; goplus gen, build, test, and run now accept --target java for a checked portable subset targeting Java 25+. The backend emits deterministic Java source and a versioned runtime ABI, builds reproducible thin or bundled JARs, and can emit strong JPMS modules. It resolves Java APIs from the selected JDK, classpath/module path, and multi-release JARs, uses explicit UTF-8 at language boundaries, and rejects unsupported Go semantics with source-mapped diagnostics instead of silently changing them. Project policy lives in goplus.toml; CI exercises the end-to-end backend with JDK 25. See the Java target guide for the portability ledger, FFI contract, and artifact layout.

Java libraries can now be released through goplus publish --target java. The command builds and verifies a Maven Central Portal bundle containing the binary, generated-source, and documentation JARs, a provenance-complete POM, checksums, and detached OpenPGP signatures. Portal token credentials are read from Maven settings or the environment; publication may stop after validation for manual review or continue automatically to the immutable Central release. The current command is self-contained: it discovers Portal credentials from Maven settings, creates and safely persists a publisher OpenPGP identity on first use, publishes the public key, and derives deterministic signature time from the Git commit. Maven and GPG executables are not required, and rebuilding the same release with the same key produces the same bundle bytes.

This release also keeps generated tail calls go vet-clean by omitting self-assignments such as value = value, and aligns non-exhaustive pointer-box diagnostics with the compiler-error exit convention. The v0.141.1 patch makes the CLI and LSP report the distribution version independently from the generated-source compatibility vintage.

It builds on v0.140.0, which adds pointer-boxed enums (//goplus:box pointer). That stores an enum’s variants behind pointers — sealed markers on pointer receivers, so only *Variant satisfies the interface and construction is &Variant{} — matching the ubiquitous Go pattern of large sum types that are boxed and mutated in place (ASTs, IRs). A match over such an enum lowers to case *Variant: and binds the pointer, so exhaustive match — and in-place mutation through the bound scrutinee — finally work on pointer-boxed sums: a missing variant is a compile error, replacing runtime “impossible case” panics. It is additive (value enums and existing generated output are byte unchanged) and directive-level (no grammar change). Its consumers include gesbuild (esbuild AST) and gpsoup (the jsoup DOM).

The standard library advances independently and is currently v0.212.0, which makes std/clock’s fake time chronological (deterministic ordering for timer-driven tests). v0.211.0 hardens std/memory with secure-zeroing and platform-allocation defaults, an explicit managed-storage fallback, overflow-safe alignment, and constant-time live-allocation statistics. It builds on v0.210.0’s grouped arenas, structure-of-arrays layouts, reusable typed buffers, and property-tested ownership laws. v0.208.0 adds std/text/scan (a buffered rune cursor for hand-written lexers — mark/rewind, consume-until, match-prefix, line/column tracking) and std/charset (character-encoding detection and decoding — BOM sniffing, label folding, Content-Type charset extraction, transparent gzip, and native UTF-8/16, latin-1, Windows-1252 fast paths plus the WHATWG registry). Both were extracted from gpsoup’s jsoup port and are now consumed by it. Install the toolchain with go install goforge.dev/goplus/cmd/goplus@v0.158.0 (and the goml surface with go install goforge.dev/goplus/cmd/goml@v0.158.0); consume the stdlib with go get goforge.dev/goplus/std@v0.213.2.

The toolchain and stdlib version lines are independent: the compiler is on the v0.15x line, the standard library on the v0.21x line.

std/iter is a lazy sequence algebra: a Seq[T] wraps the standard iter.Seq[T] with fluent combinators (Map, Filter, FilterMap, FlatMap, Enumerate, Uniq, Take/Drop/TakeWhile/DropWhile, Reverse, Chunk, Concat, Fold), First/Fold return std/option/std/result values, and it erases back with Seq(). Because First() Option[T] gives value-or-default (.UnwrapOr(d)) and Enumerate (v0.209.0) gives indexed iteration without an int in every callback, Go+ programs get the full functional-collection surface from the standard library — no third-party lodash required. Its laws (round-trip, map∘filter fusion, take/drop partition, reverse involution) are property-checked, and the goforge.dev/lo/it iterator package is a thin facade over it.

v0.26.0 — Method-Indexed Linear HTTP Foundations

The /goals/09-resty forcing case adds cross-package inference for an omitted natural index when the same call consumes a quantity-1 capability. HTTP method, body replayability, and decode phase now survive ordinary-Go erasure without making Go+ callers spell proof-only parameters or generated LinOf wrappers.

std/retry exposes the shared protocol-neutral layer: normalized attempts, cancellable waits with a zero-allocation immediate path, and overflow-safe capped delay progression. HTTP status policy and response ownership remain in the client rather than leaking into the standard library.

v0.25.0 — Dependent Rewrite Foundations

The first eight package rewrites now feed a shared, released Go+ foundation: scale-indexed decimal arithmetic, nonempty and length-indexed collections, schema-indexed configuration, pattern-indexed HTTP routes, typed expressions and bytecode, schema-aware JSON paths, validated witnesses, and grammar-indexed schedules.

The compiler reconstructs dependent indices across package boundaries, nested calls, GADT constructors, dependent parameters, and stable local bindings. Generated Go retains runtime witnesses and guards wherever ordinary Go crosses an erased dependent boundary. The complete program and opt-in dependent typing roadmap is tracked in the source repository’s GOALS.md.

v0.24.1 — Durable Workflows and Effect Boundaries

Six Go+-authored standard-library packages make command-line and delivery workflows explicit without pretending external systems are transactional:

  • std/process executes commands with capture/stream modes, cancellation, typed exit failures, and secret-safe diagnostics.
  • std/semver implements strict Semantic Versioning 2.0 parsing, precedence, formatting, and major/minor/patch increments.
  • std/workflow journals resumable saga steps and compensations; its supplied file journal uses crash-safe replacement.
  • std/config composes defaults, format adapters, semantic validators, and field-path errors.
  • std/fsatomic replaces files through write, sync, rename, and directory sync, with platform-correct durability behavior.
  • std/cas defines typed observations and the exhaustive Updated, Changed, and Missing outcomes shared by compare-and-swap stores.

These packages separate locally provable workflow state from facts that must be observed again at an external mutation boundary. Go+ enums make CAS outcomes exhaustive, while generated Go keeps every package usable by ordinary Go programs.

The v0.24.1 patch removes redundant unreachable sentinels for consistent Go 1.26 analysis and gives workflow journal records an explicit stable JSON schema.

v0.23.0 — QUIC v2, CBOR, and Proven DAG-CBOR

HTTP now works through the simplest package-level calls with automatic HTTP/3 discovery and safe HTTP/2 and HTTP/1.1 fallback. The default server supports RFC 9368 compatible QUIC version negotiation and RFC 9369 QUIC v2.

The standard library adds generic serde.Codec[T], deterministic RFC 8949 CBOR, explicit RFC 7049 compatibility, streaming sequences, tags, raw messages, custom marshal hooks, and diagnostic notation.

Strict DAG-CBOR enforces the IPLD data model and deterministic wire form, including string map keys, finite 64-bit floats, and CID tag 42. Its unforgeable Proof[T] binds a decoded Go or Go+ value to canonical bytes and their SHA-256 digest, making trust boundaries visible in the type signature.

v0.22.0 — Refinement Types and Structural GADT Elimination

Refinement declarations express checked semantic subsets of ordinary Go types while keeping the generated representation portable:

type Positive refine(value int) { value > 0 }

Go+ proves constant constructions, path-guarded values, calls, assignments, and returns where possible. It rejects unproved uses during generation and adds runtime guards at exported Go boundaries. Generated contract markers carry refinement semantics across package boundaries.

Structural GADT matches can also eliminate composite indices through generic scrutinees, including recursive cases such as Expr[U] matching a constructor whose result is Expr[[]T]. Private erased views implement those matches while the public API remains typed and the emitted code remains standard Go.

v0.21.0 — Native Tail Calls

tail func and its explicit recur(nextArgs...) statement provide constant- stack self recursion while preserving Go’s evaluation rules:

tail func sumTo(n, acc uint64) uint64 {
	if n == 0 {
		return acc
	}
	recur(n-1, acc+n)
}

The generated Go is a labelled for loop with simultaneous parameter assignment and continue; no recursive call remains. recur must be the final statement of the function or a tail branch, works in methods and nested if/switch/select/match control flow, and uses Go’s left-to-right argument evaluation. In a total func, the existing structural-decrease proof still applies before lowering.

v0.20.0 — Native HTTP/3 and RFC 9220 WebSockets

The standard library gained native HTTP/3 client and server transports over QUIC, including QPACK, connection and stream flow control, recovery, congestion control, and a compatibility backend built on quic-go. The HTTP facade keeps HTTP/1.1, HTTP/2, and HTTP/3 behind one request/server API. WebSockets now work over HTTP/3 extended CONNECT (RFC 9220) as well as HTTP/2 (RFC 8441) and the HTTP/1.1 Upgrade path (RFC 6455).

v0.18.0 — WebSockets over HTTP/2

RFC 8441 extended CONNECT added WebSocket client and server support over HTTP/2, with automatic RFC 6455 fallback when the peer does not advertise the extension. The same framing and message semantics are shared across both transports.

v0.17.0 / v0.17.1 — WebSocket Semantics

std/websocket introduced RFC 6455 framing, client and server handshakes, fragmentation, control messages, per-message deflate, limits, and typed protocol failures. Its Go+ API models connection phases with indexed sessions and linear capabilities, so sending and closing preserve single ownership while plain Go callers can use Conn directly. The follow-up completed edge semantics and strengthened conformance, fuzz, race, benchmark, and Autobahn coverage.

v0.16.0 / v0.16.1 — Cross-Package Law Tests

Generated property tests for class laws now preserve the source package’s imports, including single-import declarations. Cross-package laws can therefore refer to imported types and helpers without producing incomplete generated Go.

v0.15.0 — Go+ Is Go+

The language, command, module, generated markers, editor integrations, and documentation moved from the old gpp name to Go+ and goplus. The public module and install path became goforge.dev/goplus, with .gp as the source extension.

v0.14.0 — Multi-Pattern Arms

Driven by rune’s elaborate/store rewrite: rigidity and spine classifiers union constructors in one arm — case Var(_), Ref(_), Univ(_), Prop: lowers to Go’s multi-type case. Alternatives take only wildcard arguments and cannot bind (split the arm to bind); each alternative is its own reachability row, so redundant alternatives are unreachable-arm errors and all alternatives count toward exhaustiveness.

v0.13.0 — The Standard Library Grows Nine

Nine general-purpose packages extracted from the first whole-system Go+ rewrite (envoy-go): std/kleene (K3 three-valued logic), std/latch, std/clock (time seam + deterministic fake), std/guarded, std/deepmap, std/retry, std/registry (freeze-after-boot), std/memo, and std/closeonce — all authored in Go+, tested under -race, and consumed in anger. No language changes.

v0.11.0 — Deep Structure

The release that arms the rune kernel rewrite: an enum’s recursive structure is now derivable, not hand-rolled. Derived deep traversals — every self-recursive enum gets <Enum>Children, <Enum>Universe (an iter.Seq, preorder), and <Enum>Transform (bottom-up rewrite, slices copied never mutated), with descent seeing through binder wrappers like Scope{Name string; Body Tm}. Derived structural equality with per-variant overrides — <Enum>Equal, plus <Enum>EqualWith threading an overrides struct whose hooks return (eq, handled): proof irrelevance becomes an override on a derived base instead of a hand-written walk; closures make an enum silently underivable, transitively. std/option joins std/result at the comma-ok boundary. Both derivations are nil-tolerant, and variant doc comments now survive lowering onto the generated structs — generated Go documents itself on pkg.go.dev.

v0.10.0 — The Dogfood Rewrite

cadence v0.2.0 is authored in Go+ — the first external artifact rewritten in the language — and the rewrite drove the release: derived rapid generators for every enum (demand-driven emission, so rapid never enters go.mod uninvited), laws that quantify over enums (every Interpreter instance gets a generated property proving the no-JS fallback law; violations shrink to counterexamples), multi-result class operations, and Go+ test sources (foo_test.gp → foo_gp_test.go). In cadence, Strategy became a real sum type — a strategy that is not Deferred cannot carry a Where or a Trigger — and the hand-rolled law checker died in favor of the law itself.

v0.9.0 — Tooling: LSP, Editors, go generate

No language changes — this release is about living with goplus. goplus lsp ships inside the binary (its version IS the language version, and its dispatch layer is authored in goplus itself): diagnostics as you type from the real pipeline run in memory, with hover, goto-definition, and completion delegated to gopls over the generated Go and mapped back. Thin clients for VS Code, Neovim, Zed, and GoLand live under editor/. The canonical workflow is now the go toolchain’s own:

goplus init          # scaffolds //go:generate go tool goplus gen ./...
go generate ./...
go build ./...

Cross-package hardening rounds it out: generated files carry a //goplus:v vintage stamp (files from a newer goplus tell you the exact upgrade command), marker reconstruction is package-wide, index domains cross packages (Socket[s states.State]), imported Eq propositions unfold their callee’s totals, and a missing instance names the transitive package that provides one — with the import line to fix it.

v0.8.0 — Parser Combinators (std/parsec)

Parsec-style consumed/empty semantics over streaming input, authored in goplus itself:

import "goforge.dev/goplus/std/parsec"

func grammar() parsec.Parser[int] {
	var expr parsec.Parser[int]
	factor := parsec.Label(parsec.Or(number(), parsec.Between(parsec.Symbol("("), parsec.Defer(&expr), parsec.Symbol(")"))), "expression")
	term := parsec.Chainl1(factor, mulOp())
	expr = parsec.Chainl1(term, addOp())
	return parsec.Then(parsec.Spaces(), parsec.Before(expr, parsec.EOF()))
}

v, _ := parsec.RunString(grammar(), "(1+2)*3")  // 9
// 1:3: unexpected '*', expecting expression

Or commits once a branch has consumed; Try restores the lookahead. Input streams from any io.Reader — the buffer retains only what a live Try could rewind to, and a byte-at-a-time reader parses identically to a string (rapid-tested alongside the monad identities and Or’s associativity). Reply is a goplus enum matched in every combinator, its derived Fold consumes replies without a match, and Run’s output rides the v0.4 railway. The linear-value cell also went atomic in this release.

v0.7.0 — The Dependent Core

Dependent types compiled to plain Go: QTT quantities, total functions, indexed enums, propositional equality, and linearity — all erased.

type Vec[T any, n nat] enum {
	Nil() Vec[T, 0]
	Cons(head T, tail Vec[T, n]) Vec[T, n+1]
}

func Head[T any](0 n nat, v Vec[T, n+1]) T {
	match v {
	case Cons(h, t):   // Nil is impossible at n+1 — no other arm needed
		return h
	}
}

total func Plus(a, b nat) nat {
	if a == 0 { return b }
	return Plus(a-1, b) + 1
}

func Cast[T any](0 n nat, 0 m nat, 0 p Eq[n, m], v Vec[T, n]) Vec[T, m] {
	return v
}
w := Cast(Plus(1, 1), 2, refl, v)   // the decider proves it; erases to identity

func Process(1 f *os.File) error { return f.Close() }  // consumed exactly once

A parameter’s quantity says how it may be used: 0 exists only at check time (indices, proofs — guaranteed absent from the generated Go), 1 is consumed exactly once on every path (checked statically; erased Go polices plain-Go callers through generated use-once Lin[T] cells), and multiplicity variables ([m mult]) abstract over both. Enums index by nats, by enum tags (typestate: Socket[Open]), and by structured first-order data; a match whose scrutinee’s index is known prunes impossible arms from exhaustiveness. total func declares compiler-verified termination and becomes callable in types; nat subtraction is admissible exactly where the path proves it safe. Eq[a, b] discharges by refl through a linear-arithmetic decider that also normalizes n+m ≡ m+n definitionally. Exported dependent functions guard their erased preconditions at runtime, so plain Go fails fast with a precise message instead of computing garbage. goforge.dev/goplus/std/vec ships the length-indexed sequence.

v0.6.0 — Folds, Full GADTs, Existentials, Delegation

Structural GADT result types, bounded existentials, a derived fold for every enum, and Kotlin-style interface delegation:

// Result arguments are arbitrary type expressions, cross-position included:
type Expr[T any] enum {
	Lit(v int) Expr[int]
	Wrap(inner Expr[T]) Expr[[]T]
}

// Bounded existentials — the hidden type erases to its interface bound:
type Row[T any] enum {
	Packed[A fmt.Stringer](x A, tag string)
}

// Every enum derives a one-level fold (opt out with //goplus:derive off):
n := Fold(Some(7), OptionCases[int, string]{
	Some: strconv.Itoa,
	None: func() string { return "-" },
})

// Interface delegation — forwarders generated, overrides respected:
type Logged struct {
	inner Store delegate
	log   *log.Logger
}

Match arms refine type parameters by structurally unifying the variant’s result type against the scrutinee’s — through slices, maps, pairs, and cross-position uses — and only genuinely mismatched conversion boundaries get an assertion. Existential type variables must carry an interface bound: Go cannot express a match arm that is generic in a hidden type (rank-2 polymorphism), so the unbounded form is a compile error with guidance, and bounded variables erase to their bound in fields, constructors, and binders. std/result now ships a derived result.Fold(r, result.ResultCases[T, E, R]{Ok: …, Err: …}), and delegation gives any struct an interface implementation through a field one keyword wide.

v0.5.0 — Typeclasses

Lean-flavored classes, named instances, implicit dispatch, and a law-tested algebraic hierarchy, lowered to plain Go witness structs:

type Monoid[T any] class {
	Semigroup[T]
	Empty() T
	law LeftId(a T) { return reflect.DeepEqual(Combine(Empty(), a), a) }
}

instance IntAdd Group[int] {
	Combine(a, b int) int { return a + b }
	Empty() int { return 0 }
	Invert(a int) int { return -a }
}

func Accumulate[T Monoid](xs []T) T {
	acc := Empty()
	for _, x := range xs {
		acc = Combine(acc, x)
	}
	return acc
}

Accumulate([]int{1, 2, 3})   // one Monoid[int] in scope: found implicitly

A class is an algebraic structure in the mathematical sense: a carrier set (the instantiating type) with operations satisfying declared laws — a Monoid is the triple (T, Combine, Empty) with associativity and a two-sided identity, and an instance names one concrete such structure. That is why int has TWO monoids, and why implicit resolution refuses to guess: with std/algebra imported, Accumulate([]int{…}) is ambiguous between IntAdd (a Group, by subsumption) and IntMul, and the error names both. Disambiguate by naming the structure you mean:

algebra.Accumulate(algebra.IntAdd, []int{2, 3, 4})  // 9  — additive
algebra.Accumulate(algebra.IntMul, []int{2, 3, 4})  // 24 — multiplicative

Explicit witnesses subsume exactly like implicit dispatch (v0.6.1): IntAdd is a Group instance, Accumulate wants a Monoid, and the compiler inserts the upcast — you name the structure, never the coercion.

Classes embed into hierarchies (diamonds collapse, upcasts generate); operations may carry default bodies instances omit; a stronger instance satisfies a weaker constraint (a Group answers a Monoid call). law members declare boolean properties and law tests generate BY DEFAULT for every concrete instance as rapid properties — goforge.dev/goplus/std/algebra ships the law-tested Magma→Group hierarchy (each structure documented as its mathematical definition), stock instances, and Accumulate/FoldMap. As of v0.5.1, lowered names come from the code itself: Stack.Map lowers to func Map when unique, receiver-prefixed only on collision — the //goplus:name directive is gone.

v0.4.0 — Typed Failure

Railway-Oriented error handling: a shipped Result[T, E] standard library, track-aware pipelines, Kleisli composition, postfix ?, and expression-oriented control flow:

import "goforge.dev/goplus/std/result"

n := s |> validate |> strings.TrimSpace |> strconv.Atoi |> audit |> .UnwrapOr(0)

pipeline := strings.TrimSpace >=> validate >=> strconv.Atoi >=> save

data := os.ReadFile(path)?

y := if x > 2 { "big" } else { "small" }
area := match shape {
case Circle(r):
	3.14 * r * r
case Rect(w, h):
	w * h
}

Once a Result flows through |>, stages lift by shape — T→Result binds, T→(U, error) adapts, T→U maps, T→() tees on the Ok path — and Err bypasses everything. >=> composes fallible steps with the same lifting. ? propagates failure to the enclosing function, in both Go-shaped (…, error) and Result functions, preserving typed errors. if/switch/match work as expressions with single-expression arms; match expressions keep exhaustiveness, GADT refinement, and nested patterns. The standard library is a separate zero-dependency module: go get goforge.dev/goplus/std@latest.

v0.3.0 — Functional Flow

Pipelines, composition, and partial application, lowered to the plain Go you would have written:

total := xs |> Filter(isEven) |> Map(double) |> Sum
answer := 21 |> Some |> .Map(double).UnwrapOr(0)
toStr  := double >>> strconv.Itoa
inc    := add(1, _)

|> inserts the piped value as the first argument (or at a _ slot) and is method-aware: bare segments resolve against the piped value’s members — Go’s selector semantics plus Go+ generic and enum methods — and against functions, constructors, builtins, and conversions in scope, with hard-error collisions and explicit disambiguating spellings. Multi-result stages follow Go’s spread rule. >>> composes into capture-once closures, constructor operands included; _ makes any call a partial application.

v0.2.0 — Algebraic Data Types

Sum types, exhaustive matching, and initial GADTs, all as portable Go:

type Option[T any] enum {
	Some(value T)
	None
}

func (o Option[T]) Map[U any](f func(T) U) Option[U] {
	match o {
	case Some(v):
		return Some(f(v))
	case None:
		return None
	}
}

Enums lower to sealed interfaces plus variant structs that plain Go consumes with an ordinary type switch. match is exhaustive with witness diagnostics (Maranget usefulness, so nested patterns like Add(Lit(a), Lit(b)) are checked correctly); constructors infer their type arguments from context; GADT variants pin result types (Lit(v int) Expr[int]) and refine type parameters inside their arms — the classic typed interpreter compiles and runs.

v0.1.0 — Generic Methods

Go forbids type parameters on methods. Go+ doesn’t:

// stack.gp
func (s Stack[T]) Map[U any](f func(T) U) Stack[U] { … }

goplus gen lowers each generic method to a package-level generic function in a committed stack_gp.go beside the source — fully typed, gofmt-clean, protobuf-style. The lowered function keeps the method’s own name (the name is already in the code); only when two types in the package share a method name do the colliders fall back to the receiver-prefixed form (StackMap, RingMap):

//goplus:method (Stack[T]) Map[U]
func Map[T any, U any](s Stack[T], f func(T) U) Stack[U] { … }

Go+ callers keep method syntax — chained calls, explicit instantiation (s.Map[string](f)), method values with bind-time receiver capture (f := s.Map[string]), and promotion through embedded fields, all following Go’s own method rules (auto-&/*, shallowest-depth promotion, real methods always win). Plain-Go consumers just call stack.Map(s, f). The //goplus:method marker makes the emitted file self-describing, so packages that import yours get method syntax too — even fetched as ordinary Go via go get.

  • Toolchain wrapper — goplus gen ./... plus goplus build|test|run|vet, which regenerate and delegate to the go tool. gen -check for CI, gen -stage for the pre-commit hook shipped in the repo.
  • Diagnostics in your terms — the emitted result is type-checked before anything is written; errors point at .gp lines.
  • Executable specification — the Cucumber/Godog feature suite and the EBNF grammar delta are the spec: examples, scenario outlines, data-driven corpora, and rapid-driven property tests (superset, lossless passthrough, deterministic and idempotent generation).

Roadmap

Algebraic data types with exhaustive matching (v0.2.0), pipelines and composition (v0.3.0), typed failure with railway pipelines (v0.4.0), typeclasses with a law-tested std/algebra (v0.5.0), folds, full GADTs, bounded existentials, and delegation (v0.6.0), and the dependent core — QTT quantities, total functions, indexed enums, Eq, linearity, std/vec (v0.7.0), streaming parser combinators (v0.8.0), the tooling milestone — LSP, four editors, go generate (v0.9.0), the dogfood rewrite of cadence (v0.10.0), and deep structure — derived traversals, derived equality with overrides, std/option (v0.11.0), and multi-pattern match arms (v0.14.0) — all shipped.