Skip to content

Latest commit

 

History

103 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

gen-algebra — pure algebraic primitives for Nix

CI License: MIT Sponsor

Foundational primitives for the gen family: a Palmer §3 search monad, intensional functions, standalone identity hashing, record algebra with scoped labels, and Either combinators.

Class A (pure, zero-input). gen-algebra declares no flake inputs and depends on nothing — not even nixpkgs lib; it is builtins-only and sits at the pure-algebra root of the ecosystem. A CI purity invariant (ci/tests/purity.nix) enforces this: any stray lib.types / mkOption / evalModules in the library source fails the suite.

Table of Contents

Overview

gen-algebra is a fully pure Nix library — zero dependencies, builtins only. Search monad for indexed state threading with convergence. Intensional function constructors for conservative equality (Palmer §2.2-2.3). Record algebra with scoped labels (Leijen §2) and mixin composition (Bracha §2-4). Either combinators. Standalone identity hashing.

The module-system tier (identity/strict/validators/cross-registry refs for lib.evalModules) relocated to gen-schema, its sole consumer; gen-algebra is the ecosystem's pure-algebra root. Its former pure tier is now simply the lib output — everything gen-algebra ships is pure.

Extraction Lineage

flake-aspects ──→ gen-algebra.search, gen-algebra.mkIntensional, gen-algebra.conservativeEq
                    ↓
              gen-schema (typed registries on gen-algebra primitives;
                          owns the module-system tier — identity/strict/validators/refs)
                    ↓
              gen-aspects (aspect composition on gen-algebra + gen-schema)
                    ↓
                   den (system configuration framework)

gen-algebra has zero flake inputs — this lineage shows where each primitive was extracted from and who consumes gen-algebra downstream, not runtime dependencies.

Gen Ecosystem

Library Role
gen-prelude Pure nixpkgs-lib-free utility base (builtins re-exports + vendored lib utils)
gen-algebra This lib — Pure primitives (record, search monad, either, intensional identity)
gen-types Clean-room MIT structural type checker (leaf/poly checkers; verify: v → null|err)
gen-merge Byte-mode module merge engine (evalModuleTree, byte-identical to nixpkgs lib.evalModules over the priority subset)
gen-schema Typed registries (kinds, instances, collections, refs); re-hosted on gen-merge
gen-aspects Aspect type system (traits, classification, dispatch); re-hosted on gen-merge
gen-scope HOAG scope-graph evaluator (demand-driven, _eval memoization, circular attributes)
gen-graph Accessor-based graph query combinators (traversal, condensation, phaseOrder)
gen-select Selector algebra (pattern matching over graph positions)
gen-bind Module binding (inject external args into NixOS modules)
gen-dispatch Relational rule dispatch STEP (stratified phases, conflict resolution)
gen-memo The incremental plane — decides reuse, never evaluates (change propagation, AFFECTED set)
gen-vars Pure-Nix vars/secrets (den-agnostic)

Quick Start

As a flake input

{
  inputs.gen.url = "github:sini/gen-algebra";

  outputs = { gen, ... }:
    let
      # Fully pure — no lib needed. Everything is under the `lib` output.
      search = gen.lib.search;
      inherit (gen.lib)
        mkIntensional
        conservativeEq
        record
        either
        ;
    in
    { /* ... */ };
}

Without flakes

let
  # Fully pure — no nixpkgs / lib needed. The non-flake entry (default.nix = import ./lib)
  # is the lib value itself, not a function — so no argument is applied.
  gen = import ./path/to/gen-algebra;
in
{
  inherit (gen) search record either mkIntensional;
}
# gen.search.empty, gen.record.fromAttrs, gen.either.right, … all `builtins`-only.

API Reference

Every exported name is documented below, grouped by primitive family. The full surface is search (8), record (26), either (6), plus top-level mkIntensional, conservativeEq and the four identity-regime readers (identityOf, regimeTagOf, isExact, comparisonSubject) — verified against nix eval .#lib.

Search Monad

An indexed state monad for monotonic data accumulation with continuation-driven convergence. Zero dependencies — pure builtins.

empty

Initial state with empty index, results, and continuations.

search.empty
# → { index = {}; results = []; continuations = []; }

insert

Add a value to a key in the index. Values accumulate — multiple inserts to the same key append.

s = search.insert "users" "alice" search.empty;
search.insert "users" "bob" s;
# index.users → [ "alice" "bob" ]

