From f7aa2d28053979f33d90a3c7bdec1ff6daa49b94 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 02:52:25 -0300 Subject: canonical term algebra: labels, records, rationals, sequences --- docs/terms.org | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 docs/terms.org (limited to 'docs') 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. -- cgit v1.2.3