Cure v0.34.0 :: Dependent Core, Staged Macros & Certified Regex

Cure v0.34.0 is the single largest release in the history of the language.

For thirty-three releases, Cure has operated with a dual personality: a surface language with rich refinements and SMT integration on one hand, and a traditional compiler pipeline targeting the BEAM on the other. In v0.34.0, that separation is gone. The classic checker and code generator have been retired. In their place stands a unified, kernel-verified, dependently-typed pipeline where every program is elaborated to a small Core, checked for type correctness and quantitative usage, certified for totality, and emitted to BEAM bytecode.

This monumental milestone represents hundreds of commits and an immense engineering effort. The vast majority of the architectural design, kernel implementation, dependent surface elaboration, macro engine, and certified regex infrastructure in this release was authored by Cosmo S. Harbinger (GitHub handle Qata).

Author Credit

The Cure community owes its deepest gratitude to Cosmo S. Harbinger (@Qata), who designed, implemented, and refined almost every major subsystem in v0.34.0. From the de Bruijn indexed kernel and Normalization by Evaluation (NbE) engine to quantitative erasure, staged macro evaluation, PCRE lookaround certification, and standard library modernization—Cosmo's work has turned Cure into a production-ready, dependently-typed language on the BEAM.

One Dependent Compiler Pipeline

The classic type checker and separate code generator are officially retired. Every .cure program now flows through a single unified pipeline:

Source (.cure) ──> Elaboration (Cure.Elab.Program) ──> Core Validation & Erasure ──> BEAM Bytecode

The Verified Kernel

Parsing now feeds directly into Cure.Elab.Program and the Core kernel. The kernel independently validates:

• Cumulative Universe Hierarchy: Sound stratification of Type universes.
• Pi and Sigma Types: Dependent function types (x: A) -> B(x) and dependent pair types Sigma(x: A, B(x)) with projection semantics.
• Indexed Inductive Families (GADTs): Parameter and index separation via indices, preserving constructor-varying indices at type-check time.
• Definitional Equality via NbE: Normalization by Evaluation (Cure.Types.Reduce) evaluates closed type-level arithmetic, booleans, and projections without invoking external SMT solvers.
• Size-Change Totality Certification: Mechanically verified termination for recursive functions and mutual recursion clusters.
• Inductive Equality: Primitive Eq/refl/rewrite tokens have been retired in favor of Std.Equivalent, providing kernel-recognized inductive identity Equivalent(a, x, y) and the reflexive constructor.

Quantitative Usage Grades {0, 1, ω}

Every binder in Core carries a usage grade:

• 0 (Erased): Compiles to compile-time proof witness; guaranteed never to survive into BEAM bytecode.
• 1 (Linear): Must be consumed exactly once.
• ω (Unrestricted): Standard affine or unrestricted computation.

Runtime code generation enforces strict quantitative erasure: erased parameters and proof terms are stripped before code emission, ensuring zero runtime cost for type-level proofs.

Dependent Language Surface & Syntax Enhancements

v0.34.0 brings the language surface in line with its new dependently-typed core.

Brace-Implicit Arguments {T}

Implicit parameters are declared with {T} braces and automatically solved via first-order unification with an occurs check:

fn id({T}, x: T) -> T = x

Implicit arguments carry grade 0 by default and are erased during compilation.

Canonical Tuple-Type Syntax %[A, B]

Tuple types now mirror tuple values by using the %[...] sigil:

fn pair(x: Int, y: String) -> %[Int, String] = %[x, y]

-- Dependent tuple binders:
type DepTuple = %[x: Int, Vector(String, x)]

Legacy (A, B) tuple type syntax is deprecated (E086 / E-TYPE-TUPLE-PAREN) and will be removed in a future edition.

Expanded Pattern & Expression Language

• Pattern Elaboration: Shared structural pattern elaboration across match, multi-clause heads, and pattern-valued let (literals, tuples, cons/list, maps, records, constructors, pins, repeated variable equality).
• Flexible Anonymous Functions: Support for single-expression, indented, brace-delimited, and end-terminated multi-expression lambdas with bidirectional type propagation.
• Covariant Top Type Any: Any functions as a genuine top type in safe covariant positions (e.g., List(Int) is assignable to List(Any)).
• Expressible Literals: Contextual integer literal interpretation via ExpressibleByNaturalLiteral and ExpressibleByIntegerLiteral.

