Skip to content

Releases: sdiehl/prism

v0.3.0

28 Jun 23:14

Choose a tag to compare

  • New surface syntax, every form sugar over the existing core:
Sugar Desugars to
x += e (and -=, *=, %=) x := x <op> e
while cond do <block> repeat_while(\() -> cond, \() -> <block>)
loop <block> (may break) repeat_while(\() -> true, \() -> <block>)
loop <block> (no break) forever(\() -> <block>) (bottom-typed: never returns)
break / continue final ctl perform of an internal Break/Continue effect, handled at the loop
return e final ctl perform of an internal Return(a) effect, handled at the function body
a ^ b pow(a, b), the Pow class method (Int instance bignum-multiplies, Float is pow_float)
a[i] index(a, i), a failable read dispatched on a's head type (Elem ! {Fail})
a[i] := v a := index_set(a, i, v), the in-place (FBIP) setter, rebinding the var
a[i] += e (and -=, *=) a[i] := a[i] + e (the read makes it ! {Fail})
f(args, using d) explicit instance selection (the old f[d](args)), f's callee wrapped in the chosen dict
  • Indexing a[i] / a[i] := v / a[i] += e over Array (Int key), HashMap (String key), read-only String byte, and List, dispatched at elaboration on the receiver's head type (no new class). A missing index performs Fail (a[i] : Elem ! {Fail}), so it composes with ??/?./default; writes are FBIP-in-place when uniquely owned, and nested grid[i][j] := v composes.
  • Explicit instance selection moves from f[name] to f(args, using name), freeing [] for indexing and converging override with first-class dictionary passing; using is reserved.
  • Instance coherence: each (class, type-head) has one canonical instance that implicit resolution always selects, so ambiguity-at-use is gone. A lone instance is canonical by default; when several share a head one is named with a top-level canonical Class(Head) = name, and two undesignated instances are a coherence error at definition (caret plus designation hint). f(args, using name) stays the visible override, and a newtype is the way to a different default. No Core, runtime, or backend change, so the parity oracle is byte-identical. canonical is reserved.
  • A right-associative power operator ^ (tighter than *), the method of a new Pow class: 2 ^ 10 is bignum-correct Int, 2.0 ^ 10.0 is Float, mixed Int ^ Float a type error. The prior integer pow is now int_pow.
  • Imperative loops (while/loop) lower to a tail-recursive prelude driver (constant stack, no per-iteration allocation), an unconditional loop to the bottom-typed forever. break/continue/return compile to non-resumable performs of internal, fully-handled effects, so none surfaces in a function's row, and a loop installs a handler only for the keyword it uses. The prelude's old while is now repeat_while.
  • Principal effect-row inference: a lambda delimits its effects onto its own arrow row, the arrow is covariant in that row (a pure function fits any effectful context via row subsumption), and the call-graph set pass is dropped as a row seed so the inferred row is the single source of truth. Builtins carry their effect row on the type, so inference attributes IO/Exn/Fail directly; rows display in canonical name-sorted order; and definitions are inferred in dependency-SCC order so a forward reference sees a generalized type.
  • mask over the sole handler of an effect now leaves the operation genuinely unhandled (the label stays in the row) instead of inferring it pure and hitting an effect-reconciliation ICE at lowering.
  • Two source warnings (the prelude is exempt): an unused local binding and a name shadowing one in scope (a leading _ and a consuming rebind let s = f(s) are exempt). Annotations are name-checked uniformly across parameters, returns, constraints, and rows: an undeclared effect or constructor is a hard error, and an annotation broader than the inferred row warns.
  • Standard library split into on-demand modules under lib/std (Data.Char/List/Map/Maybe/Result/Set/String), shrinking the always-loaded prelude; Set gains set_union/set_intersection/set_difference, and a project may replace the built-in prelude via [package] prelude in prism.toml.
  • CLI: a bare prism program.pr compiles a single file to a native binary named after the source (-o overrides, --mlir selects the backend); prism build is the project verb (nearest prism.toml) and interpreting is explicit via prism run.
  • Local monadification confines the free-monad form to the component entangled with an escaping effect, keeping unrelated functions on their fused evidence/state path and falling back to whole-program lowering only when the split is unclean. The fallback now warns on stderr by default (silence with PRISM_QUIET), naming the functions that lost fusion.
  • Constant-stack effect handlers: a closed free-monad handler is driven by one self-tail-recursive {n}@region loop, so a tail-resumptive or function-answer state handler resumes via musttail in constant native stack (a perf_gate State loop goes from ~10^5 to millions of iterations in a 2 MB stack). On by default (opt out with PRISM_NATIVE_EFFECTS=0); it changes the driver, not the one-EOp-cell-per-operation reification.
  • Compiler-internal correctness, with no change to accepted programs or output: existential scope is enforced unconditionally at solve; numeric defaulting is deferred to one pass at generalization; and FBIP reuse becomes a scoped WithReuse/Reuse core node, making free-once and spend-at-one-allocation well-formedness properties of the term.
  • The Lean core model (models/) grows from a substitution small-step into a mechanized CEK machine proved to implement a big-step semantics, with unique normal forms, a progress trichotomy, and effect progress/unhandled lemmas, all sorry-free over propext/Quot.sound. It runs as a third differential oracle via a new prism dump core-json phase, checked against the interpreter across a fixture corpus.
  • Hardening: the bignum allocator is overflow-checked like every cell, each builtin's calling convention is derived from an exhaustive Builtin method (so a new builtin cannot ship without declaring its ABI), and the reference grammar is single-sourced in models/grammar.ebnf, sliced into the spec by mdbook anchors.

v0.2.0

25 Jun 10:31
c56b8f5

Choose a tag to compare

0.2.0

  • Fixed-width bitwise and shift builtins on the I64/U64 lanes: i64_and/i64_or/i64_xor/i64_shl/i64_shr and their u64_* counterparts. and/or/xor share one bit pattern across lanes; i64_shr is arithmetic, u64_shr logical; shift counts are taken modulo 64.
  • system(String) -> Int runs a shell command and returns its exit code, and eprint/eprintln write to stderr, so a program can drive external tools and emit diagnostics off the stdout stream.
  • Superclasses: a class may declare another as a superclass (class Ord(a) given Eq(a)). Each instance carries a resolved superclass dictionary as a leading field of its dict cell, and a given Ord(a) constraint discharges an Eq(a) obligation by projecting it, found automatically from the instances in scope. The prelude's Ord now requires Eq.
  • Growable mutable Array(a) (array_new/array_empty/array_len/array_get/array_set/array_push), an ordinary reference-counted heap cell so drops recurse into its elements. array_set and array_push write in place when the array is uniquely owned (FBIP) and copy otherwise; array_push doubles capacity when full, so appends are amortized O(1). The prelude adds array_of_list.
  • string_of_array and the prelude concat_all/array_of_list build a string from many chunks in a single allocation, replacing the quadratic right-nested concat chain.
  • Prelude HashMap(v): a separate-chaining hash table with String keys built on the growable array (hm_new/hm_insert/hm_lookup/hm_member/hm_get_or/hm_keys/hm_values/hm_size/hm_to_list/hm_delete/hm_from_list/hm_adjust), doubling its bucket count past load factor 1. Keys hash by a fixed-width FNV-1a written in the language, so iteration order is a deterministic function of the inserts.
  • O(1) byte access: byte_at/byte_len (UTF-8 unaware) and string_of_bytes, so a lexer or hash scans raw bytes in linear time. array_pop rounds out the array API, and array_foldl/array_to_list are added to the prelude.
  • Surface fixed-width arithmetic: i64_*/u64_* add/sub/mul/div/rem/cmp (wrapping, no bignum promotion), enabling a real fixed-width hash in userland.
  • Higher-kinded types: a class parameter may range over a type constructor (kind * -> *), applied as f(a) in method signatures, with instance resolution keyed on the head constructor. The prelude adds the Functor/Applicative/Monad/Foldable/Traversable tower with List and Option instances. fmap/traverse are effect-polymorphic, so the per-element effect row threads through instead of an Applicative wrapper (effects, not do-notation).
  • String-utility prelude: character classifiers (is_digit/is_alpha/is_alnum/is_space/is_upper/is_lower, to_upper_c/to_lower_c), starts_with/ends_with/contains/index_of, to_upper/to_lower/trim, and args().
  • prism fmt separates top-level declarations with a blank line.
  • Editor tooling: a dependency-free Neovim highlighter under scripts/nvim/ (an ftdetect/ filetype map for *.pr plus a syntax/ highlighter), with its keyword set mirrored from src/lex/token.rs so it tracks the lexer.
  • A project and module system. A prism.toml manifest ([package] name, [bin] entry) plus a src/ tree make a multi-file project that prism run/build compiles, resolving module paths from the project root rather than the entry file's directory (single-file invocation is unchanged). Name resolution now canonicalizes every top-level definition to a module-qualified symbol (Data.Map.insert for exports, Data.Map@helper for privates), so qualified references (M.x) reach disjoint namespaces and two modules may export the same short name and coexist; selective imports (import M (a, b)) bring only the listed names into bare scope, and pub controls what an importer can reach. Instances record their defining module: an orphan instance (defined apart from both its class and its type) and instances overlapping across modules are reported as warnings, and an ambiguity names each candidate's module.
  • Module-system follow-ups: pub import M (x) re-exports the named items through the importing module, with chains resolving transitively to the original definition; a module's full dotted path qualifies a reference (Geo.Util.one), not only its last component (Util.one); and orphan/overlapping-instance warnings render with a source caret when they point into the program being compiled.
  • Static fip/fbip checking of the FP^2 discipline. fbip proves zero fresh allocation and that an annotated body calls only annotated, allocation-free functions; fip additionally proves linearity (each owned non-immediate binding consumed at most once, checked on the source term with scalars exempt) and bounded stack (every recursive call in the call-graph SCC is a tail call or a single tail-modulo-cons/-add). The tail/TRMC classification is shared with codegen (src/core/tailrec.rs), so an accepted fip function always lowers to a loop; fip may call only fip, fbip may call either. Recursive accumulator/TRMC functions like rev_onto and bump now type-check as fip and run in constant heap and stack.
  • A cyclic superclass hierarchy (class A given B, class B given A) is now reported as a superclass cycle: A -> B -> A error at class-construction time, instead of overflowing the stack the first time the chain is walked at a use site.
  • Pattern coverage now treats an irrefutable if true guard as always-matching: such an arm completes exhaustiveness like an unguarded one (no spurious non-exhaustive error) and shadows any later arm (which is reported unreachable). Fallible guards keep their conservative non-covering treatment.
  • The fip bounded-stack rejection now explains when a function joins the tail-recursion group only because another function flows as a first-class value (a capture) rather than through a direct call cycle, pointing at the fix (call directly or annotate fbip). The set of accepted programs is unchanged; only the diagnostic is sharper.
  • Rank-N polymorphism is predicative: a forall written directly as a type-constructor argument (List(forall a. (a) -> a)) is now rejected at the annotation with a clear "impredicative type" message naming the constructor, instead of surfacing later as a confusing expected a, got Int mismatch from a leaked rigid variable. Higher-rank types remain available as function parameters, results, and declared data fields (a polymorphic field carries a forall through a generic container).