lookup

Retrieve values for a key. Returns [] for absent keys.

search.lookup "users" (search.insert "users" "alice" search.empty)
# → [ "alice" ]

search.lookup "missing" search.empty
# → []

has

Check if a key exists in the index.

search.has "users" (search.insert "users" "alice" search.empty)
# → true

search.has "users" search.empty
# → false

emit

Append items to the results list.

s = search.emit [ "a" "b" ] search.empty;
(search.emit [ "c" ] s).results
# → [ "a" "b" "c" ]

foldl

builtins.foldl' — thread state through a list of values.

search.foldl (acc: item:
  search.insert item true (search.emit [ item ] acc)
) search.empty [ "a" "b" "c" ]
# results → [ "a" "b" "c" ], index has "a", "b", "c"

on

Register a continuation that fires when a key has unprocessed values during converge.

s0 = search.insert "users" "alice" search.empty;
s1 = search.on "users" (name: s: search.emit [ "hello:${name}" ] s) s0;
(search.converge s1).results
# → [ "hello:alice" ]

converge

Fixed-point convergence: fires all registered continuations on unprocessed values, repeats until stable. Safety guard at 1000 iterations.

Continuations registered during convergence (via on inside a continuation body) fire in subsequent rounds. Intensional continuations (created with mkIntensional) watching the same index key are deduplicated by identity regime: where the wrapped value carries a minted identity the key is exact and presence decides, and otherwise the key is a bucket whose membership is decided by Nix == on the reified value minus __id.

That distinction is load-bearing. A program point is constant across a constructor's instances, so a name-only key merged continuations that behave differently and dropped one silently; the bucket keeps both. The bucket's precision is an allocation artefact — one value registered twice dedups, two separately-constructed equal-shaped values do not — and since converge merges work, a finer relation costs dedup and never correctness.

Every key also carries a one-character regime tag between the index key and the payload, so the three arms occupy disjoint key spaces. Without it a continuation merely named string-equal to another's minted digest lands on that digest's key and one of the two is dropped — and the drop is order-sensitive, so a probe that registers them in only one order reads clean.

__id is excluded from the compared value, and it is the only exclusion. It is an accessor rather than distinguishing content, and where nothing is minted that accessor is the named refusal, so forcing it inside a bucket scan would detonate the decision the refusal exists to permit. One exclusion suffices: __mint.minted is the only other refusal-valued accessor, and the tagged sum shields it — its minted and sealed arms live under different key names, and Nix == decides on the name set before forcing any value.

# Multi-round: A inserts data, B watches data
s0 = search.insert "trigger" "go" search.empty;
s1 = search.on "trigger" (v: s: search.insert "data" "from-A" s) s0;
s2 = search.on "data" (v: s: search.emit [ "B-saw:${v}" ] s) s1;
(search.converge s2).results
# → [ "B-saw:from-A" ]

Intensional Functions

Palmer §2.2-2.3: function wrappers with program-point identity, built by an encoder rather than assembled by the caller. Palmer discharges his closure-consistency requirements by construction at an encoder and never by a check, and this constructor is that transposed: the author names a constructor and an inert argument value, and a registry supplies the body.

mkIntensional

mkIntensional : hashIdentity -> registry -> ctor -> args -> intensional

registry is { revision; members; }, where members maps a constructor name to a builder over the inert argument value. revision is required and total — a registry without one is refused by name at construction, never defaulted.

registry = {
  revision = "r1";
  members.addN = args: (x: x + args.n);
};
mk = mkIntensional genIdentity.hashIdentity registry;

fn = mk "addN" { n = 1; };
fn 5           # → 6 (callable via __functor)
fn.name        # → "addN" (the program point, DERIVED from the constructor)
fn.closure     # → { n = 1; } (the reified argument value — it IS `args`)
fn.__mint      # → { minted = "its:…"; } (lazy: an unread identity hashes nothing)

The mint is injected. hashIdentity is the substrate's one minting authority and it lives in gen-identity, a dependency-free leaf. It was gen-schema's, downstream of gen-algebra, and importing it would have closed a flake dependency cycle — which is why the injection exists and why the authority became a leaf. Taking it as a constructor parameter mints the value inside the consumer's own eval — the identity is owned rather than borrowed, and gen-algebra keeps its zero-dependency property.