Interfaces, Implementations & Canonical Modules

The protocol system has been modernized to align with dependently-typed interface standards:

• interface and implementation: Replace legacy proto / impl keywords. Generic constraints are declared using requires:

interface Comparable(T) {
  fn compare(a: T, b: T) -> Ordering
}

implementation Comparable(Int) {
  fn compare(a: Int, b: Int) -> Ordering = ...
}

• Separation of Equality Concerns:
  • Std.Equatable: Backs runtime structural equality (==, !=).
  • Std.Comparable: Replaces Std.Ord, backing comparison operators (<, <=, >, >=).
  • Std.Equivalent: Kernel-level proof equality.
• Topological Module Graph: Declaration loading and prelude discovery now follow module dependency graphs rather than arbitrary file ordering. Operator precedence groups propagate through use directives.

Staged Derivation & MetaAST Macro Engine

v0.34.0 introduces a robust staged macro surface and syntax reflection model:

• Structural Derivation: @derive(Show, Equatable, Ord) automatically generates Comparable and Show implementations; @derive(JSON) generates to_json/1.
• User-Defined Syntax: Staged syntax ... becomes definitions, typed hygienic holes, quote with splicing, computed by, and Std.Syntax reflection enable embedded domain-specific languages. OTP actors, FSMs, supervisors, and reactive abstractions are now authored entirely through this macro surface.

Standard Library Overhaul & Peer Lazy Iterators (Std.Iter)

The standard library has been systematically restructured around canonical module paths:

• Canonical homes: Std.Option (Option, Some, None), Std.Result (Result, Ok, Error), Std.Vector, Std.NonEmpty, Std.Decision, Std.Sigma, Std.Tuple, and Std.Otp.
• String is now a transparent alias for List(Char).

Lazy Iterators (Std.Iter)

Std.Iter is now a first-class peer of Std.List, providing an efficient, non-allocating lazy pipeline API:

use Std.List
use Std.Iter

fn even_squares(nums: List(Int)) -> List(Int) =
  nums
  |> lazy
  |> filter(fn(x) -> x % 2 == 0)
  |> map(fn(x) -> x * x)
  |> take(5)
  |> to_list

• Entry Point: lazy/1 (alias of from_list/1) explicitly marks the transition to lazy evaluation.
• Producers: iterate/2, unfold/2, repeat/1, cycle/1.
• Transformers: map/2, filter/2, flat_map/2, concat/2, zip_with/3, intersperse/2.
• Slicers: take_while/2, drop/2, drop_while/2.
• Consumers: each/2, count/2, any/2, all/2, find/3, fold/3, to_list/1.

Codebase-Wide pickup Adoption

Per the v0.33.0 specification (docs/PICKUP.md), legacy if/elif/else syntax has been completely removed across all lib/std/*.cure modules and all project examples in favor of pickup.

Certified Refutational Regex Engine (Std.Regex)

Std.Regex has been completely rewritten into a certified, type-indexed pattern machine:

• Direct Pattern Machine Compilation: Compiles regexes directly into executable state machines with typed evidence decoding.
• Advanced PCRE Features: Full support for lookarounds ((?=...), (?!...), (?<=...), (?<!...)), capture conditionals (?(condition)then|else), branch reset groups (?|...), and Unicode character properties.
• Proof-Carrying Refutations: Search paths carry typed traversal witnesses and indexed refutation trees certifying finite search exhaustion for complex lookaround assertions.

Diagnostics, Migration & Verification

• Diagnostic Registry Alignment: Fixed a diagnostic code collision where protocol verification borrowed E056; protocol diagnostics now reside cleanly under PROTO001.
• Language Editions (@edition): Codebases can pin grammar and keyword sets. The cure migrate CLI command performs automated, idempotent AST migrations for keywords (proto -> interface), tuple types, and pickup syntax.
• Trust Audit: cure audit trust <Module> audits all reachable postulate, bodyless @extern, and believe_me escape hatches in a project.
• Verification Status: All 40+ root examples pass cleanly under mix cure.check.examples, and over 1,800 unit and integration tests pass with zero regressions.

Summary of Changes

Looking Ahead

With the single dependent pipeline established and the core type theory fully realized on the BEAM, Cure enters a new era of safety, performance, and developer ergonomics.

To upgrade your projects to v0.34.0, run cure migrate on your codebase and explore the refreshed documentation in docs/STDLIB.md.