← All posts

Cure v0.17.0 :: Proofs & Polish—Toward Idris

by Aleksei Matiushkin

release dependent-types sigma pi equality holes totality repl lsp doctests

For seven versions Cure has been building infrastructure: a lexer, a parser, a bidirectional type checker, refinement types, Z3 integration, FSMs, a protocol system, an effect system. It worked. It even shipped real programs. But the gap between Cure as a language and Cure as a dependently-typed language was conspicuous. Every time you wanted to say "this function’s return type is Vector(T, m + n)", the compiler nodded politely and moved on.

In v0.17.0 it stops nodding.

Sigma types, Pi types, equality types

Three shapes that have been missing arrive together:

  • Sigma types pair a value with a type that depends on it. Sigma(n: Nat, Vector(T, n)) is "a pair of a natural number and a vector of exactly that length." Cure.Types.Sigma recognises the surface syntax, subtypes componentwise, and round-trips to plain tuples at runtime.

  • Pi types are function types whose return depends on the arguments:

    fn append(xs: Vector(T, m), ys: Vector(T, n)) -> Vector(T, m + n)

    At each call site the checker substitutes the actual arguments into the return type, normalises with Cure.Types.Reduce, and resolves the result. Trivial arithmetic never touches the SMT solver.

  • Equality types let programs carry proofs that two terms are equal. refl(x) : Eq(T, x, x) is the single constructor; rewrite eq in expr is the single eliminator. Both vanish at runtime via the :cure_refl atom. The new Std.Equal module exposes refl, sym, trans, and cong.

The glue is a small terminating normaliser, Cure.Types.Reduce, that folds closed type-level arithmetic, booleans, comparisons, and pair projection. Vector(T, 2 + 3) is the same type as Vector(T, 5) -- no solver round-trip required.

Implicit arguments and the unification trace

Implicit arguments land with {T} braces:

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

At each call site, first-order unification with an occurs check (Cure.Types.Unify) solves the implicit from the explicit arguments. When it fails, Cure emits a :unification_trace pipeline event: the LSP renders it in hover, the CLI prints it in error output. You can see where the constraint died—which argument, which position, which prior substitution was responsible. Implicit parameters are erased at codegen: they cost nothing at runtime.

Hole-driven development

The most practical consequence of the dependent-types stack is that you can leave holes in your program and ask the type checker what to put there.

fn safe_head(xs: List(T)) -> T = ?body

Compile, and Cure tells you:

?body : T
in scope:
  xs : List(T)

Anonymous ?? holes are numbered ?_1, ?_2, ... in source order. Every hole encountered during checking emits a :hole_goal event carrying the goal type and the local context at the hole position. The REPL’s new :holes meta-command lists every hole recorded during the last evaluation. This is how Idris users write programs; it is now how Cure users can write programs.

Totality, done gently

A function is total when it terminates on every input and its pattern matching is exhaustive. Cure.Types.Totality classifies every function as :total, :partial, or :unknown, combining coverage (via Cure.Types.PatternChecker) with a structural-recursion check. The default is report-only; decorating with @total true upgrades the classification to a hard requirement:

@total true
fn factorial(n: Int) -> Int
  | 0 -> 1
  | n -> n * factorial(n - 1)

Direct structural recursion only in v0.17.0—mutual recursion joins the party in v0.18.0.

Path-sensitive refinement

The refinement system now flows along if and match guards.

if x != 0 then 100 / x else 0

Inside the then branch, Cure.Types.PathRefinement refines x to {x: Int | x != 0}, so the division is safe without an explicit refinement annotation. The new Std.Refine stdlib module provides drop-in refinements for everyday needs: NonZero, Positive, Negative, NonNegative, Percentage, Probability, and predicate helpers.

A real REPL

Cure.REPL is a complete rewrite. Multi-line input (terminated with a blank line or ;;), meta-commands :t, :doc, :effects, :load, :reload, :use, :holes, :env, :reset, :fmt, :help, :quit. Command history persists to ~/.cure_history. :t gives you the type; :effects gives you the inferred effect set; :doc prints the attached ## block; :holes lists the holes from the last evaluation with their goals and contexts.

Watch mode

cure watch lib/ --action check

Cure.Watch recompiles, type-checks, or runs tests on every save with a 200 ms debounce. No dependency on :file_system—a small polling fallback is included so it runs out of the box on any BEAM.

LSP polish

Cure.LSP.Server gains seven new capabilities at once:

  • Inlay hints (textDocument/inlayHint).
  • Signature help (textDocument/signatureHelp).
  • Formatting (textDocument/formatting) routed through the round-trip-tested Cure.Compiler.Printer.
  • prepareRename + rename (textDocument/rename).
  • Code lenses (textDocument/codeLens).
  • Semantic tokens (textDocument/semanticTokens/full).
  • Workspace symbols (workspace/symbol).

Unification traces and hole goals are rendered in hover; pattern coverage warnings appear as diagnostics.

