habedi-work/useful-notes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add a glossary section the IR note file

Browse Source
This commit is contained in:
Hassan Abedi 2026-03-30 10:34:26 +02:00
parent bbe9653a78
commit 6ba970e55c
1 changed files with 25 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
hassan/011-geolog-intermediate-representation.md
View File

@ -16,9 +16,28 @@ The current pipeline is:
The lowering entry point is `geolog-lang/src/Geolog/Lower.hs`, via `lowerTop`, which calls `lower`, then `lowerEntry`, then `finishTheory`. The lowering entry point is `geolog-lang/src/Geolog/Lower.hs`, via `lowerTop`, which calls `lower`, then `lowerEntry`, then `finishTheory`.
## Glossary
- `IR`: Intermediate representation. A simpler form used between elaboration and later evaluation.
- `lowering`: The step that converts elaborated Geolog code into the IR.
- `Path`: A qualified name like `M.mul`.
- `ColType`: The type of one table column.
- `Table`: A lowered relational object with columns and maybe a primary key.
- `RelTable`: A table used for a relation or predicate.
- `FunTable`: A table used for something function-like, where input columns determine an output.
- `Term`: A small IR expression, such as a variable, literal, or projection.
- `Atom`: One table occurrence with concrete arguments.
- `Prop`: A logical formula built from atoms and connectives like equality and conjunction.
- `Law`: A quantified rule over IR propositions.
- `FlatTheory`: The final lowered result: a set of tables plus laws.
- `foreignKeys`: Generated laws saying a row depends on other rows existing.
- `total`: Generated laws saying a function row must exist when its inputs exist.
- `PiColumn`: A column introduced as part of a table's explicit shape.
- `JoinColumn`: A column introduced while following a reference or join.
## Core IR data types ## Core IR data types
The IR is intentionally relational. The IR is intentionally relational. It turns theory structure into tables and rules.
- `Path = [QName]`: a hierarchical name like `["M","mul"]`, pretty-printed as `M.mul`. - `Path = [QName]`: a hierarchical name like `["M","mul"]`, pretty-printed as `M.mul`.
- `ColType` is the type of a column. `EntityType Path` means the column refers to rows from another entity/table, `PrimType PrimInt | PrimString` covers builtin scalars, and `Tuple [(QName, ColType)]` supports structured values. - `ColType` is the type of a column. `EntityType Path` means the column refers to rows from another entity/table, `PrimType PrimInt | PrimString` covers builtin scalars, and `Tuple [(QName, ColType)]` supports structured values.
@ -32,7 +51,7 @@ See `geolog-lang/src/Geolog/IR.hs` for the concrete definitions.
## What lowering does ## What lowering does
Lowering walks an elaborated theory and converts type-theoretic structure into tables plus integrity laws. Lowering walks the elaborated theory and turns it into tables plus rules.
### 1. Records become path prefixes ### 1. Records become path prefixes
@ -54,7 +73,7 @@ See `lowerTheoryTy` in `geolog-lang/src/Geolog/Lower.hs`.
### 3. Functions/entities become `FunTable` ### 3. Functions/entities become `FunTable`
When lowering encounters an abstract decoded type that does not reduce to a more concrete theory shape, it emits a `FunTable`. When lowering finds something function-like that does not reduce to a simpler theory shape, it emits a `FunTable`.
At the end of lowering, function tables get a primary key consisting of all columns except the final result column. That matches the examples: At the end of lowering, function tables get a primary key consisting of all columns except the final result column. That matches the examples:
@ -65,7 +84,7 @@ This logic is in `finishTheory` in `geolog-lang/src/Geolog/Lower.hs`.
### 4. Dependent structure becomes extra columns ### 4. Dependent structure becomes extra columns
The interesting part is that lowering is not just flattening syntax. It also lambda-lifts shared context into explicit columns. Lowering is not just flattening syntax. It also turns shared context into explicit columns.
`liftOnShared` copies shared outer variables into the current row shape so that dependencies become relationally explicit. This is why tables like `D.mul` contain both `M.car` arguments and displayed-car columns. `liftOnShared` copies shared outer variables into the current row shape so that dependencies become relationally explicit. This is why tables like `D.mul` contain both `M.car` arguments and displayed-car columns.
@ -90,7 +109,7 @@ Each lowered table may carry generated laws.
`makeFkeys` says: if a row exists in table `p`, then the rows it depends on must also exist. `makeFkeys` says: if a row exists in table `p`, then the rows it depends on must also exist.
Operationally, this is how dependent references are reified as relational constraints. A row in `D.mul` implies the existence of corresponding rows in `D.car` and `M.mul`. This is how dependent references become relational constraints. A row in `D.mul` implies the existence of corresponding rows in `D.car` and `M.mul`.
See `makeFkeys` in `geolog-lang/src/Geolog/Lower.hs`. See `makeFkeys` in `geolog-lang/src/Geolog/Lower.hs`.
@ -139,7 +158,7 @@ The implemented IR is best understood as a relationalized, flattened theory:
- references become foreign-key-style laws - references become foreign-key-style laws
- total functions become tables plus totality laws - total functions become tables plus totality laws
So the IR is not just an AST for queries. It is the bridge from elaborated dependent syntax to a database-shaped semantics that downstream query/evaluation machinery can consume. So the IR is not just an AST for queries. It is the bridge from elaborated dependent syntax to a database-shaped form that later evaluation code can consume.
## Note ## Note