diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2025-12-01 18:34:31 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2025-12-01 18:34:31 -0300 |
| commit | 8c8b32d59acc78c7c3e1e8ecae8492a1b728b482 (patch) | |
| tree | b218e550b2b09e4920af6e12db531bfd65f65929 /docs | |
| parent | e03b7c75be589d12ddc97d074abd2e3a5c6b7cdf (diff) | |
| download | Sakura-8c8b32d59acc78c7c3e1e8ecae8492a1b728b482.tar.gz Sakura-8c8b32d59acc78c7c3e1e8ecae8492a1b728b482.zip | |
Diagrams (#18)
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/command-interface.puml | 58 | ||||
| -rw-r--r-- | docs/constraint-classification.puml | 82 | ||||
| -rw-r--r-- | docs/constraint-enforcement-strategies.puml | 42 | ||||
| -rw-r--r-- | docs/data-model.puml | 101 | ||||
| -rw-r--r-- | docs/distribution-architecture.puml | 63 | ||||
| -rw-r--r-- | docs/infinite-relations.puml | 177 | ||||
| -rw-r--r-- | docs/iterator-pipeline.puml | 45 | ||||
| -rw-r--r-- | docs/karuta-interface-layers.puml | 65 | ||||
| -rw-r--r-- | docs/merkle-tree-hierarchy.puml | 50 | ||||
| -rw-r--r-- | docs/module-dependencies.puml | 39 | ||||
| -rw-r--r-- | docs/provenance-lineage.puml | 69 | ||||
| -rw-r--r-- | docs/query-execution-flow.puml | 54 | ||||
| -rw-r--r-- | docs/reactive-queries.puml | 51 | ||||
| -rw-r--r-- | docs/roadmap.puml | 72 | ||||
| -rw-r--r-- | docs/system-overview.puml | 81 | ||||
| -rw-r--r-- | docs/temporal-queries.puml | 61 | ||||
| -rw-r--r-- | docs/type-checking-flow.puml | 108 | ||||
| -rw-r--r-- | docs/type-hierarchy.puml | 289 |
18 files changed, 1507 insertions, 0 deletions
diff --git a/docs/command-interface.puml b/docs/command-interface.puml new file mode 100644 index 0000000..4c0319a --- /dev/null +++ b/docs/command-interface.puml @@ -0,0 +1,58 @@ +@startuml command-interface +!theme plain +title Command-Based Interface Flow + +participant "Karuta" as K +participant "domino:execute/2" as API +participant "Command Validator" as V +participant "operations.erl" as Ops +database "Mnesia" as DB + +K -> API: execute(DB0, {create, relation, employee, Schema}) +activate API +API -> V: validate({create, relation, ...}) +activate V +V -> V: check schema format +V -> V: verify types +V --> API: ok +deactivate V + +API -> Ops: create_relation(DB0, employee, Schema) +activate Ops +Ops -> DB: transaction(fn -> ... end) +activate DB +DB -> DB: insert relation record +DB -> DB: update database tree +DB --> Ops: {atomic, {NewDB, Hash}} +deactivate DB +Ops --> API: {NewDB, Hash} +deactivate Ops + +API --> K: {ok, DB1, {relation_created, employee, Hash}} +deactivate API + +K -> API: execute(DB1, {insert, tuple, employee, Data}) +activate API +API -> V: validate({insert, tuple, ...}) +activate V +V -> V: check schema compliance +V -> V: verify constraints +V --> API: ok +deactivate V + +API -> Ops: create_tuple(DB1, employee, Data) +activate Ops +Ops -> DB: transaction(fn -> ... end) +activate DB +DB -> DB: store attribute values +DB -> DB: create tuple record +DB -> DB: update merkle tree +DB --> Ops: {atomic, {NewDB2, TupleHash}} +deactivate DB +Ops --> API: {NewDB2, TupleHash} +deactivate Ops + +API --> K: {ok, DB2, {tuple_inserted, TupleHash}} +deactivate API + +@enduml diff --git a/docs/constraint-classification.puml b/docs/constraint-classification.puml new file mode 100644 index 0000000..09094f1 --- /dev/null +++ b/docs/constraint-classification.puml @@ -0,0 +1,82 @@ +@startuml constraint-classification +!theme plain +title Constraint Classification (McGoveran Framework) + +package "Database Constraints" { + class RelationConstraints { + Which relations must/can exist + Example: referential integrity + } + + class CardinalityConstraints { + Relation size limits + Examples: + - exactly N tuples + - at most M tuples + } +} + +package "Relation Constraints" { + package "Tuple Constraints" { + class AttributeConstraints { + Domain constraints per attribute + Examples: + - age >= 18 + - salary > 0 + - name ≠ "" + } + + class TupleLevelConstraints { + Cross-attribute rules + Example: + if salary > 200k then age >= 30 + } + } + + package "Relation-Level Constraints" { + class KeyConstraints { + Uniqueness + not null + - Primary keys + - Candidate keys + - Composite keys + } + + class FunctionalDependencies { + A → B + Example: ZIP → {city, state} + } + + class ForeignKeys { + Inclusion dependencies + Example: employee.dept_id ⊆ department.id + } + } +} + +package "Transition Constraints" { + class StateTransitionRules { + Before → After constraints + Examples: + - salary (monotonic increasing) + - created_at (immutable) + } + + class TemporalConstraints { + Time-based rules + Example: end_date >= start_date + } +} + +package "Multi-Relation Constraints" { + class AggregateConstraints { + Cross-relation aggregates + Example: sum(dept_salaries) <= dept_budget + } + + class MutualExclusion { + Disjoint sets + Example: managers ∩ ICs = ∅ + } +} + +@enduml diff --git a/docs/constraint-enforcement-strategies.puml b/docs/constraint-enforcement-strategies.puml new file mode 100644 index 0000000..6e0305d --- /dev/null +++ b/docs/constraint-enforcement-strategies.puml @@ -0,0 +1,42 @@ +@startuml constraint-enforcement-strategies +!theme plain +title Constraint Enforcement Strategies + +state "Operation Request" as Request +state "Immediate Validation" as Immediate +state "Deferred Validation" as Deferred +state "Execute Operation" as Execute +state "Transaction Commit" as Commit +state "Rollback" as Rollback +state "Success" as Success + +Request --> Immediate: Strategy 1:\nEager +Request --> Execute: Strategy 2:\nDeferred + +Immediate --> Execute: Valid +Immediate --> Rollback: Invalid + +Execute --> Deferred: At commit +Deferred --> Commit: Valid +Deferred --> Rollback: Invalid + +Commit --> Success +Rollback --> Request: Retry + +note right of Immediate + Immediate Checking: + - Validate before execute + - Simple reasoning + - May reject valid intermediate states + - Lower performance +end note + +note right of Deferred + Deferred Checking: + - Validate at transaction end + - Allows intermediate invalid states + - Better performance + - Complex error handling +end note + +@enduml diff --git a/docs/data-model.puml b/docs/data-model.puml new file mode 100644 index 0000000..59e2cff --- /dev/null +++ b/docs/data-model.puml @@ -0,0 +1,101 @@ +@startuml data-model +!theme plain +title Data Model Core Abstractions + +class attribute { + + hash: SHA256 + + value: term() +} + +class tuple { + + hash: SHA256 + + relation: atom() + + attribute_map: #{name => hash} +} + +class relation { + + hash: SHA256 + + name: atom() + + tree: merkle_tree() + + schema: #{attr => type_relation} + + constraints: constraints() + + cardinality: {finite, N} | aleph_zero | continuum + + generator: function() | undefined + + provenance: provenance() +} + +class type_relation { + + name: atom() + + erlang_type: type() + + membership_predicate: function() + + unfold_generator: function() + + cardinality: aleph_zero | continuum +} + +class database_state { + + hash: SHA256 + + name: atom() + + tree: merkle_tree() + + relations: #{name => hash} + + type_relations: #{name => type_relation} + + timestamp: integer() +} + +database_state "1" *-- "many" relation : contains +database_state "1" *-- "many" type_relation : defines types +relation "1" *-- "many" tuple : contains +tuple "1" *-- "many" attribute : references +relation --> type_relation : schema references + +note right of attribute + Content-Addressed Storage: + - SHA-256 hash of value + - Automatic deduplication + - Immutable once stored + + Value Validation: + Value must be member of + type relation specified in schema +end note + +note right of relation + Storage Strategy: + - Finite: Merkle tree (materialized) + - Infinite: Generator (lazy) + + Type Relations: + - Primitives: natural, integer, real, string + - Composite: views over other relations +end note + +note left of type_relation + **Schema Philosophy:** + Attributes are typed by type relations (not primitives). + Types are relations (stored as infinite relations). + Schema validation = membership checking. + + **Type Relations are Relations:** + They define domains via: + 1. Erlang type constraint + 2. Additional predicates + 3. Unfold generator for enumeration + + Examples: + - natural[X] :- integer[X], X >= 0 + - complex[X] :- X is (A,B), real[A], real[B] +end note + +note bottom of database_state + **Schema Example:** + employee relation schema: + #{ + name => non_empty_string, % type relation + age => natural, % type relation + salary => positive_integer % type relation + } + + Each schema value is a reference to a type relation, + NOT a primitive type string like "integer" +end note + +@enduml diff --git a/docs/distribution-architecture.puml b/docs/distribution-architecture.puml new file mode 100644 index 0000000..fd2fd8c --- /dev/null +++ b/docs/distribution-architecture.puml @@ -0,0 +1,63 @@ +@startuml distribution-architecture +!theme plain +title Future Distribution Architecture (Proposed) + +node "Node 1" { + component "Domino Instance 1" as D1 + database "Mnesia Replica 1" as M1 + component "Merkle Tree 1" as MT1 +} + +node "Node 2" { + component "Domino Instance 2" as D2 + database "Mnesia Replica 2" as M2 + component "Merkle Tree 2" as MT2 +} + +node "Node 3" { + component "Domino Instance 3" as D3 + database "Mnesia Replica 3" as M3 + component "Merkle Tree 3" as MT3 +} + +cloud "Sync Protocol" { + [Hash Comparison] as HC + [Delta Transfer] as DT + [Conflict Resolution] as CR +} + +D1 --> MT1 +D2 --> MT2 +D3 --> MT3 + +MT1 --> M1 +MT2 --> M2 +MT3 --> M3 + +MT1 <--> HC: compare hashes +MT2 <--> HC +MT3 <--> HC + +HC --> DT: if different +DT --> CR: if conflict +CR --> M1: apply changes +CR --> M2 +CR --> M3 + +note right of HC + Merkle tree enables efficient sync: + 1. Compare root hashes + 2. If different, compare subtrees + 3. Transfer only changed branches + 4. O(log n) comparison complexity +end note + +note bottom of CR + Conflict Resolution Strategies: + - Last-write-wins (timestamp) + - CRDTs (commutative operations) + - Consensus (Raft/Paxos) + - Application-defined merge +end note + +@enduml diff --git a/docs/infinite-relations.puml b/docs/infinite-relations.puml new file mode 100644 index 0000000..cd6aa0f --- /dev/null +++ b/docs/infinite-relations.puml @@ -0,0 +1,177 @@ +@startuml infinite-relations +!theme plain +title Infinite Type Relations: Unfold Pattern & Membership + +abstract class InfiniteTypeRelation { + + name: atom() + + cardinality: aleph_zero | continuum + + erlang_type: type() + + membership_predicate: function() + + unfold_generator: function() + + constraints: constraints() +} + +class Naturals { + Erlang Type: integer() + Membership: natural[X] :- + erlang:is_integer(X), + X >= 0. + + Unfold Generator: + unfold(0, fun(N) -> N + 1 end) + → 0, 1, 2, 3, ... + + Cardinality: aleph_zero +} + +class Integers { + Erlang Type: integer() + Membership: integer[X] :- + erlang:is_integer(X). + + Unfold Generator: + unfold({0, 1}, fun({N, S}) -> + case S of + 1 -> {N, -1}; + -1 -> {N+1, 1} + end + end) + → 0, 1, -1, 2, -2, ... + + Cardinality: aleph_zero +} + +class Rationals { + Erlang Type: {integer(), integer()} + Membership: rational[X] :- + X is (P, Q), + integer[P], integer[Q], + Q ≠ 0. + + Unfold Generator: + Stern-Brocot tree unfold + → (0,1), (1,1), (1,2), ... + + Cardinality: aleph_zero +} + +class Reals { + Erlang Type: float() + Membership: real[X] :- + erlang:is_float(X). + + Unfold Generator: + IEEE 754 float enumeration + (impractical, continuum) + + Cardinality: continuum +} + +class Strings { + Erlang Type: string() + Membership: string[X] :- + erlang:is_list(X), + all_chars(X). + + Unfold Generator: + Length-ordered, lexicographic + → "", "a", "b", ..., "aa", ... + + Cardinality: aleph_zero +} + +class Plus { + Erlang Type: {integer(), integer(), integer()} + Membership: plus[A, B, Sum] :- + integer[A], integer[B], + Sum is A + B. + + Unfold Generator: + Diagonalization of ℤ × ℤ + → (0,0,0), (0,1,1), (1,0,1), ... + + Cardinality: continuum (ℤ × ℤ) +} + +package "Constraint Application" { + class ConstrainedGenerator { + Pattern: Apply constraints during unfold + base_generator: unfold() + constraints: [constraint()] + .. + filter_unfold(Gen, Constraints) -> + filter(Gen, satisfies_all(Constraints)) + } + + note bottom of ConstrainedGenerator + **Example 1: Bounded Naturals** + natural[X], X >= 0, X =< 100 + → Generates: 0, 1, 2, ..., 100 (finite!) + + **Example 2: Constrained Plus** + plus[5, B, 12] + → Solves: B = 7 + → Generates: single tuple (5, 7, 12) + + **Example 3: Range Query** + integer[X], X >= -10, X =< 10 + → Generates: 0, 1, -1, 2, -2, ..., 10, -10 + end note +} + +package "Composite Type Relations (Views)" { + class Complex { + Type Definition (Karuta): + complex[X] :- + X is (A, B), + real[A], real[B]. + + Implementation: + Unfold real × real with + product enumeration + + Not primitive: Defined as view + over primitive real relation + } +} + +InfiniteTypeRelation <|-- Naturals +InfiniteTypeRelation <|-- Integers +InfiniteTypeRelation <|-- Rationals +InfiniteTypeRelation <|-- Reals +InfiniteTypeRelation <|-- Strings +InfiniteTypeRelation <|-- Plus + +Naturals --> ConstrainedGenerator: apply\nconstraints +Integers --> ConstrainedGenerator +Rationals --> ConstrainedGenerator +Plus --> ConstrainedGenerator + +Reals --> Complex: used in\nproduct +Complex : (view relation) + +note right of Naturals + **Core Pattern:** Infinite relations use unfold + to generate members. Primitive types are + infinite relations. + + **Membership:** Erlang type + constraints + + **Unfold Pattern:** + unfold(Seed, Step) generates infinite sequence: + Seed, Step(Seed), Step(Step(Seed)), ... + + This enables lazy evaluation and + constraint-based pruning. +end note + +note left of Plus + **Function Relations:** + Mathematical functions like plus, multiply, etc. + are relations with continuum cardinality. + + Membership = evaluation + Generation = enumeration +end note + +@enduml diff --git a/docs/iterator-pipeline.puml b/docs/iterator-pipeline.puml new file mode 100644 index 0000000..810ef63 --- /dev/null +++ b/docs/iterator-pipeline.puml @@ -0,0 +1,45 @@ +@startuml iterator-pipeline +!theme plain +title Volcano Iterator Model - Process Pipeline + +component "Scan Iterator\n(Process)" as P1 { + [Read from Relation] as S1 +} + +component "Select Iterator\n(Process)" as P2 { + [Apply Predicate] as S2 +} + +component "Project Iterator\n(Process)" as P3 { + [Filter Attributes] as S3 +} + +component "Sort Iterator\n(Process)" as P4 { + [Sort All Tuples] as S4 +} + +component "Take Iterator\n(Process)" as P5 { + [Limit N Tuples] as S5 +} + +P1 -right-> P2: {next, Pid}\n{tuple, T} | done +P2 -right-> P3: {next, Pid}\n{tuple, T} | done +P3 -right-> P4: {next, Pid}\n{tuple, T} | done +P4 -right-> P5: {next, Pid}\n{tuple, T} | done + +note bottom of P1 + Each iterator is an + independent Erlang process + + Message passing protocol: + - Request: {next, CallerPid} + - Response: {tuple, Data} | done + + Benefits: + - Lazy evaluation + - Memory-bounded + - Composable + - Concurrent +end note + +@enduml diff --git a/docs/karuta-interface-layers.puml b/docs/karuta-interface-layers.puml new file mode 100644 index 0000000..cd5443e --- /dev/null +++ b/docs/karuta-interface-layers.puml @@ -0,0 +1,65 @@ +@startuml karuta-interface-layers +!theme plain +title Karuta Interface Architecture Layers + +actor "Karuta Program" as Karuta + +package "Language Bindings" { + [Karuta FFI] as FFI + [Erlang Ports] as Ports + [NIF (Native)] as NIF +} + +package "Stable Contract Layer" { + component "domino.erl" as DominoAPI { + [create_database/1] + [execute/2] + [query/2] + [transaction/2] + } +} + +package "Command Processor" { + [Command Parser] as CmdParser + [Validator] as Validator + [Executor] as Executor +} + +package "Implementation Layer" { + component "operations.erl" as Ops { + [create_relation/3] + [create_tuple/3] + [get_tuples_iterator/2] + [etc...] + } +} + +database "Mnesia Storage" as Storage + +Karuta --> FFI +Karuta --> Ports +Karuta --> NIF + +FFI --> DominoAPI +Ports --> DominoAPI +NIF --> DominoAPI + +DominoAPI --> CmdParser +CmdParser --> Validator +Validator --> Executor + +Executor --> Ops +Ops --> Storage + +note right of DominoAPI + Stable, versioned interface + Command format: + {Verb, Entity, Name, Parameters} + + Examples: + {create, relation, employee, Schema} + {insert, tuple, employee, Data} + {query, relation, employee, Constraints} +end note + +@enduml diff --git a/docs/merkle-tree-hierarchy.puml b/docs/merkle-tree-hierarchy.puml new file mode 100644 index 0000000..4e86e26 --- /dev/null +++ b/docs/merkle-tree-hierarchy.puml @@ -0,0 +1,50 @@ +@startuml merkle-tree-hierarchy +!theme plain +title Merkle Tree Hierarchy + +package "Database Level" { + [Database Hash] as DBHash + database "Merkle Tree of Relations" as DBTree +} + +package "Relation Level" { + [Relation Hash 1] as R1Hash + [Relation Hash 2] as R2Hash + [Relation Hash N] as RNHash + + database "Merkle Tree of Tuples (R1)" as R1Tree + database "Merkle Tree of Tuples (R2)" as R2Tree +} + +package "Tuple Level" { + [Tuple Hash 1.1] as T11 + [Tuple Hash 1.2] as T12 + [Tuple Hash 2.1] as T21 + [Tuple Hash 2.2] as T22 +} + +DBHash --> DBTree +DBTree --> R1Hash +DBTree --> R2Hash +DBTree --> RNHash + +R1Hash --> R1Tree +R2Hash --> R2Tree + +R1Tree --> T11 +R1Tree --> T12 +R2Tree --> T21 +R2Tree --> T22 + +note bottom of DBHash + Single hash represents + entire database state + + Benefits: + - Version control + - Efficient diffing + - Distributed sync + - Integrity verification +end note + +@enduml diff --git a/docs/module-dependencies.puml b/docs/module-dependencies.puml new file mode 100644 index 0000000..dcc955b --- /dev/null +++ b/docs/module-dependencies.puml @@ -0,0 +1,39 @@ +@startuml module-dependencies +!theme plain +title Module Dependencies + +package "Entry Points" { + [main.erl] as Main + [repl.erl] as REPL +} + +package "Server Layer" { + [xml_server_app.erl] as XMLApp + [xml_server.erl] as XMLServer +} + +package "Query Layer" { + [query_planner.erl] as Planner +} + +package "Core Layer" { + [operations.erl] as Ops +} + +package "Support Modules" { + [relation.erl] as Relation + [generators.erl] as Generators + [visualizer.erl] as Visualizer +} + +Main --> XMLApp +XMLApp --> XMLServer +XMLServer --> Planner +REPL --> Ops + +Planner --> Ops +Ops --> Relation +Ops --> Generators +Ops --> Visualizer + +@enduml diff --git a/docs/provenance-lineage.puml b/docs/provenance-lineage.puml new file mode 100644 index 0000000..4e8f68a --- /dev/null +++ b/docs/provenance-lineage.puml @@ -0,0 +1,69 @@ +@startuml provenance-lineage +!theme plain +title Provenance and Lineage Tracking + +component "Base Tuple\n(employee)" as T1 + +note right of T1 + **Data:** + id = 1 + name = "Alice" + age = 30 + salary = 100000 + + **Meta:** + provenance: + id: (employee, id) + name: (employee, name) + age: (employee, age) + salary: (employee, salary) + lineage: (base, employee) +end note + +component "After Select\n(age > 25)" as T2 + +note right of T2 + **Data:** + id = 1 + name = "Alice" + age = 30 + salary = 100000 + + **Meta:** + provenance: (same as above) + lineage: + select + fun(T) -> age > 25 end + (base, employee) +end note + +component "After Project\n[name, age]" as T3 + +note right of T3 + **Data:** + name = "Alice" + age = 30 + + **Meta:** + provenance: + name: (employee, name) + age: (employee, age) + lineage: + project + [name, age] + (select, _, (base, employee)) +end note + +T1 -down-> T2: select operation\nadds to lineage +T2 -down-> T3: project operation\nfilters provenance + +note bottom of T3 + **Benefits:** + - Data source tracking + - Query result explanation + - Reproducibility + - Debugging support + - Foundation for updatable views +end note + +@enduml diff --git a/docs/query-execution-flow.puml b/docs/query-execution-flow.puml new file mode 100644 index 0000000..998b0e2 --- /dev/null +++ b/docs/query-execution-flow.puml @@ -0,0 +1,54 @@ +@startuml query-execution-flow +!theme plain +title Query Execution Flow + +actor Client +participant "Query Planner" as Planner +participant "Scan Iterator" as Scan +participant "Select Iterator" as Select +participant "Project Iterator" as Project +participant "Operations API" as Ops +database "Mnesia" as DB + +Client -> Planner: query({project,\n {select, {scan, employee}, Pred},\n [name, age]}) +activate Planner +Planner -> Planner: parse & validate +Planner -> Scan: spawn_iterator(employee) +activate Scan +Planner -> Select: spawn_iterator(Scan, Pred) +activate Select +Planner -> Project: spawn_iterator(Select, [name, age]) +activate Project +Planner --> Client: {ok, Iterator} +deactivate Planner + +Client -> Project: next_tuple() +Project -> Select: next_tuple() +Select -> Scan: next_tuple() +Scan -> Ops: get_tuples_iterator(employee) +Ops -> DB: transaction(read tuple) +DB --> Ops: {ok, Tuple} +Ops --> Scan: {ok, Tuple} +Scan --> Select: {ok, Tuple} +Select -> Select: apply Predicate +Select --> Project: {ok, Tuple} +Project -> Project: filter attributes +Project --> Client: {ok, #{name => "Alice", age => 30}} + +Client -> Project: next_tuple() +Project -> Select: next_tuple() +Select -> Scan: next_tuple() +Scan -> Ops: get_tuples_iterator(employee) +Ops -> DB: transaction(read tuple) +DB --> Ops: done +Ops --> Scan: done +Scan --> Select: done +Select --> Project: done +Project --> Client: done + +Client -> Project: close_iterator() +deactivate Project +deactivate Select +deactivate Scan + +@enduml diff --git a/docs/reactive-queries.puml b/docs/reactive-queries.puml new file mode 100644 index 0000000..bcba5d5 --- /dev/null +++ b/docs/reactive-queries.puml @@ -0,0 +1,51 @@ +@startuml reactive-queries +!theme plain +title Reactive Queries (Live Subscriptions) + +participant "Client" as C +participant "Subscription Manager" as SM +participant "Domino" as D +database "employee relation" as E + +C -> SM: subscribe(query: "age > 30") +activate SM +SM -> D: register_subscription(employee, predicate) +activate D +D -> E: initial query +E --> D: [{name: "Alice", age: 35}] +D --> SM: initial results +SM --> C: [{name: "Alice", age: 35}] +deactivate D +deactivate SM + +... time passes ... + +C -> D: insert(employee, {name: "Bob", age: 32}) +activate D +D -> D: check affected subscriptions +D -> D: evaluate predicate on new tuple\n(32 > 30? yes) +D -> SM: notify(subscription_id, {inserted: "Bob"}) +activate SM +SM -> C: delta: {inserted: {name: "Bob", age: 32}} +deactivate SM +deactivate D + +C -> D: insert(employee, {name: "Charlie", age: 25}) +activate D +D -> D: evaluate predicate\n(25 > 30? no) +D -> D: no notification needed +deactivate D + +note right of SM + Subscription tracks: + - Relation(s) to watch + - Filter predicate + - Client callback + + On mutation: + 1. Check which subscriptions affected + 2. Evaluate predicate on changed tuples + 3. Send delta (not full re-query) +end note + +@enduml diff --git a/docs/roadmap.puml b/docs/roadmap.puml new file mode 100644 index 0000000..42ad8c2 --- /dev/null +++ b/docs/roadmap.puml @@ -0,0 +1,72 @@ +@startuml roadmap +!theme plain +title Suggested Implementation Roadmap + +package "Phase 1: Stable Interface (MVP)" { + [domino.erl wrapper] as P1_1 + [Command interface] as P1_2 + [Basic constraint validation] as P1_3 + [Karuta FFI bindings] as P1_4 +} + +package "Phase 2: Type System" { + [Fake-relations primitives] as P2_1 + [Constraint-based refinement] as P2_2 + [Subtype checking] as P2_3 + [Type inference] as P2_4 +} + +package "Phase 3: Advanced Constraints" { + [Foreign keys] as P3_1 + [Functional dependencies] as P3_2 + [Tuple/relation-level constraints] as P3_3 + [Transition constraints] as P3_4 +} + +package "Phase 4: Query Features" { + [Updatable views] as P4_1 + [Materialized views] as P4_2 + [Query optimization] as P4_3 + [Explain plans] as P4_4 +} + +package "Phase 5: Distribution" { + [Merkle sync] as P5_1 + [Multi-node replication] as P5_2 + [Partition strategies] as P5_3 + [Consistency protocols] as P5_4 +} + +package "Phase 6: Advanced Features" { + [Temporal queries] as P6_1 + [Reactive queries] as P6_2 + [Constraint solving] as P6_3 + [Datalog engine] as P6_4 +} + +P1_1 -down-> P2_1 +P1_2 -down-> P2_2 +P1_3 -down-> P3_1 +P1_4 -down-> P2_1 + +P2_1 -down-> P3_1 +P2_2 -down-> P3_2 +P2_3 -down-> P3_3 +P2_4 -down-> P4_1 + +P3_1 -down-> P4_1 +P3_2 -down-> P4_2 +P3_3 -down-> P4_3 +P3_4 -down-> P4_4 + +P4_1 -down-> P5_1 +P4_2 -down-> P5_2 +P4_3 -down-> P5_3 +P4_4 -down-> P6_1 + +P5_1 -down-> P6_1 +P5_2 -down-> P6_2 +P5_3 -down-> P6_3 +P5_4 -down-> P6_4 + +@enduml diff --git a/docs/system-overview.puml b/docs/system-overview.puml new file mode 100644 index 0000000..8d76fc5 --- /dev/null +++ b/docs/system-overview.puml @@ -0,0 +1,81 @@ +@startuml system-overview +!theme plain +title Domino System Overview + +package "Client Interfaces" { + [XML Server\n(TCP/IP Port 8080)] as XML + [REPL\n(Interactive Shell)] as REPL + [Direct API\n(Erlang Apps)] as API +} + +package "Query Processing Layer" { + package "Query Planner" { + [DSL Parser] as Parser + [Plan Validation\n& Compilation] as Validator + } + + package "Volcano Iterator Model" { + [Scan Iterator] as Scan + [Select Iterator] as Select + [Project Iterator] as Project + [Sort Iterator] as Sort + [Take Iterator] as Take + [Join Iterators] as Join + } +} + +package "Operations Layer (API)" { + [Database Management] as DBMgmt + [Relation Operations] as RelOps + [Tuple Operations] as TupleOps + [Iterator Management] as IterMgmt +} + +package "Data Model Layer" { + [Core Abstractions\nattribute, tuple,\nrelation, database_state] as CoreAbs + [Finite Relations\n(Merkle Trees)] as Finite + [Infinite Relations\n(Generators)] as Infinite +} + +package "Content-Addressed Storage" { + database "Mnesia" { + [attribute table] as AttrTable + [tuple table] as TupleTable + [relation table] as RelTable + [database_state table] as DBTable + } +} + +XML --> Parser +REPL --> Parser +API --> Parser + +Parser --> Validator +Validator --> Scan + +Scan --> Select +Select --> Project +Project --> Sort +Sort --> Take +Join --> Take + +Scan --> TupleOps +Select --> IterMgmt +Project --> IterMgmt + +DBMgmt --> CoreAbs +RelOps --> CoreAbs +TupleOps --> CoreAbs +IterMgmt --> CoreAbs + +CoreAbs --> Finite +CoreAbs --> Infinite + +Finite --> AttrTable +Finite --> TupleTable +Finite --> RelTable +Finite --> DBTable + +Infinite --> AttrTable + +@enduml diff --git a/docs/temporal-queries.puml b/docs/temporal-queries.puml new file mode 100644 index 0000000..7d72ed5 --- /dev/null +++ b/docs/temporal-queries.puml @@ -0,0 +1,61 @@ +@startuml temporal-queries +!theme plain +title Temporal Queries with Immutable Database States + +database "DB @ t0" as DB0 +note bottom of DB0 + hash = abc123... + timestamp = 2024-01-01 10:00 + + relations: + employee => hash_e0 +end note + +database "DB @ t1" as DB1 +note bottom of DB1 + hash = def456... + timestamp = 2024-01-01 11:00 + + relations: + employee => hash_e1 +end note + +database "DB @ t2" as DB2 +note bottom of DB2 + hash = ghi789... + timestamp = 2024-01-01 12:00 + + relations: + employee => hash_e2 +end note + +database "Current DB" as DB3 +note bottom of DB3 + hash = jkl012... + timestamp = 2024-01-01 13:00 + + relations: + employee => hash_e3 +end note + +DB0 -right-> DB1: insert tuple +DB1 -right-> DB2: update salary +DB2 -right-> DB3: delete tuple + +note top of DB0 + **Time Travel Queries:** + + query_at_time(2024-01-01 10:00) + → returns DB0 + + query_at_time(2024-01-01 12:00) + → returns DB2 + + diff(DB0, DB3) + → (inserted: [...], deleted: [...], modified: [...]) + + history(employee, id: 1) + → [(t0, state0), (t1, state1), (t2, state2)] +end note + +@enduml diff --git a/docs/type-checking-flow.puml b/docs/type-checking-flow.puml new file mode 100644 index 0000000..d1e6654 --- /dev/null +++ b/docs/type-checking-flow.puml @@ -0,0 +1,108 @@ +@startuml type-checking-flow +!theme plain +title Type Checking as Relation Membership Checking + +participant "Karuta Program" as K +participant "Type Checker" as TC +participant "Domino" as D +database "Type Relations\n(Infinite Relations)" as TR + +note over K,TR + **Type Checking:** Check if value is member of type relation + **Type Relations:** Primitives stored as infinite relations + **Membership:** Erlang type check + constraint satisfaction +end note + +K -> TC: insert(employee, {age: 25, name: "Alice"}) +activate TC + +TC -> D: check: natural[25]? +activate D +D -> TR: membership query: natural[25] +activate TR +TR -> TR: 1. Erlang type check:\n is_integer(25) → true +TR -> TR: 2. Constraint check:\n 25 >= 0 → true +TR --> D: true (25 ∈ natural) +deactivate TR +D --> TC: member ✓ +deactivate D + +TC -> D: check: non_empty_string["Alice"]? +activate D +D -> TR: membership query: non_empty_string["Alice"] +activate TR +TR -> TR: 1. Check string["Alice"]:\n is_list("Alice") ∧ all_chars → true +TR -> TR: 2. Constraint check:\n length("Alice") > 0 → true +TR --> D: true ("Alice" ∈ non_empty_string) +deactivate TR +D --> TC: member ✓ +deactivate D + +TC --> K: type_check passed ✓\n{age: 25, name: "Alice"} ∈ employee +deactivate TC + +== Type Check Failure Example == + +K -> TC: insert(employee, {age: -5, name: ""}) +activate TC + +TC -> D: check: natural[-5]? +activate D +D -> TR: membership query: natural[-5] +activate TR +TR -> TR: 1. Erlang type check:\n is_integer(-5) → true +TR -> TR: 2. Constraint check:\n -5 >= 0 → false ✗ +TR --> D: false (-5 ∉ natural) +deactivate TR +D --> TC: not_member ✗ +deactivate D + +TC --> K: type_error: -5 ∉ natural\nExpected: natural[Age]\nGot: Age = -5 +deactivate TC + +== Composite Type Example == + +K -> TC: check: complex[(3.14, 2.71)]? +activate TC + +TC -> D: check: complex[(3.14, 2.71)]? +activate D +note over D + complex[X] :- + X is (A, B), + real[A], real[B]. +end note + +D -> TR: membership query: real[3.14] +activate TR +TR -> TR: is_float(3.14) → true +TR --> D: true (3.14 ∈ real) +deactivate TR + +D -> TR: membership query: real[2.71] +activate TR +TR -> TR: is_float(2.71) → true +TR --> D: true (2.71 ∈ real) +deactivate TR + +D --> TC: member ✓\n(3.14, 2.71) ∈ complex +deactivate D + +TC --> K: type_check passed ✓ +deactivate TC + +note right of TR + **Type Relation Storage:** + - Primitives: infinite relations + - Membership: predicate evaluation + - No materialization needed + - Lazy constraint checking + + **Example:** + natural[X] is stored as: + - erlang_type: integer() + - constraint: X >= 0 + - generator: unfold(0, +1) +end note + +@enduml diff --git a/docs/type-hierarchy.puml b/docs/type-hierarchy.puml new file mode 100644 index 0000000..c53a965 --- /dev/null +++ b/docs/type-hierarchy.puml @@ -0,0 +1,289 @@ +@startuml type-hierarchy +!theme plain +title Type System: Stratified Universes & Types as Relations + +package "Universe Stratification" { + class "Universe₀" as U0 { + Base values + Examples: 3, -5, 3.14, true, "hello" + The set of all runtime values + } + + class "Universe₁" as U1 { + Type relations (classify values) + Examples: natural, integer, real, boolean + Each type is a relation over Universe₀ + Type relations are infinite relations + } + + class "Universe₂" as U2 { + Type of type relations + The classifier of type relations + Prevents self-reference paradoxes + } + + class "Universe₃" as U3 { + Meta-type level + Type : Universe₂ : Universe₃ + } + + U0 : Universe₁ + U1 : Universe₂ + U2 : Universe₃ + U3 : Universe₄ + + note right of U1 + **Stratification prevents Russell's Paradox** + Type relations live in Universe₁ + and classify values in Universe₀. + A type cannot contain itself. + + natural : Universe₁ + 3 ∈ natural (3 ∈ Universe₀) + But: natural ∉ natural ✗ (universe mismatch) + end note +} + +package "Supertypes (Universe₁)" { + class Number { + Membership: number[X] where X : Universe₀ + Definition: Union of all numeric types + number[X] :- natural[X]; integer[X]; + rational[X]; real[X]. + Allows polymorphism over numeric types + Universe level: Universe₁ + } + + class Scalar { + Membership: scalar[X] where X : Universe₀ + Definition: Atomic (non-composite) values + scalar[X] :- number[X]; boolean[X]; string[X]. + Universe level: Universe₁ + } +} + +package "Numeric Type Relations (Universe₁)" { + class Naturals { + Membership: natural[X] where X : Universe₀ + Criteria: + - X is erlang:integer() + - X >= 0 + Cardinality: aleph_zero + Generator: 0, 1, 2, 3, ... + Universe level: Universe₁ + } + + class Integers { + Membership: integer[X] where X : Universe₀ + Criteria: + - X is erlang:integer() + Cardinality: aleph_zero + Generator: 0, 1, -1, 2, -2, ... + Universe level: Universe₁ + } + + class Rationals { + Membership: rational[X] where X : Universe₀ + Criteria: + - X is (P, Q) + - integer[P], integer[Q] + - Q ≠ 0 + Cardinality: aleph_zero + Generator: Stern-Brocot tree + Universe level: Universe₁ + } + + class Reals { + Membership: real[X] where X : Universe₀ + Criteria: + - X is erlang:float() + Cardinality: continuum + Generator: IEEE 754 floats + Universe level: Universe₁ + } +} + +package "Other Primitive Types (Universe₁)" { + class Strings { + Membership: string[X] where X : Universe₀ + Criteria: + - X is erlang:string() + Cardinality: aleph_zero + Ordering: by length, then lexicographic + Universe level: Universe₁ + } + + class Booleans { + Membership: boolean[X] where X : Universe₀ + Criteria: + - X is erlang:boolean() + - X ∈ {true, false} + Cardinality: 2 + Universe level: Universe₁ + } +} + +package "Constrained Type Relations (Universe₁)" { + class PositiveIntegers { + Definition: positive_int[X] where X : Universe₀ + Criteria: + - integer[X] + - X > 0 + Relation: positive_int ⊆ integer + Universe level: Universe₁ + } + + class BoundedInt { + Definition: bounded_int[X, Min, Max] + where X : Universe₀ + Criteria: + - integer[X] + - Min ≤ X ≤ Max + Relation: bounded_int ⊆ integer + Universe level: Universe₁ + } + + class NonEmptyStrings { + Definition: non_empty_string[X] + where X : Universe₀ + Criteria: + - string[X] + - length(X) > 0 + Relation: non_empty_string ⊆ string + Universe level: Universe₁ + } +} + +package "Composite Type Relations (Universe₁)" { + class Complex { + Definition (Karuta-style): + complex[X] where X : Universe₀ + complex[X] :- + X is (A, B), + real[A], real[B]. + + Interpretation: + - (A, B) where A is real part + - B is imaginary part + Relation: complex ⊆ real × real + Universe level: Universe₁ + } + + class Employee { + Definition: + employee[X] where X : Universe₀ + employee[X] :- + X is (Name, Age, Salary), + non_empty_string[Name], + positive_int[Age], + positive_int[Salary]. + + Relation: employee ⊆ string × ℕ⁺ × ℕ⁺ + Universe level: Universe₁ + } +} + +' Universe stratification relationships +U1 --> U0 : classifies values in +U2 --> U1 : types type relations +U3 --> U2 : meta-level + +' All type relations live in Universe₁ +U1 ..> Number : contains +U1 ..> Naturals : contains +U1 ..> Integers : contains +U1 ..> Rationals : contains +U1 ..> Reals : contains +U1 ..> Booleans : contains +U1 ..> Strings : contains +U1 ..> Scalar : contains + +' Type relation hierarchy (within Universe₁) +Number <|-- Naturals : ⊇ +Number <|-- Integers : ⊇ +Number <|-- Rationals : ⊇ +Number <|-- Reals : ⊇ + +Number <|-- Scalar : ⊇ +Booleans <|-- Scalar : ⊇ +Strings <|-- Scalar : ⊇ + +' Subset relations among numeric types +Naturals .up.|> Integers : ⊆ +Integers .up.|> Rationals : ⊆ +Rationals .up.|> Reals : ⊆ + +' Constrained types +Integers .down.|> PositiveIntegers : ⊇ +Integers .down.|> BoundedInt : ⊇ +Strings .down.|> NonEmptyStrings : ⊇ + +' Composite types (also in Universe₁) +Number .down.|> Complex : number × number +Complex : (view: pair of numbers) + +Scalar .down.|> Employee : scalar × scalar × scalar +Employee : (view: string × nat × nat) + +note right of Complex + **Views as Type Relations:** + Types can be defined as relational views + over other type relations. + + Example using supertype: + complex[C] :- C is (R, I), + number[R], number[I]. + + Or more specifically: + complex[C] :- C is (R, I), + real[R], real[I]. + + Views can use supertypes for flexibility! + All views live in Universe₁. +end note + +note left of Number + **Core Principle:** Every type is a relation + Type checking = membership checking in relations + T1 <: T2 iff T1 ⊆ T2 (subset relation) + + **Supertypes enable polymorphism:** + A function can accept number[X] and work + with naturals, integers, rationals, or reals. + + **Universe Levels:** + All type relations: Universe₁ + All values: Universe₀ + Type of types: Universe₂ + + **Erlang Type Mapping:** + natural → integer() + (≥ 0) + integer → integer() + rational → {integer(), integer()} + real → float() + string → string() + boolean → boolean() +end note + +note bottom of U0 + **Avoiding Russell's Paradox:** + + Like F*, Domino uses predicative universe + stratification. The key invariant: + + Type u#i : Type u#(i+1) + + In Domino: + - Values (3, "hello", true) : Universe₀ + - Type relations (natural, string) : Universe₁ + - Type : Universe₂ + + This prevents: + natural ∈ natural (universe mismatch!) + + A type relation cannot be a member of itself. + All type relations classify values in Universe₀ + but exist at Universe₁. +end note + +@enduml |