There is no closure argument to under-supply. The shipped constructor took the name and the closure from the caller, so an under-complete closure was undetectable and two bodies could share one program point. Here both are derived: name = ctor, closure = args.

The registry construction is Lorenzen's lazy constructor (§1). A lazy constructor holds inert first-order operands and no behaviour; the behaviour is "the associated right-hand side of the data declaration", looked up by constructor when forcing arrives. { ctor; args; } is inert, fn = registry.members.<ctor> args resolves only at demand, and no other field forces it — so the operands are readable on a value nobody has applied, as Lorenzen's debug-show reads a lazy constructor without forcing it. Where the two part company is openness: §8 records that lazy constructors "have to be declared up-front in the data type definition", so one declaration site fixes the whole map and no coordinate is needed to say which map was meant. Here the registry is a value a caller supplies, which is exactly why revision has to enter the identity coordinate below.

Reynolds is the constructor-plus-inert-argument shape only (§6, pp. 376-377) — not this registry. His record fields are read off the lambda's own global variables (§6's table gives one record equation per lambda expression) rather than chosen by a caller; elimination is a single interpretive apply doing closed case analysis over FUNVAL = CLOSR ∪ SC ∪ EQ1 ∪ EQ2, where dispatch here is an attribute selection into an open map; and that union is enumerated from every lambda expression in the program, making it a whole-program transformation with no registry to pass.

The identity coordinate is (registry, ctor, args). The registry term is not decoration — Nix has no linking, so a builder's free variables include its registry module instance's whole lexical scope. Without it, two pins of the substrate give the same ctor and the same args one identity for two behaviours.

conservativeEq

Palmer's own term (§2.3, §5.3, §8) — "intensional" qualifies the function, never the equality. Fig. 5 is a conjunction over identity AND closure, and the relation this replaces shipped the first conjunct alone, which coarsens: it called behaviourally distinct functions equal, the one direction §2.3's guarantee forbids.

a = mk "addN" { n = 1; };
b = mk "addN" { n = 2; };
conservativeEq a b   # → false — one program point, two substitutions, two behaviours
a 5                  # → 6
b 5                  # → 7

c = mk "addN" { n = 1; };
conservativeEq a c   # → true — independently constructed, one coordinate, one identity

The relation dispatches on the identity regime rather than reading one field. Where both sides carry a minted identity the digests decide; where nothing is minted it compares the reified value minus __id, never a list of components — an attribute selection is an indirection, so a component-wise form is false even against itself and the relation would be empty rather than finer. That form's precision is an allocation artefact and is declared as such: it merges strictly less than Fig. 5 and never more.

__id is excluded because it is the accessor a consumer reads when it demands an identity, and where nothing is minted that accessor is the named refusal itself.

Continuation dedup in search.converge shares this discipline rather than calling conservativeEq: it keys exactly where an identity is minted and buckets otherwise, with every key carrying a regime tag so the three arms occupy disjoint key spaces.

Record Algebra

A record algebra with scoped labels (Leijen §2) and mixin composition (Bracha §2-4). Records support duplicate labels via shadow stacks — extending with an existing label pushes a new value, restriction pops it, exposing the previous value.

All operations are in gen-algebra.record (import path) — or inputs.gen-algebra.lib.record via the flake output. Zero dependencies.

Representation

Records use an attrset-with-shadow-stack representation for O(1) select:

# Internal: { __entries = { label = [value-stack]; }; __order = [labels]; }
r = record.fromAttrs { port = 8080; hostname = "localhost"; };
record.select r "port"      # → 8080
record.emit r                # → { port = 8080; hostname = "localhost"; }

Core primitives (Leijen §2)

record.empty                         # empty record
record.extend r "x" 42              # push value onto label's stack
record.select r "x"                  # head of stack (throws if absent)
record.restrict r "x"               # pop head (no-op if absent)
record.has r "x"                     # bool: label present?
record.depth r "x"                   # stack depth (0 if absent)

Scoped labels

# Duplicate labels form a stack — restriction exposes previous values
base = record.fromAttrs { level = "info"; };
env  = record.extend base "level" "warn";
user = record.extend env "level" "debug";

record.select user "level"                                      # → "debug"
record.select (record.restrict user "level") "level"            # → "warn"
record.select (record.restrict (record.restrict user "level") "level") "level"  # → "info"

Conversion

