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

Cure v0.17.0 -- Proofs & Polish

Toward Idris.
Cure is a dependently-typed programming language for the BEAM virtual
machine with first-class finite state machines and SMT-backed
verification.
v0.17.0 is the release where the type system grows up. Sigma types,
Pi types, propositional equality, implicit arguments, type-level
reduction, hole-driven development, and totality checking all land
together -- with a matching round of day-to-day quality-of-life
improvements and the first real regression CI.

Highlights

• Dependent-type core: Sigma, Pi, Eq, refl, rewrite,
  implicit {T} arguments, type-level Reduce, ?name / ??
  holes, Cure.Types.Totality, path-sensitive refinement.
• Friction-free UX: proper REPL (:t, :doc, :effects,
  :load, :reload, :use, :holes, :env, :reset, :fmt,
  :help, :quit, multi-line input, history), cure watch, LSP
  inlay hints + signature help + formatting + rename + code lenses +
  semantic tokens + workspace symbols, cure new project templates,
  Cure.lock, git dependencies, cure bench, cure test --filter
  and --doctests, doctest harvester, ten-chapter tutorial.
• Ecosystem groundwork: MIT license, mix.exs Hex package
  metadata, VS Code extension scaffold, package-registry design
  document.
• Quality engineering: mix cure.check runs the stdlib and
  example regression suites; CI gates every merge on it.

Dependent-type maturation

Sigma types

type Sized(T) = Sigma(n: Nat, Vector(T, n))

A Sigma type pairs a value with a type that depends on it. Recognised
by Type.resolve/1, subtyped componentwise, and convertible to and
from plain tuples.

Pi types

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

The return type may reference parameter names. At each call site the
checker substitutes the actual arguments, normalises the result with
Cure.Types.Reduce, and resolves it back to a concrete type. No SMT
call for trivial arithmetic cases.

Propositional equality

refl(x) : Eq(T, x, x)
rewrite eq in expr

Eq(T, a, b) is the type of proofs that a == b. refl(x) is the
only constructor, rewrite the only eliminator. All erased at
runtime via the :cure_refl atom. The new Std.Equal stdlib module
exposes refl, sym, trans, cong.

Implicit arguments

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

{T} introduces an implicit parameter. Cure.Types.Unify solves it
at every call site via first-order unification with an occurs check.
Failures emit a structured :unification_trace pipeline event the
LSP renders in hover and the CLI prints in errors. Implicit
parameters are erased at codegen: they cost nothing at runtime.

Hole-driven development

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

A ?name or ?? placeholder triggers a :hole_goal event carrying
the goal type and the local context at the hole position.
Anonymous ?? holes are numbered ?_1, ?_2, ... in source order.
The REPL's new :holes command lists every hole recorded during the
last evaluation.

Totality

#[total]
fn factorial(n: Int) -> Int
  | 0 -> 1
  | n -> n * factorial(n - 1)

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; #[total] upgrades the classification to a
hard requirement. Mutual recursion arrives in v0.18.0.

Path-sensitive refinement

if x != 0 then 100 / x else 0

Inside the then arm the checker refines x to
{x: Int | x != 0}, so the division is safe without an explicit
refinement annotation. See Cure.Types.PathRefinement and the new
Std.Refine stdlib module (NonZero, Positive, Percentage,
Probability, ...).

Friction-free UX

REPL

Complete rewrite. Multi-line input (terminate with blank line or
;;), meta-commands :t, :doc, :effects, :load, :reload,
:use, :holes, :env, :reset, :fmt, :help, :quit.
Command history persisted to ~/.cure_history.

Watch mode

cure watch lib/ --action check

Recompiles, type-checks, or runs tests on every save with a 200 ms
debounce. No dependency on :file_system; uses a small polling
fallback so it runs out of the box.

LSP polish

Cure.LSP.Server gains:

• 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).

Project & tooling

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

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. See
lib/cure/doc/doctests.ex and examples/doctest_demo.cure.

Error catalog

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

Tutorial

docs/TUTORIAL.md -- ten progressive chapters from "hello world" to
dependent pairs, Pi types, holes, totality, and FSMs.
docs/DEPENDENT_TYPES.md -- full reference for the new type-system
features.

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+.

Language-layer polish

• ###...### fenced multi-line docstrings -- a single
  :doc_comment token 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.
• @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 params.

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.

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.
• 0 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. The mix.exs version bumped to 0.17.0. If you depend on Cure
   via path, your downstream Cure.lock should be regenerated 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 pa...