v0.1.0

20 Jun 16:11

Choose a tag to compare

0.1.0

Initial release.

  • Strict, impure functional language with ML-family surface syntax: ADTs, pattern matching, parametric polymorphism, and a prelude of Option/Result/List/Map combinators.
  • Hindley-Milner type inference with bidirectional, higher-rank (rank-N) checking and subsumption.
  • Type classes by dictionary passing, with named instances and deriving (Eq, Ord, Show).
  • Algebraic effects and handlers: inferred, extensible effect rows via row polymorphism; multishot resume; final ctl non-resumable clauses; scoped/masked handlers and forwarding.
  • Evidence-passing compilation of handlers, with tail-resumptive clauses lowered to direct calls and a free-monad fallback when effects escape tracking.
  • Exhaustiveness and redundancy checking, plus decision-tree pattern-match compilation.
  • First-class optics: record-update paths, view patterns, bidirectional pattern synonyms, and deriving (Lens).
  • Stream fusion: effectful producer/transformer/consumer pipelines fuse to zero intermediate allocations.
  • Verse-inspired failure model (fail, guard, ??, ?., transact) and structured error handling, both built on effect handlers.
  • Deterministic memory management via Perceus reference counting with in-place reuse (FBIP), no garbage collector.
  • Call-by-push-value core in A-normal form with tail-call optimization and tail recursion modulo cons.
  • Three backends kept byte-identical: a tree-walking interpreter, native code via LLVM, and a text-MLIR backend.
  • Lean model of the core with a machine-checked determinism theorem.
  • Compiles to WebAssembly, so the language runs in the browser.
  • Tooling: interactive shell, run, build, check, fmt, and phase dump.