Manual updates for current Coln

flake.nix

@@ -4,12 +4,17 @@
     flake-utils.url = "github:numtide/flake-utils";
     rust-overlay.url = "github:oxalica/rust-overlay";
     ghc-wasm-meta.url = "gitlab:haskell-wasm/ghc-wasm-meta?host=gitlab.haskell.org";
+    bib2forester = {
+      url = "github:olynch/bib2forester";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
   };
   outputs =
     inputs@{
       self,
       nixpkgs,
       rust-overlay,
+      bib2forester,
       ...
     }:
     inputs.flake-utils.lib.eachSystem [ "x86_64-linux" "aarch64-darwin" ] (
@@ -214,6 +219,7 @@
         devShells.default = pkgs.mkShell {
           name = "coln";
           buildInputs = with pkgs; [
+            bib2forester.packages."${system}".default
             cabal-install
             cabal2nix
             cargo-llvm-cov

manual/templates/plain.tree

@@ -0,0 +1 @@
+\import{prelude}

manual/theme/javascript-source/forester.js

@@ -10,7 +10,7 @@ function partition(array, isValid) {
 }
 
 window.addEventListener("load", (event) => {
- autoRenderMath(document.body)
+    autoRenderMath(document.body, { fleqn: true })
 
  const openAllDetailsAbove = elt => {
   while (elt != null) {

manual/theme/style.css

@@ -85,10 +85,15 @@ h6 {
   margin-bottom: 0;
 }
 
-h5,
-h6,
 p {
   margin-top: 0;
+  margin-bottom: 0;
+}
+
+section.block > details {
+  > :not(:first-child)+* {
+    margin-top: 1rem;
+  }
 }
 
 h1,
@@ -263,6 +268,12 @@ section .block[data-taxon] details>summary>header>h1 {
   font-size: 12pt;
 }
 
+section .block[data-taxon] {
+    border-left-style: solid;
+    border-width: 2px;
+    border-radius: 0px;
+}
+
 span.taxon {
   color: #444;
   font-weight: bolder;
@@ -298,7 +309,8 @@ section.block>details {
 
 
 section.block>details[open] {
-  margin-bottom: 1em;
+    /* border-right: 1px; */
+  margin-bottom: 0;
 }
 
 
@@ -447,6 +459,15 @@ td.macro-doc {
   font-size: .9em;
 }
 
+.database-example th,
+.database-example td {
+  padding: 0.35rem 0.8rem;
+}
+
+.database-example th {
+  border-bottom: 1px solid #aaa;
+}
+
 .enclosing.macro-scope>.enclosing {
   border-radius: 2px;
 }

manual/trees/0001.tree

@@ -1,12 +1,20 @@
 \title{Coln manual}
+\import{prelude}
 
-\p{Coln is a database with an expressive language for schemas, queries, and migrations. This document forms the manual for Coln.}
+\p{\mvrnote{clean up TOC to not include examples, etc.}}
 
-\ol{
-  \li{[[002H]]}
-  \li{[[0002]]}
-  \li{[[000K]]}
-  \li{[[000L]]}
-  \li{[[000M]]}
-  \li{[[0003]]}
-}
+\transclude{002H}
+% Coln as a type theory
+\transclude{000L}
+% Coln as a database language
+\transclude{000M}
+% Coln in practice
+\transclude{0032}
+% Theoretical foundations
+\transclude{000K}
+% f-notation
+\transclude{000R}
+% Meta
+\transclude{0002}
+% Glossary
+\transclude{0003}

manual/trees/0002.tree

@@ -1,4 +1,5 @@
-\title{About the manual}
+\title{About the Manual}
+\taxon{Appendix}
 \import{prelude}
 
 \subtree[0004]{
@@ -69,7 +70,3 @@
 
   \p{More generally, the Coln manual should be thought of as more of a [[hyperbook]] than a [[zettelkasten]].}
 }
-
-\transclude{000B}
-
-\transclude{000I}

manual/trees/000B.tree

@@ -2,11 +2,14 @@
 
 \p{There are a variety of intended audiences for this manual; a given reader may fall into several of the following categories.}
 
+\scope{
+\put\transclude/toc{false}
 \transclude{000C}
 \transclude{000D}
 \transclude{000E}
 \transclude{000H}
 \transclude{000G}
+}
 
 \p{The [programmer-user](000G) who also falls into the earlier categories will benefit from a deeper understanding of Coln. However, Coln is also comprehensible in a self-contained way, just as one does not need to understand cartesian closed categories in order to use \code{lambda x: x + 1} in Python, and it is a goal of this manual to present a clear conceptual picture for the non-mathematical programmer-user.}
 

manual/trees/000G.tree

@@ -2,4 +2,4 @@
 \title{The programmer-user}
 \import{prelude}
 
-\p{The \defcase{programmer-user} is a reader who intends to incorporate Coln into a larger application. The programmer-user should be familiar with the language that they intend to use Coln from (currently, this is only TypeScript), and should be willing to learn a new language. We say “programmer-user” to distinguish this audience from the user of an application that the “programmer-user” creates; this user needs not read this manual.}
+\p{The \defcase{programmer-user} is a reader who intends to incorporate Coln into a larger application. The programmer-user should be familiar with the language that they intend to use Coln from (currently, this is only TypeScript), and should be willing to learn a new language. We say “programmer-user” to distinguish this audience from the user of an application that the “programmer-user” creates; such a user need not read this manual.}

manual/trees/000I.tree

@@ -1,3 +1,4 @@
 \title{Organization}
+\import{prelude}
 
-\p{}
+\p{\mvrnote{TODO}}

manual/trees/000K.tree

@@ -1,6 +1,6 @@
 \title{Theoretical foundations}
 
-\p{In this section, each section is a relatively self-contained introduction to some of the math or design philosophy behind Coln. The start of each section specifies which [audience](000B) the section is intended for.}
+\p{In this section, each subsection is a relatively self-contained introduction to some of the math or design philosophy behind Coln. The start of each section specifies which [audience](000B) the section is intended for.}
 
 \transclude{0028}
 

manual/trees/000L.tree

@@ -1,12 +1,17 @@
-\title{Coln as a language}
+\title{Coln as a type theory}
 \import{prelude}
 
+% Intro
 \transclude{000N}
 
-\transclude{000O}
+% Basic type constructors
+\transclude{000S}
 
-\transclude{000R}
+% Levels
+\transclude{0033}
 
-\transclude{000S}
+% Sets as views
+\transclude{0035}
 
+% Inductive types
 \transclude{001N}

manual/trees/000M.tree

@@ -1,6 +1,7 @@
-\title{Coln as a database}
+\title{Coln as a database language}
+\import{prelude}
 
-\p{Coln can work as a little proof assistant which is restricted to positive types, but the real point of this restriction is to enable a translation to the database world.}
+\p{Coln can work as a little proof assistant which is restricted to positive types, but the real point of this restriction is to enable a translation to the database world. \mvrnote{This is the first occurrence of the word "positive"}}
 
 \p{One could look at this in two ways, depending on whether you think of the language or the database as “primary.”}
 

manual/trees/000N.tree

@@ -1,25 +1,21 @@
 \title{Introduction}
+\import{prelude}
 
-\p{A traditional database language (or indeed general-purpose language) has many syntactic classes used for different purposes.}
+\p{A traditional database language (or indeed general-purpose language) has many syntactic classes used for different purposes.
+For example, a single [SQL](sql) \code{SELECT} statement has many possible clauses, each with their own syntax (see the [PostgreSQL manual](https://www.postgresql.org/docs/current/queries.html)).}
 
-\subtree{
-  \taxon{Example}
+\p{Coln has only one syntactic class: the syntactic class of an element of a type. We write \code{a : A} to express that \code{a} is an element of the type \code{A}, so, for example, it will be the case that \code{19 : Int}.}
 
-  \p{[SQL](sql) has an exceedingly large grammar. For instance, a single SELECT statement has many possible clauses, each with their own syntax (see the [postgresql manual](https://www.postgresql.org/docs/current/queries.html)).}
-}
-
-\subtree{
-  \taxon{Example}
+\p{Even types themselves are in this same syntactic class, because they are elements of [type universes](type-universe). In this case, \code{Int : Set}; the type of integers is a set. What is achieved in other languages via syntactic differentiation is achieved instead by semantic restrictions in Coln.}
 
-  \p{Many languages have a different syntax for type parameters to a function than regular parameters. For instance, in Rust one uses \code{Vec<i32>} for applying the \code{Vec : Type -> Type} function to \code{i32} while normal function application looks like \code{plus(1, 2)}, in OCaml one uses \code{int list} while normal function application looks like \code{plus 1 2}.}
-}
+\collapsedaside{\taxon{Aside} This is in contrast to typical languages with strong type systems whose syntax differs, depending on whether an operation is happening at the value or the type level. For instance, in Rust one uses \code{Vec<i32>} to apply the \code{Vec : Type -> Type} function to \code{i32}, rather than ordinary function application \code{f(1, 2)}, and in OCaml one writes the postfix \code{'t list} at the type level and \code{plus 1 2} at the value level.}
 
-\p{Coln differs from this, perhaps to an extreme degree, by only having essentially one syntactic class: the syntactic class of an element of a type. Even types themselves are in this syntactic class, because types are elements of [type universes](type-universe). What is achieved via syntactic differentiation in other languages is achieved instead by semantic restrictions in Coln.}
+\p{In Coln, a database schema is described by constructing a type. When a type is playing the role of a schema, we will call it a \defcase{theory}. An element of such a theory is called a \defcase{model}, and corresponds to a database instance that has that schema. Later, when we discuss [type levels](0033), we will be able to make precise when a type counts as a theory with an associated database schema.}
 
-\subtree{
-  \taxon{Example}
+\p{In the code examples in the upcoming sections, we will make top-level theory declarations using the following syntax:}
 
-  \p{In Coln there are set-level types, theory-level types, and top-level types. These all use the same syntax; operations which only work on set-level types will produce an error during [elaboration](000O). See [[000S]] for more information about this topic.}
+\pre{%
+\kw{theory} FavouriteNumber := Int
 }
 
-\p{One downside of this approach is that the grammar of Coln is not a very meaningful way of getting a feel for the language; the grammar is almost trivial. What is important is understanding the [semantics](000S) of Coln and the process of [elaboration](000O).}
+% \p{In practice, each declaration of this kind can be \em{lowered} into a database schema using a further [realm](TODO) declaration, which we defer discussion of until much later.}

manual/trees/000O.tree

@@ -6,7 +6,7 @@
   \taxon{Definition}
   \title{Syntax}
 
-  \p{Syntax is a data type in the Coln compiler, the elements of which are a compressed form for correct [derivations](derivation) in the Coln type theory.}
+  \p{Syntax is a data type that represents correct [derivations](derivation) in the Coln type theory. In the compiler, syntax is stored in a compressed form.}
 
   \p{The process of elaboration ensures that any syntax produced does in fact refer uniquely to some derivation.}
 }
@@ -15,7 +15,7 @@
   \taxon{Definition}
   \title{Notation}
 
-  \p{Notation is another data type in the Coln compiler. Notation is the first “tree-shaped” data type that is produced in the compilation pipeline, and is fairly permissive in terms of what is allowed.}
+  \p{Notation is another data type representing minimally processed Coln input; it is the first “tree-shaped” data type that is produced in the compilation pipeline, and is fairly permissive in terms of what is allowed.}
 
   \p{See [fnotation](000R) for a description of the notation used in Coln.}
 }

manual/trees/000R.tree

@@ -1,8 +1,11 @@
 \title{F-notation}
+\taxon{Appendix}
+\import{prelude}
+
 
 \p{Coln follows the philosophy of [[krishnamurthi-2024-bicameral]] in using a fairly unstructured “lower house syntax” as the target of parsing (or as [Krishnamurthi](shriram-krishnamurthi) calls it, “reading”). We use the term “notation” as a shorthand for “lower house syntax” in order to reserve the word “syntax” for [trees that compactly refer to derivations](000Q). Unlike a traditional LISP, we do not use s-expressions. Our notation is instead inspired by modern LISPs like [[julia]] and [[rhombus]]. We call it “f-notation” for no particular reason.}
 
-\p{In this section, we describe f-notation.}
+\p{In this section, we describe f-notation. \mvrnote{Some examples by this point, so the reader has something to cling to? Probably much sooner}}
 
 \transclude{000W}
 

manual/trees/000S.tree

@@ -1,43 +1,22 @@
-\title{Basic types}
+\title{Basic type constructors}
 \import{prelude}
 
-\p{At its core, there are only two things in the Coln language: types and elements of those types. We write \code{a : A} to express that \code{a} is an element of the type \code{A}. In this section, we describe informally the various types in Coln and how they are functionally involved in the database.}
+\p{In this section, we describe informally the various type constructors available in Coln.}
 
-\subtree[001F]{
-  \taxon{Slogan}
-  \title{Theories are schemas, models are instances}
-
-  \p{In Coln, we use the word \defcase{theory} to mean a type used as a database schema, and we say \defcase{model} to refer to an element of a theory, which you might also think of as a database instance on the schema described by that theory.}
-}
-
-\p{We now show how to build up progressively more complex theories via different type formers. In order to give an intuition for what each of these type formers means, we also describe how to interact with models of those theories via the TypeScript FFI (note: the TypeScript FFI is a work in progress at the moment).}
+\p{As we introduce each new type construction, we demonstrate the database schema produced by the Coln compiler, together with a valid instance of that schema. Click the "Example" heading to expand it. \mvrnote{forward link to more details}}
 
+\transclude{0031}
 \transclude{001B}
 \transclude{001C}
 \transclude{001D}
 \transclude{001E}
+\transclude{0034}
 \transclude{001G}
 \transclude{001I}
 
-\p{These six type formers ([[001B]], [[001C]], [[001D]], [[001E]], [[001G]] and [[001I]]) can be used to compositionally build up fairly complex combinatorial structures of sets, functions and relations. However, they are still limited when it comes to handling \em{data}, which often has, for instance, numbers and strings in it.}
-
-\p{We could simply put in \code{String} and \code{Int} in as “base sets”. However, this would permit functions \code{String -> String}, and we cannot store a function like that in a database because the set of strings is infinite and the function must be total, so storing the value of the function at every string would take infinite storage. We could say that \code{String} was a theory and not a set, which would prevent it from being used in the domain of a function, but it is perfectly sensible to have the theory \code{String -> Prop} (which denotes a subset of the set of all strings), and making \code{String} a theory would prevent us from forming that.}
-
-\p{The solution to this problem requires building up a little more theory, so we do not address it right now, and instead continue on to give a full account of the “purely combinatorial” fragment of Coln.}
-
-\subtree[001A]{
-  \taxon{Slogan}
-  \title{Sets are queries, elements are results}
-
-  \p{One can query a database in Coln via for-loops in TypeScript, but this is obviously not the most efficient or ergonomic way to do it. In fact, we already have the machinery to write down queries, it just requires a bit of rethinking what we have already learned. The idea is that giving a way to produce a set from a model of a theory is a query. The elements of that set are the results of the query.}
-}
-
-\transclude{001H}
-
-\transclude{001J}
-
-\transclude{001K}
-
-\transclude{001L}
+\p{These type formers ([[0031]], [[001B]], [[001C]], [[001D]],
+[[001E]], [[0034]], [[001G]] and [[001I]]) are individually simple,
+but can be composed to build complex combinatorial structures of sets,
+functions and relations.}
 
-\transclude{001M}
+\transclude{0036}