canonical term algebra: labels, records, rationals, sequences

1 files changed, 48 insertions, 0 deletions

diff --git a/docs/terms.org b/docs/terms.org
new file mode 100644
index 0000000..638863d
--- /dev/null
+++ b/docs/terms.org
@@ -0,0 +1,48 @@
+#+TITLE: Terms
+
+* About
+
+This document describes =lib/label= and =lib/term=, the first modules
+of the Sol implementation. They realize the term algebra of the
+language specification and the canonical form discipline of decision
+12 in the integration document.
+
+* Labels
+
+A label names an attribute, like =age:= or =dept_id:=. The module
+validates on construction: lowercase first letter, then letters,
+digits or underscores. Since the type is sealed, holding a =Label.t=
+is proof the name is well formed. Labels carry a total order, and
+that order is what gives records a canonical attribute layout
+independent of how the source spelled them.
+
+* Terms
+
+A =Term.t= is a value of Sol: an integer, a rational, a string, the
+empty sequence =#()=, or a record (a labeled tuple). The type is
+exposed as private, so anyone can pattern match on it, but building
+one goes through the smart constructors. This is where the canonical
+form rules live:
+
+- rationals reduce by the gcd and carry the sign on the numerator;
+- a rational with denominator one collapses to the integer itself,
+  the minimal shape, so an integer valued rational is literally an
+  integer and inclusion of the integers in the rationals holds with
+  no coercion;
+- a denominator of zero is rejected at construction;
+- records reject duplicate labels instead of picking one, and reject
+  emptiness, since =#()= is the only empty term;
+- sequences are sugar: =#(1 2 3)= elaborates to nested
+  ={head: 1 tail: ...}= records ending in =#()=, exactly as the
+  specification publishes.
+
+Because every term is canonical by construction, structural equality
+is value equality. Content addressing later hashes terms directly and
+relies on this.
+
+* Printing
+
+Terms print back as Sol notation: =42=, =1/4=, ="Sun"=, =#()=,
+={a: 1 b: 2}=. A record chain shaped like a sequence prints as
+=#(1 2 3)=. An improper chain prints with an explicit dangling tail,
+=#(1 | X)=, so nothing pretends to be a proper list that is not.