record.emit r                  # → plain attrset (heads only)
record.emitAll r [ "validators" ]  # → full stacks for listed labels, heads for rest
record.fromAttrs { a = 1; }   # → record with single-element stacks
record.show r                  # → "{ x = [2, 1]; y = [3] }" (full stacks)
record.showCompact r           # → "{ x = 2; y = 3 }" (heads only)

Derived operations

record.update r "x" 99        # replace head (throws if absent — strict)
record.upsert r "x" 99        # insert-or-update (no error)
record.rename r "old" "new"   # move label
record.labels r                # label names in insertion order

Composition (Bracha §2-4)

# Left-biased combination (⊕): a's values shadow b's
record.combine a b

# Smalltalk direction: delta wins over parent
record.mixin delta parent      # → combine (delta parent) parent

# Beta direction: parent controls, delta extends
record.mixinBeta prefix suffix

# Associative mixin composition (⋆)
record.compose m1 m2           # → fun(i) m1(m2(i) ⊕ i) ⊕ m2(i)

Row compatibility

record.satisfies r [ "port" "hostname" ]      # → bool
record.assertSatisfies r [ "port" "hostname" ] # → r or throws with missing fields

foldLayers

Fold ordered layers with per-field merge strategies. Useful for composing configuration from multiple priority tiers (e.g. defaults, system, user overrides) where different fields need different merge semantics.

Pure — builtins only, no lib dependency.

record.foldLayers {
  strategies ? {};   # field name → "replace" | "append" | "recursive"
  defaults ? {};     # fallback values for fields absent from all layers
  layers ? [];       # list of attrsets, least-specific first (base before overrides, last wins)
}

