Cure v0.19.0 :: Bring the Furniture

v0.18.0 spent the whole release refinishing one thing—pattern matching. That focus was deliberate: the previously-slated v0.18.0 "furniture" items all needed destructuring to land cleanly first.

v0.19.0 is the furniture.

proof containers

Cure is dependently typed at the core; v0.17.0 brought Sigma, Pi, Eq(T, a, b), and the rest. What was missing was a syntactic home for propositions. Enter proof:

proof Std.Proof
  fn plus_zero(_n: Int) -> Eq(Int, n, n) = :cure_refl
  fn append_nil(_xs: List(T)) -> Eq(List(T), xs, xs) = :cure_refl

Same shape as a module, except every binding must return Eq(...) or a refinement witness. The compiler enforces the shape under code E026. Runtime values are just :cure_refl atoms; the type checker does the work, the BEAM module is normal-looking code.

assert_type expr : T

A compile-time type assertion with zero runtime cost:

fn doubled(n: Int) -> Int = assert_type n * 2 : Int

The type checker verifies that expr has type T; codegen strips the wrapper. Mismatches surface as E027.

Record field defaults

rec Person
  name: String = "Anonymous"
  age: Int = 0
  active: Bool = true

Fields with default expressions merge in at construction time. A caller-supplied value always wins. Default-versus-declared-type mismatches are caught as E028.

@derive(Show, Eq, Ord)

@derive(Show, Eq, Ord)
rec Point
  x: Int
  y: Int

Cure.Types.Derive existed since v0.12.0 but was never fully wired. v0.19.0 plumbs it end-to-end: the decorator synthesises show/1, eq/2, and compare/2 as plain module exports.

Property-based testing

Two new stdlib modules work together:

• Std.Gen ships tiny stateless generators (int_in, bool, list_int, list_of_int, one_of, constant) backed by :rand.
• Std.Test.forall(gen, property, runs) runs the property against samples; it returns :ok or raises :property_failed.

mod Laws
  use Std.Gen
  use Std.Test

  fn test_plus_zero() -> Atom =
    forall(fn(_) -> int_in(-100, 100), fn(n) -> n + 0 == n, 100)

Std.Iter

A minimalist lazy iterator protocol:

use Std.Iter

fn sum_range(n: Int) -> Int =
  let it = range(1, n)
  fold(it, 0, fn(x) -> fn(acc) -> acc + x)

Constructors: empty/0, from_list/1, range/2. Consumers: fold/3, take/2, to_list/1. take/2 stops before materialising the tail, so unbounded ranges are safe so long as you only peek at a prefix.

Package registry, first half

Cure.Project.Version parses SemVer versions and compound constraints:

• ~>, >=, <=, <, >, == individually.
• and to combine (~> 1.0 and < 1.5.0).
• MAJOR.MINOR is accepted as shorthand for MAJOR.MINOR.0.

Cure.Project.Resolver.resolve/2 is a deterministic backtracking resolver over a local registry. Newest compatible version wins. Conflicts surface as E030. The remote index service is slated for v0.20.0.

Mutual-recursion totality

Cure.Types.Totality.check_mutual/1 runs Tarjan’s SCC algorithm on a module’s call graph. Non-trivial strongly-connected components are classified :ok (structural decrease proven on at least one path) or :suspect (E029).

Multi-head cons patterns

match xs
  [a, b, c | rest] -> a + b + c
  _                -> 0

The parser desugars [a, b | rest] into right-associated cons cells. Works in pattern and construction position.

Error catalog

Five new codes: E026 proof shape, E027 assert_type failed, E028 record default mismatch, E029 mutual recursion not structural, E030 package version conflict. cure explain E0xx works for every entry.

By the numbers

• 2 new Elixir modules (Cure.Project.Version, Cure.Project.Resolver); major extensions to Cure.Types.Totality, Cure.Compiler.Codegen, Cure.Compiler.Parser, Cure.Types.Checker, Cure.Types.Type, Cure.Compiler.Errors.
• 3 new stdlib modules (Std.Proof, Std.Gen, Std.Iter); Std.Test extended.
• 4 new examples, 1 new documentation file (docs/PROOFS.md).
• Total tests jumped to ~970; mix credo --strict stays at 0 issues; mix cure.check.stdlib at 24/24 and mix cure.check.examples at 30/30.

What’s next

• v0.20.0: the remote package-registry index service, signing, and Hex.pm cross-publishing.
• Refinement narrowing through nested record/map patterns.
• Full bitstring-pattern segment specifiers in PatternCompiler.

Getting started

git clone https://github.com/am-kantox/cure-lang.git
cd cure
mix deps.get && mix test
mix escript.build
./cure version            # Cure 0.19.0
./cure run examples/proof_laws.cure
./cure run examples/derived_show.cure
./cure run examples/lazy_iter.cure

The repository is at github.com/am-kantox/cure-lang. The furniture is in. Time to actually live in the place.