Project, tooling, doctests

  • cure new <name> [--lib | --app | --fsm] with three project templates.
  • Cure.lock lockfile; cure deps update; cure deps tree; Cure.Project.resolve_git_dep/2 for git-based dependencies via git = "...", ref = "..." in Cure.toml.
  • cure bench—benchmark runner for bench/**/*.cure.
  • cure test --filter PATTERN --doctests.

Any ## or ### block immediately above a function whose body contains cure> / => pairs becomes a test case:

###
Adds two integers.

    cure> Demo.add(2, 3)
    => 5
###
fn add(a: Int, b: Int) -> Int = a + b

cure test --doctests runs them. The implementation lives in Cure.Doc.Doctests; a worked example is in examples/doctest_demo.cure.

Error catalog, doubled

Ten new codes (E011-E020) in Cure.Compiler.Errors cover implicit-argument failures, sigma destructuring, totality failures, unfilled holes, refinement counterexamples, dependent-type mismatches, equality proof mismatches, and doctest mismatches. Every code has a detailed explanation available via cure explain Eddd or cure why Eddd.

Language-layer polish

  • Fenced multi-line docstrings. ###...### now tokenises to a single :doc_comment with common leading indentation stripped. The single-line ## text form is unchanged and now composes correctly with multi-clause functions in every position.
  • Trailing ? on identifiers. even?, is_empty?, positive? lex and compile as single identifiers. ?name hole prefixes are preserved. ! stays reserved for effect annotations and FSM hard events.
  • Soft keywords as function names. fn spawn(...), fn send(...), fn receive(...) are accepted in definitions, so Std.Fsm compiles end-to-end without carve-outs.
  • @extern module-name resolution. Dotted PascalCase atoms like Elixir.Cure.FSM.Builtins now pass through cleanly.
  • Zero-warning codegen. Mangled variables preserve the user-visible _name shape (_V_name rather than V__name), so erl_lint never warns about deliberately unused parameters.

Ecosystem groundwork

  • MIT license—LICENSE at repo root.
  • Hex package metadata—mix.exs carries a full package block and a docs extras list (CHANGELOG, TUTORIAL, DEPENDENT_TYPES, ...).
  • VS Code extension scaffold—vscode-cure/ contains a TypeScript language-client wrapper, a TextMate grammar, language configuration, and a README. Marketplace publication is deferred to a later release; for now npm run compile && F5 gets you a working development host.
  • Package registry design—docs/PACKAGE_REGISTRY.md sketches the manifest, version-constraint solver, and index service that will land in v0.18.0+.

Regression CI

mix cure.check.stdlib     # 20 Std.* modules; errors and warnings fail
mix cure.check.examples   # 24 examples with per-file expected output
mix cure.check            # both, sequenced
mix check                 # mix alias: stdlib + cure.check

test/cure/regression_test.exs wraps both as :regression-tagged ExUnit tests so mix test surfaces them too. The GitHub Actions workflow (.github/workflows/ci.yml) runs the whole suite on every push and every pull request.

The numbers

  • ~11 new Elixir modules; ~12 new test files; ~155 new tests (830 total, 0 failures).
  • 2 new stdlib .cure modules (Std.Equal, Std.Refine); 20 total.
  • 7 new examples—one for every major new feature.
  • 3 new docs (DEPENDENT_TYPES.md, TUTORIAL.md, PACKAGE_REGISTRY.md) plus refreshed LANGUAGE_SPEC.md, TYPE_SYSTEM.md, STDLIB.md.
  • Zero credo issues in strict mode. mix format clean. mix compile --warnings-as-errors clean.
  • mix check green (20 stdlib + 24 examples).

Upgrade notes

v0.17.0 is source-compatible with v0.16.0. Three small nudges if you are porting existing code:

  1. The lexer now treats a trailing ? on an identifier as part of the name. x?y (no space) used to tokenise as three tokens; now x? is one identifier followed by y. Add whitespace (x ? y) or parentheses if you need the old behaviour.
  2. mix.exs version bumped to 0.17.0. If you depend on Cure via path, regenerate your downstream Cure.lock with mix cure.compile_stdlib && mix cure.check.
  3. Module-level docstrings written as ## ... lines between mod X and the first definition now reliably attach to the first definition inside the block. Previously they would sometimes silently drop. No change is required—behaviour is strictly more correct.

What’s next—v0.18.0 Bring the Furniture

The deferred "new ideas" from the v0.17.0 plan come home:

  • proof containers.
  • assert_type builtin.
  • Records with default field values.
  • Finished @derive(Show, Eq, Ord) on records.
  • Property-based testing in Std.Test.
  • Std.Iter lazy iterator protocol.
  • First half of the package registry—version-constraint parser, resolver, deeper Cure.lock semantics.
  • Mutual-recursion totality.

Acknowledgements

Thanks to the Finitomata project for the FSM inspiration that landed in v0.16.0 and continues to pay dividends, and to the Idris community for the hole-driven-development workflow this release adopts.

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.17.0
./cure repl             # new multi-line REPL with :t, :doc, :holes
./cure watch lib/       # recompile on save

The repository is at github.com/am-kantox/cure-lang. The rewrite is complete. The type system is honest. The tools work. Time to use the language.