Strategy types:

  • "replace" (default) — last layer providing the field wins. CSS cascade order: later overrides earlier.
  • "append" — list concatenation across all layers in order, starting from defaults. Result: defaults ++ layer1 ++ layer2 ++ ...
  • "recursive" — nested attrset merge (//) across layers in order. Later layers override earlier keys.
  • "semilattice-set" — list-valued fields merged by set-union: fold each layer's elements into the accumulator, skipping any already present (dedup by builtins.elem). Unlike the three above — which are associative but order-sensitive (replace and append both depend on layer order, recursive on override order) — set-union is ACI: associative, commutative, and idempotent. The result is the layers' elements viewed as a set, so it is invariant under layer reordering and under duplicate contributions. This is the join of a set-union join-semilattice (∪ over finite sets); it is the strategy that lets foldLayersTraced stand in for the "semi-naïve evaluation over a lattice" merge of Datafun (ICFP 2016) and Flix (PLDI 2016), where a relation's value is the least upper bound of its contributions rather than a last-writer-wins cell.
record.foldLayers {
  strategies = {
    tags = "append";
    settings = "recursive";
    # name uses default "replace"
  };
  defaults = {
    tags = [ "base" ];
    settings = { verbose = false; };
  };
  layers = [
    # layer 0: lower priority (system)
    { name = "default"; tags = [ "system" ]; settings = { verbose = true; pager = "less"; }; }
    # layer 1: highest priority (user)
    { name = "custom"; tags = [ "user" ]; settings = { color = true; }; }
  ];
}
# → {
#   name = "custom";                                     # replace: last layer wins
#   tags = [ "base" "system" "user" ];                   # append: defaults ++ layers in order
#   settings = { verbose = true; pager = "less"; color = true; };  # recursive: merge in order
# }

foldLayersTraced

Single-pass variant of foldLayers that also returns per-field provenance. Takes additional layerNames (opaque labels aligned 1:1 with layers, least-specific first), optional defaultLabel, and optional entryTransform; returns { value; provenance; } where provenance.<field> is an ordered list of { layer; value; } (default first when present, then each contributing layer). Any value is admissible as a layer name; the fold stores each verbatim into provenance.<field>[].layer and never reads one. Powers settings stratification.

record.foldLayersTraced {
  strategies = { tags = "append"; };
  defaults = { tags = [ "base" ]; };
  layers = [ { tags = [ "system" ]; } { tags = [ "user" ]; } ];
  layerNames = [ "system" "user" ];
}
# → { value = { tags = [ "base" "system" "user" ]; };
#     provenance.tags = [ { layer = "default"; value = [ "base" ]; }
#                         { layer = "system"; value = [ "system" ]; }
#                         { layer = "user"; value = [ "user" ]; } ]; }

The value agrees with foldLayers on the strategies both accept, and only there. Over "replace" — declared explicitly or reached by omission — "append", "recursive", and a field carried by defaults alone, the two return byte-identical values for the same strategies, defaults and layers; the value-identity guards in ci/tests/rec-fold-layers-traced.nix hold exactly that. They are not one primitive with two return shapes: "semilattice-set" resolves here and foldLayers refuses it. Computing an expected value from the untraced sibling is licensed on the shared domain and nowhere else.

entryTransform — refining the emission, per entry, on demand

entryTransform is an optional field -> entry -> entry' applied to every entry of a field's chain, the default entry included. It is for a caller that wants a derived reading of each entry — the entry's value under some substitution the caller owns — to be emitted by the fold rather than re-mapped over its output afterwards. The fold hands over the field name and learns nothing in return: the transform is opaque to it, exactly as layer labels are.

record.foldLayersTraced {
  defaults = { font = "unset"; };
  layers = [ { font = "mono"; } ];
  layerNames = [ "host" ];
  entryTransform = field: entry: { inherit (entry) layer; resolved = lookup field entry.value; };
}
# → provenance.font = [ { layer = "default"; resolved = <thunk>; }
#                       { layer = "host";    resolved = <thunk>; } ]

Non-interference. Application is per entry and demand-driven (call-by-need, Launchbury 1993 §2). Forcing a chain's spine, one entry's own transformed record, or any sibling entry never applies the transform to another entry, and forcing .value never applies it at all. So a transform that is lazy in its derived part keeps a diverging entry — one whose refinement throws, because it points at something absent — harmless to the rest of the trace: the chain still has a length, the entry still reports which layer it came from, its siblings still resolve. That property, not the hook, is the capability; it is what a consumer-side map over the finished provenance cannot give you. Omitting entryTransform emits the chain untransformed with no per-entry application.

Nested-layer variants

flattenAttrs, unflattenAttrs, and foldNestedLayers extend layer folding to nested attrsets. foldNestedLayers is foldLayers for nested structures (flatten → foldLayers → unflatten); flattenAttrs/unflattenAttrs are its dot-separated-key flatten/rebuild primitives (flattenAttrs halts recursion at fields whose strategy is "recursive").

Either Combinators

Short-circuit and accumulating error handling via { right = value; } | { left = error; }. Zero dependencies.

All operations are in gen-algebra.either (import path) — or inputs.gen-algebra.lib.either via the flake output.

right / left

Construct Either values.

either.right 42      # → { right = 42; }
either.left "oops"   # → { left = "oops"; }

pipe

Short-circuit chain: first left stops the pipeline.

either.pipe [
  (x: if x > 0 then either.right (x * 2) else either.left "must be positive")
  (x: if x < 100 then either.right x else either.left "too large")
] 5
# → { right = 10; }

collectErrors

Accumulate all errors without short-circuiting.

either.collectErrors [
  (x: if x > 0 then either.right x else either.left "must be positive")
  (x: if x > -3 then either.right x else either.left "must be > -3")
] (-5)
# → { left = [ "must be positive" "must be > -3" ]; }

mapR

Map over the right value, passing left through unchanged.

either.mapR (x: x + 1) (either.right 41)   # → { right = 42; }
either.mapR (x: x + 1) (either.left "err")  # → { left = "err"; }

chain

FlatMap on right — apply a function that returns a new Either.

either.chain (x: if x > 0 then either.right (x * 10) else either.left "neg") (either.right 3)
# → { right = 30; }

Demo

See examples/demo/ for a self-contained example exercising search monad workflow, intensional dedup, record algebra, and either combinators.

cd examples/demo
nix eval --override-input gen-algebra ../.. .#searchResult
nix eval --override-input gen-algebra ../.. .#dedupResult
nix eval --override-input gen-algebra ../.. .#scopedLabels
nix eval --override-input gen-algebra ../.. .#eitherDemo

Architecture

gen-algebra/
  default.nix              — non-flake entry (bare lib value: import ./lib, no argument)
  flake.nix                — flake output (single `lib` value, no __functor)
  lib/
    default.nix            — exports search + intensional + either + record
    search.nix             — Palmer §3 Search monad (8 public primitives)
    intensional.nix        — mkIntensional, conservativeEq, the identity-regime discipline
    either.nix             — Either combinators (right, left, pipe, collectErrors, mapR, chain)
    rec.nix                — Leijen §2 record algebra with scoped labels + Bracha §2-4 mixin composition + foldLayers
  ci/                      — nix-unit test suite (incl. the purity invariant)
  examples/
    demo/                  — self-contained demo (search + dedup + records + either)

gen-algebra is fully pure — zero dependencies of any kind, not even nixpkgs lib. The CI purity invariant (ci/tests/purity.nix) enforces this: a stray lib.types / mkOption / evalModules in the library source fails the suite. The module-system tier relocated to gen-schema, its sole consumer.

Testing

Tests live in ci/ and run under nix-unit (via gen.lib.mkCi). 154 test cases across 12 suites (either, intensional, purity, rec-primitives, rec-derived, rec-row, rec-composition, rec-fold-layers, rec-fold-layers-traced, rec-nested-layers, search-primitives, search-converge), including the purity invariant that fails on any stray lib.types / mkOption / evalModules in the library source. Requires nix-unit.

# all suites
nix flake check --override-input gen-algebra . ./ci

# one suite (nix-unit)
nix-unit --flake ./ci#tests.rec-composition --override-input gen-algebra .

Theoretical Foundations

Paper Relationship Used for
Palmer et al. (2024) Intensional Functions Informed by Search monad with continuation dedup (§3); the three intensional eliminators __functor/name/closure (§2.2-2.3). The constructor is an encoder (§5's Def 5.5–5.7 discharged by construction, as Palmer discharges them, rather than by a check), and both dedup and conservativeEq are regime-dispatched — exact where an identity is minted, a bucket or whole-value == otherwise — because Fig. 5 is a conjunction and the name-only relation gen used to ship merged behaviourally distinct functions. The closure-consistency hypotheses discharge CONDITIONALLY, on the registry revision a declaration can get wrong; the condition disappears only when builders become first-order terms. Theorem 1 does not transfer at all: it is a preservation theorem about 𝜆ITS reduction and gen is not 𝜆ITS.
Lorenzen et al. (2025) First-Class Labels: First-Order Laziness Implements The registry construction in lib/intensional.nix is a lazy constructor (§1): inert first-order operands, with behaviour "the associated right-hand side of the data declaration" looked up by constructor at forcing, and the operands readable before anything is forced. The mechanism was identified at the landed construction rather than derived from the paper, and the fit is exact for §1's construct alone — none of the paper's memoization, in-place reuse or reference-counting results are claimed. Where the two part company is openness: §8 records the up-front data-type declaration as a limitation, and it is precisely because gen's registry is an open caller-supplied value that revision must enter the identity coordinate.
Reynolds (1972) Definitional Interpreters for Higher-Order Programming Languages Informed by The constructor-plus-inert-argument shape only (§6, pp. 376-377) — replace a function value by a tag plus inert fields and interpret the tag. Scoped deliberately: his record fields are read off the lambda's own global variables (§6's one-record-equation-per-lambda table) where an author here chooses args; elimination is a single interpretive apply doing closed case analysis over FUNVAL = CLOSR ∪ SC ∪ EQ1 ∪ EQ2 where dispatch here selects into an open map; and the union is enumerated from every lambda in the program, so it is a whole-program transformation with no registry.
Leijen (2005) Extensible Records with Scoped Labels Implements Record algebra with extension/selection/restriction (§2), scoped labels via shadow stacks (§2.1-3.2), row compatibility checks (§3.1)
Bracha & Cook (1990) Mixin-Based Inheritance Implements Left-biased combination (§2.1 ⊕ operator), Smalltalk-direction mixin (§2.1), Beta-direction mixin (§2.2), associative mixin composition ⋆ (§4)

Implements means the code directly realizes the paper's constructs (lib/search.nix + lib/intensional.nix for Palmer's search monad and intensional structure and for Lorenzen's lazy constructor; lib/rec.nix for Leijen and Bracha). One caveat on the Palmer row: conservativeEq dispatches on the identity regime and merges strictly less than Fig. 5 rather than realizing it, the closure-consistency hypotheses discharge only conditionally — on a registry revision an author can get wrong — and Theorem 1 does not transfer at all. See Intensional Functions.

About

gen-algebra: pure Nix primitives — search monad, intensional functions, record algebra, validators

Resources

Stars

5 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages