diff --git a/flake.lock b/flake.lock index 145fa01a..ffc04f1a 100644 --- a/flake.lock +++ b/flake.lock @@ -1,5 +1,26 @@ { "nodes": { + "bib2forester": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1782480966, + "narHash": "sha256-GwnoDQZ7Atb8EFrDKheM0pGRSQR9POcLglqDd/5FeJ4=", + "owner": "olynch", + "repo": "bib2forester", + "rev": "1099ec2f432c37b689870002e76f20c45c3a529e", + "type": "github" + }, + "original": { + "owner": "olynch", + "repo": "bib2forester", + "type": "github" + } + }, "flake-utils": { "inputs": { "systems": "systems" @@ -107,6 +128,7 @@ }, "root": { "inputs": { + "bib2forester": "bib2forester", "flake-utils": "flake-utils", "ghc-wasm-meta": "ghc-wasm-meta", "nixpkgs": "nixpkgs_2", diff --git a/flake.nix b/flake.nix index 860d0be0..fcbae972 100644 --- a/flake.nix +++ b/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 diff --git a/manual/templates/plain.tree b/manual/templates/plain.tree index e69de29b..a29ce570 100644 --- a/manual/templates/plain.tree +++ b/manual/templates/plain.tree @@ -0,0 +1 @@ +\import{prelude} diff --git a/manual/theme/forester.js b/manual/theme/forester.js index 9c8b046c..a7e1b019 100644 --- a/manual/theme/forester.js +++ b/manual/theme/forester.js @@ -685,7 +685,7 @@ l0,-`+(t+144)+`c-2,-159.3,-10,-310.7,-24,-454c-53.3,-528,-210,-949.7, |[ \r ]+ ?)[ \r ]*`,Yr="[\u0300-\u036F]",G1=new RegExp(Yr+"+$"),K1="("+Bi+"+)|"+(V1+"|")+"([!-\\[\\]-\u2027\u202A-\uD7FF\uF900-\uFFFF]"+(Yr+"*")+"|[\uD800-\uDBFF][\uDC00-\uDFFF]"+(Yr+"*")+"|\\\\verb\\*([^]).*?\\4|\\\\verb([^*a-zA-Z]).*?\\5"+("|"+U1)+("|"+F1+")"),Zt=class{constructor(e,t){this.input=void 0,this.settings=void 0,this.tokenRegex=void 0,this.catcodes=void 0,this.input=e,this.settings=t,this.tokenRegex=new RegExp(K1,"g"),this.catcodes={"%":14,"~":13}}setCatcode(e,t){this.catcodes[e]=t}lex(){var e=this.input,t=this.tokenRegex.lastIndex;if(t===e.length)return new C0("EOF",new A0(this,t,t));var a=this.tokenRegex.exec(e);if(a===null||a.index!==t)throw new T("Unexpected character: '"+e[t]+"'",new C0(e[t],new A0(this,t,t+1)));var n=a[6]||a[3]||(a[2]?"\\ ":" ");if(this.catcodes[n]===14){var i=e.indexOf(` `,this.tokenRegex.lastIndex);return i===-1?(this.tokenRegex.lastIndex=e.length,this.settings.reportNonstrict("commentAtEnd","% comment has no terminating newline; LaTeX would fail because of commenting the end of math mode (e.g. $)")):this.tokenRegex.lastIndex=i+1,this.lex()}return new C0(n,new A0(this,t,this.tokenRegex.lastIndex))}},Xr=class{constructor(e,t){e===void 0&&(e={}),t===void 0&&(t={}),this.current=void 0,this.builtins=void 0,this.undefStack=void 0,this.current=t,this.builtins=e,this.undefStack=[]}beginGroup(){this.undefStack.push({})}endGroup(){if(this.undefStack.length===0)throw new T("Unbalanced namespace destruction: attempt to pop global namespace; please report this as a bug");var e=this.undefStack.pop();for(var t in e)e.hasOwnProperty(t)&&(e[t]==null?delete this.current[t]:this.current[t]=e[t])}endGroups(){for(;this.undefStack.length>0;)this.endGroup()}has(e){return this.current.hasOwnProperty(e)||this.builtins.hasOwnProperty(e)}get(e){return this.current.hasOwnProperty(e)?this.current[e]:this.builtins[e]}set(e,t,a){if(a===void 0&&(a=!1),a){for(var n=0;n0&&(this.undefStack[this.undefStack.length-1][e]=t)}else{var i=this.undefStack[this.undefStack.length-1];i&&!i.hasOwnProperty(e)&&(i[e]=this.current[e])}t==null?delete this.current[e]:this.current[e]=t}},W1=bi;d("\\noexpand",function(r){var e=r.popToken();return r.isExpandable(e.text)&&(e.noexpand=!0,e.treatAsRelax=!0),{tokens:[e],numArgs:0}});d("\\expandafter",function(r){var e=r.popToken();return r.expandOnce(!0),{tokens:[e],numArgs:0}});d("\\@firstoftwo",function(r){var e=r.consumeArgs(2);return{tokens:e[0],numArgs:0}});d("\\@secondoftwo",function(r){var e=r.consumeArgs(2);return{tokens:e[1],numArgs:0}});d("\\@ifnextchar",function(r){var e=r.consumeArgs(3);r.consumeSpaces();var t=r.future();return e[0].length===1&&e[0][0].text===t.text?{tokens:e[1],numArgs:0}:{tokens:e[2],numArgs:0}});d("\\@ifstar","\\@ifnextchar *{\\@firstoftwo{#1}}");d("\\TextOrMath",function(r){var e=r.consumeArgs(2);return r.mode==="text"?{tokens:e[0],numArgs:0}:{tokens:e[1],numArgs:0}});var qn={0:0,1:1,2:2,3:3,4:4,5:5,6:6,7:7,8:8,9:9,a:10,A:10,b:11,B:11,c:12,C:12,d:13,D:13,e:14,E:14,f:15,F:15};d("\\char",function(r){var e=r.popToken(),t,a="";if(e.text==="'")t=8,e=r.popToken();else if(e.text==='"')t=16,e=r.popToken();else if(e.text==="`")if(e=r.popToken(),e.text[0]==="\\")a=e.text.charCodeAt(1);else{if(e.text==="EOF")throw new T("\\char` missing argument");a=e.text.charCodeAt(0)}else t=10;if(t){if(a=qn[e.text],a==null||a>=t)throw new T("Invalid base-"+t+" digit "+e.text);for(var n;(n=qn[r.future().text])!=null&&n{var a=r.consumeArg().tokens;if(a.length!==1)throw new T("\\newcommand's first argument must be a macro name");var n=a[0].text,i=r.isDefined(n);if(i&&!e)throw new T("\\newcommand{"+n+"} attempting to redefine "+(n+"; use \\renewcommand"));if(!i&&!t)throw new T("\\renewcommand{"+n+"} when command "+n+" does not yet exist; use \\newcommand");var l=0;if(a=r.consumeArg().tokens,a.length===1&&a[0].text==="["){for(var u="",h=r.expandNextToken();h.text!=="]"&&h.text!=="EOF";)u+=h.text,h=r.expandNextToken();if(!u.match(/^\s*[0-9]+\s*$/))throw new T("Invalid number of arguments: "+u);l=parseInt(u),a=r.consumeArg().tokens}return r.macros.set(n,{tokens:a,numArgs:l}),""};d("\\newcommand",r=>da(r,!1,!0));d("\\renewcommand",r=>da(r,!0,!1));d("\\providecommand",r=>da(r,!0,!0));d("\\message",r=>{var e=r.consumeArgs(1)[0];return console.log(e.reverse().map(t=>t.text).join("")),""});d("\\errmessage",r=>{var e=r.consumeArgs(1)[0];return console.error(e.reverse().map(t=>t.text).join("")),""});d("\\show",r=>{var e=r.popToken(),t=e.text;return console.log(e,r.macros.get(t),se[t],K.math[t],K.text[t]),""});d("\\bgroup","{");d("\\egroup","}");d("~","\\nobreakspace");d("\\lq","`");d("\\rq","'");d("\\aa","\\r a");d("\\AA","\\r A");d("\\textcopyright","\\html@mathml{\\textcircled{c}}{\\char`\xA9}");d("\\copyright","\\TextOrMath{\\textcopyright}{\\text{\\textcopyright}}");d("\\textregistered","\\html@mathml{\\textcircled{\\scriptsize R}}{\\char`\xAE}");d("\u212C","\\mathscr{B}");d("\u2130","\\mathscr{E}");d("\u2131","\\mathscr{F}");d("\u210B","\\mathscr{H}");d("\u2110","\\mathscr{I}");d("\u2112","\\mathscr{L}");d("\u2133","\\mathscr{M}");d("\u211B","\\mathscr{R}");d("\u212D","\\mathfrak{C}");d("\u210C","\\mathfrak{H}");d("\u2128","\\mathfrak{Z}");d("\\Bbbk","\\Bbb{k}");d("\xB7","\\cdotp");d("\\llap","\\mathllap{\\textrm{#1}}");d("\\rlap","\\mathrlap{\\textrm{#1}}");d("\\clap","\\mathclap{\\textrm{#1}}");d("\\mathstrut","\\vphantom{(}");d("\\underbar","\\underline{\\text{#1}}");d("\\not",'\\html@mathml{\\mathrel{\\mathrlap\\@not}}{\\char"338}');d("\\neq","\\html@mathml{\\mathrel{\\not=}}{\\mathrel{\\char`\u2260}}");d("\\ne","\\neq");d("\u2260","\\neq");d("\\notin","\\html@mathml{\\mathrel{{\\in}\\mathllap{/\\mskip1mu}}}{\\mathrel{\\char`\u2209}}");d("\u2209","\\notin");d("\u2258","\\html@mathml{\\mathrel{=\\kern{-1em}\\raisebox{0.4em}{$\\scriptsize\\frown$}}}{\\mathrel{\\char`\u2258}}");d("\u2259","\\html@mathml{\\stackrel{\\tiny\\wedge}{=}}{\\mathrel{\\char`\u2258}}");d("\u225A","\\html@mathml{\\stackrel{\\tiny\\vee}{=}}{\\mathrel{\\char`\u225A}}");d("\u225B","\\html@mathml{\\stackrel{\\scriptsize\\star}{=}}{\\mathrel{\\char`\u225B}}");d("\u225D","\\html@mathml{\\stackrel{\\tiny\\mathrm{def}}{=}}{\\mathrel{\\char`\u225D}}");d("\u225E","\\html@mathml{\\stackrel{\\tiny\\mathrm{m}}{=}}{\\mathrel{\\char`\u225E}}");d("\u225F","\\html@mathml{\\stackrel{\\tiny?}{=}}{\\mathrel{\\char`\u225F}}");d("\u27C2","\\perp");d("\u203C","\\mathclose{!\\mkern-0.8mu!}");d("\u220C","\\notni");d("\u231C","\\ulcorner");d("\u231D","\\urcorner");d("\u231E","\\llcorner");d("\u231F","\\lrcorner");d("\xA9","\\copyright");d("\xAE","\\textregistered");d("\uFE0F","\\textregistered");d("\\ulcorner",'\\html@mathml{\\@ulcorner}{\\mathop{\\char"231c}}');d("\\urcorner",'\\html@mathml{\\@urcorner}{\\mathop{\\char"231d}}');d("\\llcorner",'\\html@mathml{\\@llcorner}{\\mathop{\\char"231e}}');d("\\lrcorner",'\\html@mathml{\\@lrcorner}{\\mathop{\\char"231f}}');d("\\vdots","\\mathord{\\varvdots\\rule{0pt}{15pt}}");d("\u22EE","\\vdots");d("\\varGamma","\\mathit{\\Gamma}");d("\\varDelta","\\mathit{\\Delta}");d("\\varTheta","\\mathit{\\Theta}");d("\\varLambda","\\mathit{\\Lambda}");d("\\varXi","\\mathit{\\Xi}");d("\\varPi","\\mathit{\\Pi}");d("\\varSigma","\\mathit{\\Sigma}");d("\\varUpsilon","\\mathit{\\Upsilon}");d("\\varPhi","\\mathit{\\Phi}");d("\\varPsi","\\mathit{\\Psi}");d("\\varOmega","\\mathit{\\Omega}");d("\\substack","\\begin{subarray}{c}#1\\end{subarray}");d("\\colon","\\nobreak\\mskip2mu\\mathpunct{}\\mathchoice{\\mkern-3mu}{\\mkern-3mu}{}{}{:}\\mskip6mu\\relax");d("\\boxed","\\fbox{$\\displaystyle{#1}$}");d("\\iff","\\DOTSB\\;\\Longleftrightarrow\\;");d("\\implies","\\DOTSB\\;\\Longrightarrow\\;");d("\\impliedby","\\DOTSB\\;\\Longleftarrow\\;");var Hn={",":"\\dotsc","\\not":"\\dotsb","+":"\\dotsb","=":"\\dotsb","<":"\\dotsb",">":"\\dotsb","-":"\\dotsb","*":"\\dotsb",":":"\\dotsb","\\DOTSB":"\\dotsb","\\coprod":"\\dotsb","\\bigvee":"\\dotsb","\\bigwedge":"\\dotsb","\\biguplus":"\\dotsb","\\bigcap":"\\dotsb","\\bigcup":"\\dotsb","\\prod":"\\dotsb","\\sum":"\\dotsb","\\bigotimes":"\\dotsb","\\bigoplus":"\\dotsb","\\bigodot":"\\dotsb","\\bigsqcup":"\\dotsb","\\And":"\\dotsb","\\longrightarrow":"\\dotsb","\\Longrightarrow":"\\dotsb","\\longleftarrow":"\\dotsb","\\Longleftarrow":"\\dotsb","\\longleftrightarrow":"\\dotsb","\\Longleftrightarrow":"\\dotsb","\\mapsto":"\\dotsb","\\longmapsto":"\\dotsb","\\hookrightarrow":"\\dotsb","\\doteq":"\\dotsb","\\mathbin":"\\dotsb","\\mathrel":"\\dotsb","\\relbar":"\\dotsb","\\Relbar":"\\dotsb","\\xrightarrow":"\\dotsb","\\xleftarrow":"\\dotsb","\\DOTSI":"\\dotsi","\\int":"\\dotsi","\\oint":"\\dotsi","\\iint":"\\dotsi","\\iiint":"\\dotsi","\\iiiint":"\\dotsi","\\idotsint":"\\dotsi","\\DOTSX":"\\dotsx"};d("\\dots",function(r){var e="\\dotso",t=r.expandAfterFuture().text;return t in Hn?e=Hn[t]:(t.slice(0,4)==="\\not"||t in K.math&&$.contains(["bin","rel"],K.math[t].group))&&(e="\\dotsb"),e});var ma={")":!0,"]":!0,"\\rbrack":!0,"\\}":!0,"\\rbrace":!0,"\\rangle":!0,"\\rceil":!0,"\\rfloor":!0,"\\rgroup":!0,"\\rmoustache":!0,"\\right":!0,"\\bigr":!0,"\\biggr":!0,"\\Bigr":!0,"\\Biggr":!0,$:!0,";":!0,".":!0,",":!0};d("\\dotso",function(r){var e=r.future().text;return e in ma?"\\ldots\\,":"\\ldots"});d("\\dotsc",function(r){var e=r.future().text;return e in ma&&e!==","?"\\ldots\\,":"\\ldots"});d("\\cdots",function(r){var e=r.future().text;return e in ma?"\\@cdots\\,":"\\@cdots"});d("\\dotsb","\\cdots");d("\\dotsm","\\cdots");d("\\dotsi","\\!\\cdots");d("\\dotsx","\\ldots\\,");d("\\DOTSI","\\relax");d("\\DOTSB","\\relax");d("\\DOTSX","\\relax");d("\\tmspace","\\TextOrMath{\\kern#1#3}{\\mskip#1#2}\\relax");d("\\,","\\tmspace+{3mu}{.1667em}");d("\\thinspace","\\,");d("\\>","\\mskip{4mu}");d("\\:","\\tmspace+{4mu}{.2222em}");d("\\medspace","\\:");d("\\;","\\tmspace+{5mu}{.2777em}");d("\\thickspace","\\;");d("\\!","\\tmspace-{3mu}{.1667em}");d("\\negthinspace","\\!");d("\\negmedspace","\\tmspace-{4mu}{.2222em}");d("\\negthickspace","\\tmspace-{5mu}{.277em}");d("\\enspace","\\kern.5em ");d("\\enskip","\\hskip.5em\\relax");d("\\quad","\\hskip1em\\relax");d("\\qquad","\\hskip2em\\relax");d("\\tag","\\@ifstar\\tag@literal\\tag@paren");d("\\tag@paren","\\tag@literal{({#1})}");d("\\tag@literal",r=>{if(r.macros.get("\\df@tag"))throw new T("Multiple \\tag");return"\\gdef\\df@tag{\\text{#1}}"});d("\\bmod","\\mathchoice{\\mskip1mu}{\\mskip1mu}{\\mskip5mu}{\\mskip5mu}\\mathbin{\\rm mod}\\mathchoice{\\mskip1mu}{\\mskip1mu}{\\mskip5mu}{\\mskip5mu}");d("\\pod","\\allowbreak\\mathchoice{\\mkern18mu}{\\mkern8mu}{\\mkern8mu}{\\mkern8mu}(#1)");d("\\pmod","\\pod{{\\rm mod}\\mkern6mu#1}");d("\\mod","\\allowbreak\\mathchoice{\\mkern18mu}{\\mkern12mu}{\\mkern12mu}{\\mkern12mu}{\\rm mod}\\,\\,#1");d("\\newline","\\\\\\relax");d("\\TeX","\\textrm{\\html@mathml{T\\kern-.1667em\\raisebox{-.5ex}{E}\\kern-.125emX}{TeX}}");var Di=z(_0["Main-Regular"]["T".charCodeAt(0)][1]-.7*_0["Main-Regular"]["A".charCodeAt(0)][1]);d("\\LaTeX","\\textrm{\\html@mathml{"+("L\\kern-.36em\\raisebox{"+Di+"}{\\scriptstyle A}")+"\\kern-.15em\\TeX}{LaTeX}}");d("\\KaTeX","\\textrm{\\html@mathml{"+("K\\kern-.17em\\raisebox{"+Di+"}{\\scriptstyle A}")+"\\kern-.15em\\TeX}{KaTeX}}");d("\\hspace","\\@ifstar\\@hspacer\\@hspace");d("\\@hspace","\\hskip #1\\relax");d("\\@hspacer","\\rule{0pt}{0pt}\\hskip #1\\relax");d("\\ordinarycolon",":");d("\\vcentcolon","\\mathrel{\\mathop\\ordinarycolon}");d("\\dblcolon",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-.9mu}\\vcentcolon}}{\\mathop{\\char"2237}}');d("\\coloneqq",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-1.2mu}=}}{\\mathop{\\char"2254}}');d("\\Coloneqq",'\\html@mathml{\\mathrel{\\dblcolon\\mathrel{\\mkern-1.2mu}=}}{\\mathop{\\char"2237\\char"3d}}');d("\\coloneq",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-1.2mu}\\mathrel{-}}}{\\mathop{\\char"3a\\char"2212}}');d("\\Coloneq",'\\html@mathml{\\mathrel{\\dblcolon\\mathrel{\\mkern-1.2mu}\\mathrel{-}}}{\\mathop{\\char"2237\\char"2212}}');d("\\eqqcolon",'\\html@mathml{\\mathrel{=\\mathrel{\\mkern-1.2mu}\\vcentcolon}}{\\mathop{\\char"2255}}');d("\\Eqqcolon",'\\html@mathml{\\mathrel{=\\mathrel{\\mkern-1.2mu}\\dblcolon}}{\\mathop{\\char"3d\\char"2237}}');d("\\eqcolon",'\\html@mathml{\\mathrel{\\mathrel{-}\\mathrel{\\mkern-1.2mu}\\vcentcolon}}{\\mathop{\\char"2239}}');d("\\Eqcolon",'\\html@mathml{\\mathrel{\\mathrel{-}\\mathrel{\\mkern-1.2mu}\\dblcolon}}{\\mathop{\\char"2212\\char"2237}}');d("\\colonapprox",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-1.2mu}\\approx}}{\\mathop{\\char"3a\\char"2248}}');d("\\Colonapprox",'\\html@mathml{\\mathrel{\\dblcolon\\mathrel{\\mkern-1.2mu}\\approx}}{\\mathop{\\char"2237\\char"2248}}');d("\\colonsim",'\\html@mathml{\\mathrel{\\vcentcolon\\mathrel{\\mkern-1.2mu}\\sim}}{\\mathop{\\char"3a\\char"223c}}');d("\\Colonsim",'\\html@mathml{\\mathrel{\\dblcolon\\mathrel{\\mkern-1.2mu}\\sim}}{\\mathop{\\char"2237\\char"223c}}');d("\u2237","\\dblcolon");d("\u2239","\\eqcolon");d("\u2254","\\coloneqq");d("\u2255","\\eqqcolon");d("\u2A74","\\Coloneqq");d("\\ratio","\\vcentcolon");d("\\coloncolon","\\dblcolon");d("\\colonequals","\\coloneqq");d("\\coloncolonequals","\\Coloneqq");d("\\equalscolon","\\eqqcolon");d("\\equalscoloncolon","\\Eqqcolon");d("\\colonminus","\\coloneq");d("\\coloncolonminus","\\Coloneq");d("\\minuscolon","\\eqcolon");d("\\minuscoloncolon","\\Eqcolon");d("\\coloncolonapprox","\\Colonapprox");d("\\coloncolonsim","\\Colonsim");d("\\simcolon","\\mathrel{\\sim\\mathrel{\\mkern-1.2mu}\\vcentcolon}");d("\\simcoloncolon","\\mathrel{\\sim\\mathrel{\\mkern-1.2mu}\\dblcolon}");d("\\approxcolon","\\mathrel{\\approx\\mathrel{\\mkern-1.2mu}\\vcentcolon}");d("\\approxcoloncolon","\\mathrel{\\approx\\mathrel{\\mkern-1.2mu}\\dblcolon}");d("\\notni","\\html@mathml{\\not\\ni}{\\mathrel{\\char`\u220C}}");d("\\limsup","\\DOTSB\\operatorname*{lim\\,sup}");d("\\liminf","\\DOTSB\\operatorname*{lim\\,inf}");d("\\injlim","\\DOTSB\\operatorname*{inj\\,lim}");d("\\projlim","\\DOTSB\\operatorname*{proj\\,lim}");d("\\varlimsup","\\DOTSB\\operatorname*{\\overline{lim}}");d("\\varliminf","\\DOTSB\\operatorname*{\\underline{lim}}");d("\\varinjlim","\\DOTSB\\operatorname*{\\underrightarrow{lim}}");d("\\varprojlim","\\DOTSB\\operatorname*{\\underleftarrow{lim}}");d("\\gvertneqq","\\html@mathml{\\@gvertneqq}{\u2269}");d("\\lvertneqq","\\html@mathml{\\@lvertneqq}{\u2268}");d("\\ngeqq","\\html@mathml{\\@ngeqq}{\u2271}");d("\\ngeqslant","\\html@mathml{\\@ngeqslant}{\u2271}");d("\\nleqq","\\html@mathml{\\@nleqq}{\u2270}");d("\\nleqslant","\\html@mathml{\\@nleqslant}{\u2270}");d("\\nshortmid","\\html@mathml{\\@nshortmid}{\u2224}");d("\\nshortparallel","\\html@mathml{\\@nshortparallel}{\u2226}");d("\\nsubseteqq","\\html@mathml{\\@nsubseteqq}{\u2288}");d("\\nsupseteqq","\\html@mathml{\\@nsupseteqq}{\u2289}");d("\\varsubsetneq","\\html@mathml{\\@varsubsetneq}{\u228A}");d("\\varsubsetneqq","\\html@mathml{\\@varsubsetneqq}{\u2ACB}");d("\\varsupsetneq","\\html@mathml{\\@varsupsetneq}{\u228B}");d("\\varsupsetneqq","\\html@mathml{\\@varsupsetneqq}{\u2ACC}");d("\\imath","\\html@mathml{\\@imath}{\u0131}");d("\\jmath","\\html@mathml{\\@jmath}{\u0237}");d("\\llbracket","\\html@mathml{\\mathopen{[\\mkern-3.2mu[}}{\\mathopen{\\char`\u27E6}}");d("\\rrbracket","\\html@mathml{\\mathclose{]\\mkern-3.2mu]}}{\\mathclose{\\char`\u27E7}}");d("\u27E6","\\llbracket");d("\u27E7","\\rrbracket");d("\\lBrace","\\html@mathml{\\mathopen{\\{\\mkern-3.2mu[}}{\\mathopen{\\char`\u2983}}");d("\\rBrace","\\html@mathml{\\mathclose{]\\mkern-3.2mu\\}}}{\\mathclose{\\char`\u2984}}");d("\u2983","\\lBrace");d("\u2984","\\rBrace");d("\\minuso","\\mathbin{\\html@mathml{{\\mathrlap{\\mathchoice{\\kern{0.145em}}{\\kern{0.145em}}{\\kern{0.1015em}}{\\kern{0.0725em}}\\circ}{-}}}{\\char`\u29B5}}");d("\u29B5","\\minuso");d("\\darr","\\downarrow");d("\\dArr","\\Downarrow");d("\\Darr","\\Downarrow");d("\\lang","\\langle");d("\\rang","\\rangle");d("\\uarr","\\uparrow");d("\\uArr","\\Uparrow");d("\\Uarr","\\Uparrow");d("\\N","\\mathbb{N}");d("\\R","\\mathbb{R}");d("\\Z","\\mathbb{Z}");d("\\alef","\\aleph");d("\\alefsym","\\aleph");d("\\Alpha","\\mathrm{A}");d("\\Beta","\\mathrm{B}");d("\\bull","\\bullet");d("\\Chi","\\mathrm{X}");d("\\clubs","\\clubsuit");d("\\cnums","\\mathbb{C}");d("\\Complex","\\mathbb{C}");d("\\Dagger","\\ddagger");d("\\diamonds","\\diamondsuit");d("\\empty","\\emptyset");d("\\Epsilon","\\mathrm{E}");d("\\Eta","\\mathrm{H}");d("\\exist","\\exists");d("\\harr","\\leftrightarrow");d("\\hArr","\\Leftrightarrow");d("\\Harr","\\Leftrightarrow");d("\\hearts","\\heartsuit");d("\\image","\\Im");d("\\infin","\\infty");d("\\Iota","\\mathrm{I}");d("\\isin","\\in");d("\\Kappa","\\mathrm{K}");d("\\larr","\\leftarrow");d("\\lArr","\\Leftarrow");d("\\Larr","\\Leftarrow");d("\\lrarr","\\leftrightarrow");d("\\lrArr","\\Leftrightarrow");d("\\Lrarr","\\Leftrightarrow");d("\\Mu","\\mathrm{M}");d("\\natnums","\\mathbb{N}");d("\\Nu","\\mathrm{N}");d("\\Omicron","\\mathrm{O}");d("\\plusmn","\\pm");d("\\rarr","\\rightarrow");d("\\rArr","\\Rightarrow");d("\\Rarr","\\Rightarrow");d("\\real","\\Re");d("\\reals","\\mathbb{R}");d("\\Reals","\\mathbb{R}");d("\\Rho","\\mathrm{P}");d("\\sdot","\\cdot");d("\\sect","\\S");d("\\spades","\\spadesuit");d("\\sub","\\subset");d("\\sube","\\subseteq");d("\\supe","\\supseteq");d("\\Tau","\\mathrm{T}");d("\\thetasym","\\vartheta");d("\\weierp","\\wp");d("\\Zeta","\\mathrm{Z}");d("\\argmin","\\DOTSB\\operatorname*{arg\\,min}");d("\\argmax","\\DOTSB\\operatorname*{arg\\,max}");d("\\plim","\\DOTSB\\mathop{\\operatorname{plim}}\\limits");d("\\bra","\\mathinner{\\langle{#1}|}");d("\\ket","\\mathinner{|{#1}\\rangle}");d("\\braket","\\mathinner{\\langle{#1}\\rangle}");d("\\Bra","\\left\\langle#1\\right|");d("\\Ket","\\left|#1\\right\\rangle");var $i=r=>e=>{var t=e.consumeArg().tokens,a=e.consumeArg().tokens,n=e.consumeArg().tokens,i=e.consumeArg().tokens,l=e.macros.get("|"),u=e.macros.get("\\|");e.macros.beginGroup();var h=g=>b=>{r&&(b.macros.set("|",l),n.length&&b.macros.set("\\|",u));var x=g;if(!g&&n.length){var k=b.future();k.text==="|"&&(b.popToken(),x=!0)}return{tokens:x?n:a,numArgs:0}};e.macros.set("|",h(!1)),n.length&&e.macros.set("\\|",h(!0));var m=e.consumeArg().tokens,v=e.expandTokens([...i,...m,...t]);return e.macros.endGroup(),{tokens:v.reverse(),numArgs:0}};d("\\bra@ket",$i(!1));d("\\bra@set",$i(!0));d("\\Braket","\\bra@ket{\\left\\langle}{\\,\\middle\\vert\\,}{\\,\\middle\\vert\\,}{\\right\\rangle}");d("\\Set","\\bra@set{\\left\\{\\:}{\\;\\middle\\vert\\;}{\\;\\middle\\Vert\\;}{\\:\\right\\}}");d("\\set","\\bra@set{\\{\\,}{\\mid}{}{\\,\\}}");d("\\angln","{\\angl n}");d("\\blue","\\textcolor{##6495ed}{#1}");d("\\orange","\\textcolor{##ffa500}{#1}");d("\\pink","\\textcolor{##ff00af}{#1}");d("\\red","\\textcolor{##df0030}{#1}");d("\\green","\\textcolor{##28ae7b}{#1}");d("\\gray","\\textcolor{gray}{#1}");d("\\purple","\\textcolor{##9d38bd}{#1}");d("\\blueA","\\textcolor{##ccfaff}{#1}");d("\\blueB","\\textcolor{##80f6ff}{#1}");d("\\blueC","\\textcolor{##63d9ea}{#1}");d("\\blueD","\\textcolor{##11accd}{#1}");d("\\blueE","\\textcolor{##0c7f99}{#1}");d("\\tealA","\\textcolor{##94fff5}{#1}");d("\\tealB","\\textcolor{##26edd5}{#1}");d("\\tealC","\\textcolor{##01d1c1}{#1}");d("\\tealD","\\textcolor{##01a995}{#1}");d("\\tealE","\\textcolor{##208170}{#1}");d("\\greenA","\\textcolor{##b6ffb0}{#1}");d("\\greenB","\\textcolor{##8af281}{#1}");d("\\greenC","\\textcolor{##74cf70}{#1}");d("\\greenD","\\textcolor{##1fab54}{#1}");d("\\greenE","\\textcolor{##0d923f}{#1}");d("\\goldA","\\textcolor{##ffd0a9}{#1}");d("\\goldB","\\textcolor{##ffbb71}{#1}");d("\\goldC","\\textcolor{##ff9c39}{#1}");d("\\goldD","\\textcolor{##e07d10}{#1}");d("\\goldE","\\textcolor{##a75a05}{#1}");d("\\redA","\\textcolor{##fca9a9}{#1}");d("\\redB","\\textcolor{##ff8482}{#1}");d("\\redC","\\textcolor{##f9685d}{#1}");d("\\redD","\\textcolor{##e84d39}{#1}");d("\\redE","\\textcolor{##bc2612}{#1}");d("\\maroonA","\\textcolor{##ffbde0}{#1}");d("\\maroonB","\\textcolor{##ff92c6}{#1}");d("\\maroonC","\\textcolor{##ed5fa6}{#1}");d("\\maroonD","\\textcolor{##ca337c}{#1}");d("\\maroonE","\\textcolor{##9e034e}{#1}");d("\\purpleA","\\textcolor{##ddd7ff}{#1}");d("\\purpleB","\\textcolor{##c6b9fc}{#1}");d("\\purpleC","\\textcolor{##aa87ff}{#1}");d("\\purpleD","\\textcolor{##7854ab}{#1}");d("\\purpleE","\\textcolor{##543b78}{#1}");d("\\mintA","\\textcolor{##f5f9e8}{#1}");d("\\mintB","\\textcolor{##edf2df}{#1}");d("\\mintC","\\textcolor{##e0e5cc}{#1}");d("\\grayA","\\textcolor{##f6f7f7}{#1}");d("\\grayB","\\textcolor{##f0f1f2}{#1}");d("\\grayC","\\textcolor{##e3e5e6}{#1}");d("\\grayD","\\textcolor{##d6d8da}{#1}");d("\\grayE","\\textcolor{##babec2}{#1}");d("\\grayF","\\textcolor{##888d93}{#1}");d("\\grayG","\\textcolor{##626569}{#1}");d("\\grayH","\\textcolor{##3b3e40}{#1}");d("\\grayI","\\textcolor{##21242c}{#1}");d("\\kaBlue","\\textcolor{##314453}{#1}");d("\\kaGreen","\\textcolor{##71B307}{#1}");var Ni={"^":!0,_:!0,"\\limits":!0,"\\nolimits":!0},Zr=class{constructor(e,t,a){this.settings=void 0,this.expansionCount=void 0,this.lexer=void 0,this.macros=void 0,this.stack=void 0,this.mode=void 0,this.settings=t,this.expansionCount=0,this.feed(e),this.macros=new Xr(W1,t.macros),this.mode=a,this.stack=[]}feed(e){this.lexer=new Zt(e,this.settings)}switchMode(e){this.mode=e}beginGroup(){this.macros.beginGroup()}endGroup(){this.macros.endGroup()}endGroups(){this.macros.endGroups()}future(){return this.stack.length===0&&this.pushToken(this.lexer.lex()),this.stack[this.stack.length-1]}popToken(){return this.future(),this.stack.pop()}pushToken(e){this.stack.push(e)}pushTokens(e){this.stack.push(...e)}scanArgument(e){var t,a,n;if(e){if(this.consumeSpaces(),this.future().text!=="[")return null;t=this.popToken(),{tokens:n,end:a}=this.consumeArg(["]"])}else({tokens:n,start:t,end:a}=this.consumeArg());return this.pushToken(new C0("EOF",a.loc)),this.pushTokens(n),t.range(a,"")}consumeSpaces(){for(;;){var e=this.future();if(e.text===" ")this.stack.pop();else break}}consumeArg(e){var t=[],a=e&&e.length>0;a||this.consumeSpaces();var n=this.future(),i,l=0,u=0;do{if(i=this.popToken(),t.push(i),i.text==="{")++l;else if(i.text==="}"){if(--l,l===-1)throw new T("Extra }",i)}else if(i.text==="EOF")throw new T("Unexpected end of input in a macro argument, expected '"+(e&&a?e[u]:"}")+"'",i);if(e&&a)if((l===0||l===1&&e[u]==="{")&&i.text===e[u]){if(++u,u===e.length){t.splice(-u,u);break}}else u=0}while(l!==0||a);return n.text==="{"&&t[t.length-1].text==="}"&&(t.pop(),t.shift()),t.reverse(),{tokens:t,start:n,end:i}}consumeArgs(e,t){if(t){if(t.length!==e+1)throw new T("The length of delimiters doesn't match the number of args!");for(var a=t[0],n=0;nthis.settings.maxExpand)throw new T("Too many expansions: infinite loop or need to increase maxExpand setting")}expandOnce(e){var t=this.popToken(),a=t.text,n=t.noexpand?null:this._getExpansion(a);if(n==null||e&&n.unexpandable){if(e&&n==null&&a[0]==="\\"&&!this.isDefined(a))throw new T("Undefined control sequence: "+a);return this.pushToken(t),!1}this.countExpansion(1);var i=n.tokens,l=this.consumeArgs(n.numArgs,n.delimiters);if(n.numArgs){i=i.slice();for(var u=i.length-1;u>=0;--u){var h=i[u];if(h.text==="#"){if(u===0)throw new T("Incomplete placeholder at end of macro body",h);if(h=i[--u],h.text==="#")i.splice(u+1,1);else if(/^[1-9]$/.test(h.text))i.splice(u,2,...l[+h.text-1]);else throw new T("Not a valid argument number",h)}}}return this.pushTokens(i),i.length}expandAfterFuture(){return this.expandOnce(),this.future()}expandNextToken(){for(;;)if(this.expandOnce()===!1){var e=this.stack.pop();return e.treatAsRelax&&(e.text="\\relax"),e}throw new Error}expandMacro(e){return this.macros.has(e)?this.expandTokens([new C0(e)]):void 0}expandTokens(e){var t=[],a=this.stack.length;for(this.pushTokens(e);this.stack.length>a;)if(this.expandOnce(!0)===!1){var n=this.stack.pop();n.treatAsRelax&&(n.noexpand=!1,n.treatAsRelax=!1),t.push(n)}return this.countExpansion(t.length),t}expandMacroAsText(e){var t=this.expandMacro(e);return t&&t.map(a=>a.text).join("")}_getExpansion(e){var t=this.macros.get(e);if(t==null)return t;if(e.length===1){var a=this.lexer.catcodes[e];if(a!=null&&a!==13)return}var n=typeof t=="function"?t(this):t;if(typeof n=="string"){var i=0;if(n.indexOf("#")!==-1)for(var l=n.replace(/##/g,"");l.indexOf("#"+(i+1))!==-1;)++i;for(var u=new Zt(n,this.settings),h=[],m=u.lex();m.text!=="EOF";)h.push(m),m=u.lex();h.reverse();var v={tokens:h,numArgs:i};return v}return n}isDefined(e){return this.macros.has(e)||se.hasOwnProperty(e)||K.math.hasOwnProperty(e)||K.text.hasOwnProperty(e)||Ni.hasOwnProperty(e)}isExpandable(e){var t=this.macros.get(e);return t!=null?typeof t=="string"||typeof t=="function"||!t.unexpandable:se.hasOwnProperty(e)&&!se[e].primitive}},In=/^[₊₋₌₍₎₀₁₂₃₄₅₆₇₈₉ₐₑₕᵢⱼₖₗₘₙₒₚᵣₛₜᵤᵥₓᵦᵧᵨᵩᵪ]/,jt=Object.freeze({"\u208A":"+","\u208B":"-","\u208C":"=","\u208D":"(","\u208E":")","\u2080":"0","\u2081":"1","\u2082":"2","\u2083":"3","\u2084":"4","\u2085":"5","\u2086":"6","\u2087":"7","\u2088":"8","\u2089":"9","\u2090":"a","\u2091":"e","\u2095":"h","\u1D62":"i","\u2C7C":"j","\u2096":"k","\u2097":"l","\u2098":"m","\u2099":"n","\u2092":"o","\u209A":"p","\u1D63":"r","\u209B":"s","\u209C":"t","\u1D64":"u","\u1D65":"v","\u2093":"x","\u1D66":"\u03B2","\u1D67":"\u03B3","\u1D68":"\u03C1","\u1D69":"\u03D5","\u1D6A":"\u03C7","\u207A":"+","\u207B":"-","\u207C":"=","\u207D":"(","\u207E":")","\u2070":"0","\xB9":"1","\xB2":"2","\xB3":"3","\u2074":"4","\u2075":"5","\u2076":"6","\u2077":"7","\u2078":"8","\u2079":"9","\u1D2C":"A","\u1D2E":"B","\u1D30":"D","\u1D31":"E","\u1D33":"G","\u1D34":"H","\u1D35":"I","\u1D36":"J","\u1D37":"K","\u1D38":"L","\u1D39":"M","\u1D3A":"N","\u1D3C":"O","\u1D3E":"P","\u1D3F":"R","\u1D40":"T","\u1D41":"U","\u2C7D":"V","\u1D42":"W","\u1D43":"a","\u1D47":"b","\u1D9C":"c","\u1D48":"d","\u1D49":"e","\u1DA0":"f","\u1D4D":"g",\u02B0:"h","\u2071":"i",\u02B2:"j","\u1D4F":"k",\u02E1:"l","\u1D50":"m",\u207F:"n","\u1D52":"o","\u1D56":"p",\u02B3:"r",\u02E2:"s","\u1D57":"t","\u1D58":"u","\u1D5B":"v",\u02B7:"w",\u02E3:"x",\u02B8:"y","\u1DBB":"z","\u1D5D":"\u03B2","\u1D5E":"\u03B3","\u1D5F":"\u03B4","\u1D60":"\u03D5","\u1D61":"\u03C7","\u1DBF":"\u03B8"}),Ir={"\u0301":{text:"\\'",math:"\\acute"},"\u0300":{text:"\\`",math:"\\grave"},"\u0308":{text:'\\"',math:"\\ddot"},"\u0303":{text:"\\~",math:"\\tilde"},"\u0304":{text:"\\=",math:"\\bar"},"\u0306":{text:"\\u",math:"\\breve"},"\u030C":{text:"\\v",math:"\\check"},"\u0302":{text:"\\^",math:"\\hat"},"\u0307":{text:"\\.",math:"\\dot"},"\u030A":{text:"\\r",math:"\\mathring"},"\u030B":{text:"\\H"},"\u0327":{text:"\\c"}},Pn={\u00E1:"a\u0301",\u00E0:"a\u0300",\u00E4:"a\u0308",\u01DF:"a\u0308\u0304",\u00E3:"a\u0303",\u0101:"a\u0304",\u0103:"a\u0306",\u1EAF:"a\u0306\u0301",\u1EB1:"a\u0306\u0300",\u1EB5:"a\u0306\u0303",\u01CE:"a\u030C",\u00E2:"a\u0302",\u1EA5:"a\u0302\u0301",\u1EA7:"a\u0302\u0300",\u1EAB:"a\u0302\u0303",\u0227:"a\u0307",\u01E1:"a\u0307\u0304",\u00E5:"a\u030A",\u01FB:"a\u030A\u0301",\u1E03:"b\u0307",\u0107:"c\u0301",\u1E09:"c\u0327\u0301",\u010D:"c\u030C",\u0109:"c\u0302",\u010B:"c\u0307",\u00E7:"c\u0327",\u010F:"d\u030C",\u1E0B:"d\u0307",\u1E11:"d\u0327",\u00E9:"e\u0301",\u00E8:"e\u0300",\u00EB:"e\u0308",\u1EBD:"e\u0303",\u0113:"e\u0304",\u1E17:"e\u0304\u0301",\u1E15:"e\u0304\u0300",\u0115:"e\u0306",\u1E1D:"e\u0327\u0306",\u011B:"e\u030C",\u00EA:"e\u0302",\u1EBF:"e\u0302\u0301",\u1EC1:"e\u0302\u0300",\u1EC5:"e\u0302\u0303",\u0117:"e\u0307",\u0229:"e\u0327",\u1E1F:"f\u0307",\u01F5:"g\u0301",\u1E21:"g\u0304",\u011F:"g\u0306",\u01E7:"g\u030C",\u011D:"g\u0302",\u0121:"g\u0307",\u0123:"g\u0327",\u1E27:"h\u0308",\u021F:"h\u030C",\u0125:"h\u0302",\u1E23:"h\u0307",\u1E29:"h\u0327",\u00ED:"i\u0301",\u00EC:"i\u0300",\u00EF:"i\u0308",\u1E2F:"i\u0308\u0301",\u0129:"i\u0303",\u012B:"i\u0304",\u012D:"i\u0306",\u01D0:"i\u030C",\u00EE:"i\u0302",\u01F0:"j\u030C",\u0135:"j\u0302",\u1E31:"k\u0301",\u01E9:"k\u030C",\u0137:"k\u0327",\u013A:"l\u0301",\u013E:"l\u030C",\u013C:"l\u0327",\u1E3F:"m\u0301",\u1E41:"m\u0307",\u0144:"n\u0301",\u01F9:"n\u0300",\u00F1:"n\u0303",\u0148:"n\u030C",\u1E45:"n\u0307",\u0146:"n\u0327",\u00F3:"o\u0301",\u00F2:"o\u0300",\u00F6:"o\u0308",\u022B:"o\u0308\u0304",\u00F5:"o\u0303",\u1E4D:"o\u0303\u0301",\u1E4F:"o\u0303\u0308",\u022D:"o\u0303\u0304",\u014D:"o\u0304",\u1E53:"o\u0304\u0301",\u1E51:"o\u0304\u0300",\u014F:"o\u0306",\u01D2:"o\u030C",\u00F4:"o\u0302",\u1ED1:"o\u0302\u0301",\u1ED3:"o\u0302\u0300",\u1ED7:"o\u0302\u0303",\u022F:"o\u0307",\u0231:"o\u0307\u0304",\u0151:"o\u030B",\u1E55:"p\u0301",\u1E57:"p\u0307",\u0155:"r\u0301",\u0159:"r\u030C",\u1E59:"r\u0307",\u0157:"r\u0327",\u015B:"s\u0301",\u1E65:"s\u0301\u0307",\u0161:"s\u030C",\u1E67:"s\u030C\u0307",\u015D:"s\u0302",\u1E61:"s\u0307",\u015F:"s\u0327",\u1E97:"t\u0308",\u0165:"t\u030C",\u1E6B:"t\u0307",\u0163:"t\u0327",\u00FA:"u\u0301",\u00F9:"u\u0300",\u00FC:"u\u0308",\u01D8:"u\u0308\u0301",\u01DC:"u\u0308\u0300",\u01D6:"u\u0308\u0304",\u01DA:"u\u0308\u030C",\u0169:"u\u0303",\u1E79:"u\u0303\u0301",\u016B:"u\u0304",\u1E7B:"u\u0304\u0308",\u016D:"u\u0306",\u01D4:"u\u030C",\u00FB:"u\u0302",\u016F:"u\u030A",\u0171:"u\u030B",\u1E7D:"v\u0303",\u1E83:"w\u0301",\u1E81:"w\u0300",\u1E85:"w\u0308",\u0175:"w\u0302",\u1E87:"w\u0307",\u1E98:"w\u030A",\u1E8D:"x\u0308",\u1E8B:"x\u0307",\u00FD:"y\u0301",\u1EF3:"y\u0300",\u00FF:"y\u0308",\u1EF9:"y\u0303",\u0233:"y\u0304",\u0177:"y\u0302",\u1E8F:"y\u0307",\u1E99:"y\u030A",\u017A:"z\u0301",\u017E:"z\u030C",\u1E91:"z\u0302",\u017C:"z\u0307",\u00C1:"A\u0301",\u00C0:"A\u0300",\u00C4:"A\u0308",\u01DE:"A\u0308\u0304",\u00C3:"A\u0303",\u0100:"A\u0304",\u0102:"A\u0306",\u1EAE:"A\u0306\u0301",\u1EB0:"A\u0306\u0300",\u1EB4:"A\u0306\u0303",\u01CD:"A\u030C",\u00C2:"A\u0302",\u1EA4:"A\u0302\u0301",\u1EA6:"A\u0302\u0300",\u1EAA:"A\u0302\u0303",\u0226:"A\u0307",\u01E0:"A\u0307\u0304",\u00C5:"A\u030A",\u01FA:"A\u030A\u0301",\u1E02:"B\u0307",\u0106:"C\u0301",\u1E08:"C\u0327\u0301",\u010C:"C\u030C",\u0108:"C\u0302",\u010A:"C\u0307",\u00C7:"C\u0327",\u010E:"D\u030C",\u1E0A:"D\u0307",\u1E10:"D\u0327",\u00C9:"E\u0301",\u00C8:"E\u0300",\u00CB:"E\u0308",\u1EBC:"E\u0303",\u0112:"E\u0304",\u1E16:"E\u0304\u0301",\u1E14:"E\u0304\u0300",\u0114:"E\u0306",\u1E1C:"E\u0327\u0306",\u011A:"E\u030C",\u00CA:"E\u0302",\u1EBE:"E\u0302\u0301",\u1EC0:"E\u0302\u0300",\u1EC4:"E\u0302\u0303",\u0116:"E\u0307",\u0228:"E\u0327",\u1E1E:"F\u0307",\u01F4:"G\u0301",\u1E20:"G\u0304",\u011E:"G\u0306",\u01E6:"G\u030C",\u011C:"G\u0302",\u0120:"G\u0307",\u0122:"G\u0327",\u1E26:"H\u0308",\u021E:"H\u030C",\u0124:"H\u0302",\u1E22:"H\u0307",\u1E28:"H\u0327",\u00CD:"I\u0301",\u00CC:"I\u0300",\u00CF:"I\u0308",\u1E2E:"I\u0308\u0301",\u0128:"I\u0303",\u012A:"I\u0304",\u012C:"I\u0306",\u01CF:"I\u030C",\u00CE:"I\u0302",\u0130:"I\u0307",\u0134:"J\u0302",\u1E30:"K\u0301",\u01E8:"K\u030C",\u0136:"K\u0327",\u0139:"L\u0301",\u013D:"L\u030C",\u013B:"L\u0327",\u1E3E:"M\u0301",\u1E40:"M\u0307",\u0143:"N\u0301",\u01F8:"N\u0300",\u00D1:"N\u0303",\u0147:"N\u030C",\u1E44:"N\u0307",\u0145:"N\u0327",\u00D3:"O\u0301",\u00D2:"O\u0300",\u00D6:"O\u0308",\u022A:"O\u0308\u0304",\u00D5:"O\u0303",\u1E4C:"O\u0303\u0301",\u1E4E:"O\u0303\u0308",\u022C:"O\u0303\u0304",\u014C:"O\u0304",\u1E52:"O\u0304\u0301",\u1E50:"O\u0304\u0300",\u014E:"O\u0306",\u01D1:"O\u030C",\u00D4:"O\u0302",\u1ED0:"O\u0302\u0301",\u1ED2:"O\u0302\u0300",\u1ED6:"O\u0302\u0303",\u022E:"O\u0307",\u0230:"O\u0307\u0304",\u0150:"O\u030B",\u1E54:"P\u0301",\u1E56:"P\u0307",\u0154:"R\u0301",\u0158:"R\u030C",\u1E58:"R\u0307",\u0156:"R\u0327",\u015A:"S\u0301",\u1E64:"S\u0301\u0307",\u0160:"S\u030C",\u1E66:"S\u030C\u0307",\u015C:"S\u0302",\u1E60:"S\u0307",\u015E:"S\u0327",\u0164:"T\u030C",\u1E6A:"T\u0307",\u0162:"T\u0327",\u00DA:"U\u0301",\u00D9:"U\u0300",\u00DC:"U\u0308",\u01D7:"U\u0308\u0301",\u01DB:"U\u0308\u0300",\u01D5:"U\u0308\u0304",\u01D9:"U\u0308\u030C",\u0168:"U\u0303",\u1E78:"U\u0303\u0301",\u016A:"U\u0304",\u1E7A:"U\u0304\u0308",\u016C:"U\u0306",\u01D3:"U\u030C",\u00DB:"U\u0302",\u016E:"U\u030A",\u0170:"U\u030B",\u1E7C:"V\u0303",\u1E82:"W\u0301",\u1E80:"W\u0300",\u1E84:"W\u0308",\u0174:"W\u0302",\u1E86:"W\u0307",\u1E8C:"X\u0308",\u1E8A:"X\u0307",\u00DD:"Y\u0301",\u1EF2:"Y\u0300",\u0178:"Y\u0308",\u1EF8:"Y\u0303",\u0232:"Y\u0304",\u0176:"Y\u0302",\u1E8E:"Y\u0307",\u0179:"Z\u0301",\u017D:"Z\u030C",\u1E90:"Z\u0302",\u017B:"Z\u0307",\u03AC:"\u03B1\u0301",\u1F70:"\u03B1\u0300",\u1FB1:"\u03B1\u0304",\u1FB0:"\u03B1\u0306",\u03AD:"\u03B5\u0301",\u1F72:"\u03B5\u0300",\u03AE:"\u03B7\u0301",\u1F74:"\u03B7\u0300",\u03AF:"\u03B9\u0301",\u1F76:"\u03B9\u0300",\u03CA:"\u03B9\u0308",\u0390:"\u03B9\u0308\u0301",\u1FD2:"\u03B9\u0308\u0300",\u1FD1:"\u03B9\u0304",\u1FD0:"\u03B9\u0306",\u03CC:"\u03BF\u0301",\u1F78:"\u03BF\u0300",\u03CD:"\u03C5\u0301",\u1F7A:"\u03C5\u0300",\u03CB:"\u03C5\u0308",\u03B0:"\u03C5\u0308\u0301",\u1FE2:"\u03C5\u0308\u0300",\u1FE1:"\u03C5\u0304",\u1FE0:"\u03C5\u0306",\u03CE:"\u03C9\u0301",\u1F7C:"\u03C9\u0300",\u038E:"\u03A5\u0301",\u1FEA:"\u03A5\u0300",\u03AB:"\u03A5\u0308",\u1FE9:"\u03A5\u0304",\u1FE8:"\u03A5\u0306",\u038F:"\u03A9\u0301",\u1FFA:"\u03A9\u0300"},Jt=class r{constructor(e,t){this.mode=void 0,this.gullet=void 0,this.settings=void 0,this.leftrightDepth=void 0,this.nextToken=void 0,this.mode="math",this.gullet=new Zr(e,t,this.mode),this.settings=t,this.leftrightDepth=0}expect(e,t){if(t===void 0&&(t=!0),this.fetch().text!==e)throw new T("Expected '"+e+"', got '"+this.fetch().text+"'",this.fetch());t&&this.consume()}consume(){this.nextToken=null}fetch(){return this.nextToken==null&&(this.nextToken=this.gullet.expandNextToken()),this.nextToken}switchMode(e){this.mode=e,this.gullet.switchMode(e)}parse(){this.settings.globalGroup||this.gullet.beginGroup(),this.settings.colorIsTextColor&&this.gullet.macros.set("\\color","\\textcolor");try{var e=this.parseExpression(!1);return this.expect("EOF"),this.settings.globalGroup||this.gullet.endGroup(),e}finally{this.gullet.endGroups()}}subparse(e){var t=this.nextToken;this.consume(),this.gullet.pushToken(new C0("}")),this.gullet.pushTokens(e);var a=this.parseExpression(!1);return this.expect("}"),this.nextToken=t,a}parseExpression(e,t){for(var a=[];;){this.mode==="math"&&this.consumeSpaces();var n=this.fetch();if(r.endOfExpression.indexOf(n.text)!==-1||t&&n.text===t||e&&se[n.text]&&se[n.text].infix)break;var i=this.parseAtom(t);if(i){if(i.type==="internal")continue}else break;a.push(i)}return this.mode==="text"&&this.formLigatures(a),this.handleInfixNodes(a)}handleInfixNodes(e){for(var t=-1,a,n=0;n=0&&this.settings.reportNonstrict("unicodeTextInMathMode",'Latin-1/Unicode text character "'+t[0]+'" used in math mode',e);var u=K[this.mode][t].group,h=A0.range(e),m;if(Is.hasOwnProperty(u)){var v=u;m={type:"atom",mode:this.mode,family:v,loc:h,text:t}}else m={type:u,mode:this.mode,loc:h,text:t};l=m}else if(t.charCodeAt(0)>=128)this.settings.strict&&(jn(t.charCodeAt(0))?this.mode==="math"&&this.settings.reportNonstrict("unicodeTextInMathMode",'Unicode text character "'+t[0]+'" used in math mode',e):this.settings.reportNonstrict("unknownSymbol",'Unrecognized Unicode character "'+t[0]+'"'+(" ("+t.charCodeAt(0)+")"),e)),l={type:"textord",mode:"text",loc:A0.range(e),text:t};else return null;if(this.consume(),i)for(var g=0;gQ1(m.left)).join("|")+")");a=e.search(i),a!==-1;){a>0&&(n.push({type:"text",data:e.slice(0,a)}),e=e.slice(a));var l=t.findIndex(m=>e.startsWith(m.left));if(a=J1(t[l].right,e,t[l].left.length),a===-1)break;var u=e.slice(0,a+t[l].right.length),h=el.test(u)?u:e.slice(t[l].left.length,a);n.push({type:"math",data:h,rawData:u,display:t[l].display}),e=e.slice(a+t[l].right.length)}return e!==""&&n.push({type:"text",data:e}),n},rl=function(e,t){var a=tl(e,t.delimiters);if(a.length===1&&a[0].type==="text")return null;for(var n=document.createDocumentFragment(),i=0;iv.indexOf(" "+b+" ")===-1);g&&r(n,t)}()}},_i=function(e,t){if(!e)throw new Error("No element provided to render");var a={};for(var n in t)t.hasOwnProperty(n)&&(a[n]=t[n]);a.delimiters=a.delimiters||[{left:"$$",right:"$$",display:!0},{left:"\\(",right:"\\)",display:!1},{left:"\\begin{equation}",right:"\\end{equation}",display:!0},{left:"\\begin{align}",right:"\\end{align}",display:!0},{left:"\\begin{alignat}",right:"\\end{alignat}",display:!0},{left:"\\begin{gather}",right:"\\end{gather}",display:!0},{left:"\\begin{CD}",right:"\\end{CD}",display:!0},{left:"\\[",right:"\\]",display:!0}],a.ignoredTags=a.ignoredTags||["script","noscript","style","textarea","pre","code","option"],a.ignoredClasses=a.ignoredClasses||[],a.errorCallback=a.errorCallback||console.error,a.macros=a.macros||{},al(e,a)};function nl(r,e){return r.reduce(([t,a],n)=>e(n)?[[...t,n],a]:[t,[...a,n]],[[],[]])}window.addEventListener("load",r=>{_i(document.body);let e=l=>{for(;l!=null;)l.nodeName=="DETAILS"&&(l.open=!0),l=l.parentNode},t=l=>{if(l.target.tagName==="A")return;let h=l.target.closest("span[data-target]").getAttribute("data-target"),m=document.querySelector(h);e(m),window.location=h};[...document.querySelectorAll("[data-target^='#']")].forEach(l=>l.addEventListener("click",t));let a=document.querySelector("ninja-keys"),i=`${document.querySelector("html").getAttribute("data-base-url")}forest.json`;fetch(i).then(l=>l.json()).then(l=>{let u=[],h='',m='';window.sourcePath&&u.push({id:"edit",title:"Edit current tree in Visual Studio Code",section:"Commands",hotkey:"cmd+e",icon:h,handler:()=>{window.location.href=`vscode://file/${window.sourcePath}`}});let v=k=>k.tags?k.tags.includes("top"):!1,g=(k,A,C)=>{let R=`${k.taxon?k.title?`${k.taxon}. ${k.title}`:k.taxon:k.title?k.title:"Untitled"} [${k.uri}]`;u.push({id:k.uri,title:R,section:A,icon:C,handler:()=>{window.location.href=k.route}})},[b,x]=nl(l,v);b.forEach(k=>g(k,"Top Trees",m)),x.forEach(k=>g(k,"All Trees",null)),a.data=u})});var il=2e3,st;function qi(){st=new EventSource("/refresh"),st.onmessage=function(r){r.data=="refresh"?(st.close(),location.reload()):console.log(r.data)},st.onerror=function(r){st.close(),setTimeout(qi,il)}}qi();})(); + please report what input caused this bug`);return a=a.slice(1,-1),{type:"verb",mode:"text",body:a,star:n}}Pn.hasOwnProperty(t[0])&&!K[this.mode][t[0]]&&(this.settings.strict&&this.mode==="math"&&this.settings.reportNonstrict("unicodeTextInMathMode",'Accented Unicode text character "'+t[0]+'" used in math mode',e),t=Pn[t[0]]+t.slice(1));var i=G1.exec(t);i&&(t=t.substring(0,i.index),t==="i"?t="\u0131":t==="j"&&(t="\u0237"));var l;if(K[this.mode][t]){this.settings.strict&&this.mode==="math"&&Fr.indexOf(t)>=0&&this.settings.reportNonstrict("unicodeTextInMathMode",'Latin-1/Unicode text character "'+t[0]+'" used in math mode',e);var u=K[this.mode][t].group,h=A0.range(e),m;if(Is.hasOwnProperty(u)){var v=u;m={type:"atom",mode:this.mode,family:v,loc:h,text:t}}else m={type:u,mode:this.mode,loc:h,text:t};l=m}else if(t.charCodeAt(0)>=128)this.settings.strict&&(jn(t.charCodeAt(0))?this.mode==="math"&&this.settings.reportNonstrict("unicodeTextInMathMode",'Unicode text character "'+t[0]+'" used in math mode',e):this.settings.reportNonstrict("unknownSymbol",'Unrecognized Unicode character "'+t[0]+'"'+(" ("+t.charCodeAt(0)+")"),e)),l={type:"textord",mode:"text",loc:A0.range(e),text:t};else return null;if(this.consume(),i)for(var g=0;gQ1(m.left)).join("|")+")");a=e.search(i),a!==-1;){a>0&&(n.push({type:"text",data:e.slice(0,a)}),e=e.slice(a));var l=t.findIndex(m=>e.startsWith(m.left));if(a=J1(t[l].right,e,t[l].left.length),a===-1)break;var u=e.slice(0,a+t[l].right.length),h=el.test(u)?u:e.slice(t[l].left.length,a);n.push({type:"math",data:h,rawData:u,display:t[l].display}),e=e.slice(a+t[l].right.length)}return e!==""&&n.push({type:"text",data:e}),n},rl=function(e,t){var a=tl(e,t.delimiters);if(a.length===1&&a[0].type==="text")return null;for(var n=document.createDocumentFragment(),i=0;iv.indexOf(" "+b+" ")===-1);g&&r(n,t)}()}},_i=function(e,t){if(!e)throw new Error("No element provided to render");var a={};for(var n in t)t.hasOwnProperty(n)&&(a[n]=t[n]);a.delimiters=a.delimiters||[{left:"$$",right:"$$",display:!0},{left:"\\(",right:"\\)",display:!1},{left:"\\begin{equation}",right:"\\end{equation}",display:!0},{left:"\\begin{align}",right:"\\end{align}",display:!0},{left:"\\begin{alignat}",right:"\\end{alignat}",display:!0},{left:"\\begin{gather}",right:"\\end{gather}",display:!0},{left:"\\begin{CD}",right:"\\end{CD}",display:!0},{left:"\\[",right:"\\]",display:!0}],a.ignoredTags=a.ignoredTags||["script","noscript","style","textarea","pre","code","option"],a.ignoredClasses=a.ignoredClasses||[],a.errorCallback=a.errorCallback||console.error,a.macros=a.macros||{},al(e,a)};function nl(r,e){return r.reduce(([t,a],n)=>e(n)?[[...t,n],a]:[t,[...a,n]],[[],[]])}window.addEventListener("load",r=>{_i(document.body,{fleqn:!0});let e=l=>{for(;l!=null;)l.nodeName=="DETAILS"&&(l.open=!0),l=l.parentNode},t=l=>{if(l.target.tagName==="A")return;let h=l.target.closest("span[data-target]").getAttribute("data-target"),m=document.querySelector(h);e(m),window.location=h};[...document.querySelectorAll("[data-target^='#']")].forEach(l=>l.addEventListener("click",t));let a=document.querySelector("ninja-keys"),i=`${document.querySelector("html").getAttribute("data-base-url")}forest.json`;fetch(i).then(l=>l.json()).then(l=>{let u=[],h='',m='';window.sourcePath&&u.push({id:"edit",title:"Edit current tree in Visual Studio Code",section:"Commands",hotkey:"cmd+e",icon:h,handler:()=>{window.location.href=`vscode://file/${window.sourcePath}`}});let v=k=>k.tags?k.tags.includes("top"):!1,g=(k,A,C)=>{let R=`${k.taxon?k.title?`${k.taxon}. ${k.title}`:k.taxon:k.title?k.title:"Untitled"} [${k.uri}]`;u.push({id:k.uri,title:R,section:A,icon:C,handler:()=>{window.location.href=k.route}})},[b,x]=nl(l,v);b.forEach(k=>g(k,"Top Trees",m)),x.forEach(k=>g(k,"All Trees",null)),a.data=u})});var il=2e3,st;function qi(){st=new EventSource("/refresh"),st.onmessage=function(r){r.data=="refresh"?(st.close(),location.reload()):console.log(r.data)},st.onerror=function(r){st.close(),setTimeout(qi,il)}}qi();})(); /*! Bundled license information: @lit/reactive-element/css-tag.js: diff --git a/manual/theme/javascript-source/forester.js b/manual/theme/javascript-source/forester.js index c99e90a6..a27a8ea7 100644 --- a/manual/theme/javascript-source/forester.js +++ b/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) { diff --git a/manual/theme/style.css b/manual/theme/style.css index a2d4c4e3..67180b3c 100644 --- a/manual/theme/style.css +++ b/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; } diff --git a/manual/trees/0001.tree b/manual/trees/0001.tree index d6d04343..b8b9bf43 100644 --- a/manual/trees/0001.tree +++ b/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} diff --git a/manual/trees/0002.tree b/manual/trees/0002.tree index 31903d18..559fef62 100644 --- a/manual/trees/0002.tree +++ b/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} diff --git a/manual/trees/000B.tree b/manual/trees/000B.tree index 87603513..2a92fb50 100644 --- a/manual/trees/000B.tree +++ b/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.} diff --git a/manual/trees/000G.tree b/manual/trees/000G.tree index 243eebbe..4e2cc65b 100644 --- a/manual/trees/000G.tree +++ b/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.} diff --git a/manual/trees/000I.tree b/manual/trees/000I.tree index 082e2790..0e0c9824 100644 --- a/manual/trees/000I.tree +++ b/manual/trees/000I.tree @@ -1,3 +1,4 @@ \title{Organization} +\import{prelude} -\p{} +\p{\mvrnote{TODO}} diff --git a/manual/trees/000K.tree b/manual/trees/000K.tree index da5cbb45..d1161e08 100644 --- a/manual/trees/000K.tree +++ b/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} diff --git a/manual/trees/000L.tree b/manual/trees/000L.tree index 86ba0a40..eaf73272 100644 --- a/manual/trees/000L.tree +++ b/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} diff --git a/manual/trees/000M.tree b/manual/trees/000M.tree index e980b737..c3b03230 100644 --- a/manual/trees/000M.tree +++ b/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.”} diff --git a/manual/trees/000N.tree b/manual/trees/000N.tree index 7b63ea17..281fdba3 100644 --- a/manual/trees/000N.tree +++ b/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} 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} 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.} diff --git a/manual/trees/000O.tree b/manual/trees/000O.tree index 10e83266..eb8a970f 100644 --- a/manual/trees/000O.tree +++ b/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.} } diff --git a/manual/trees/000R.tree b/manual/trees/000R.tree index 491525d5..a5f1a5f5 100644 --- a/manual/trees/000R.tree +++ b/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} diff --git a/manual/trees/000S.tree b/manual/trees/000S.tree index 8812c49e..8732af47 100644 --- a/manual/trees/000S.tree +++ b/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} diff --git a/manual/trees/000Y.tree b/manual/trees/000Y.tree index 0e7578f9..2cac0380 100644 --- a/manual/trees/000Y.tree +++ b/manual/trees/000Y.tree @@ -1,4 +1,4 @@ -\title{Trees} +\title{Notation} \import{prelude} \p{From tokens, the tree structure of f-notation is fairly simple. We give the main syntactic constructs here.} @@ -14,7 +14,7 @@ \li{[[0011]]} } - \p{The exception is [declarations](0012) which may only appear in [blocks](0012); a block contains \em{statements} which are either declarations or expressions. However, a block is an expression.} + \p{The exception is [declarations](0012) which may only appear in [blocks](0012); a block contains \em{statements} which are either declarations or expressions. However, a block is itself an expression.} } \subtree[000Z]{ @@ -32,11 +32,13 @@ \subtree[0011]{ \title{Juxtaposition and infix application} - \p{\defcase{Juxtaposition} is two expressions next to each other, like \code{f x}. As \code{a.b} lexes as two tokens, \code{a} and \code{.b}, this is also a juxtaposition.} + \p{\defcase{Juxtaposition} is the placement of two expressions next to each other, like \code{f x}. Juxtaposition left associates, so \code{f a b} is \code{(f a) b}.} + + \p{An exception is made for "immediate" field accessors, written \code{a.b} with no intervening whitespace between an expression and a field projection. This is parsed the as \code{a .b} but with higher precedence than ordinary juxtaposition, so that \code{f a.x a.y} is \code{f (a .x) (a .y)} rather than \code{f a .x a .y}.} \p{\defcase{Infix application} is two expressions with a symbolic identifier or keyword between them, like \code{a : Int}.} - \p{Juxtaposition binds tighter than infix application and left associates. Thus, \code{f x y} is \code{(f x) y} and \code{f x + y} is \code{(f x) + y}. The binding strength and associativity of infix application is determined by a custom precedence table.} + \p{Juxtaposition binds tighter than infix application, thus \code{f x + y} is \code{(f x) + y}. The binding strength and associativity of infix application is determined by a custom precedence table.} \p{The precedence table for Coln is as follows.} @@ -45,7 +47,9 @@ }{ \row{\cell{\code{:=}} \cell{10} \cell{non-associative}} \row{\cell{\code{:}} \cell{20} \cell{non-associative}} + % \row{\cell{\code{*:}} \cell{20} \cell{non-associative}} \row{\cell{\code{->}} \cell{30} \cell{right-associative}} + % \row{\cell{\code{->}} \cell{30} \cell{right-associative}} \row{\cell{\code{=>}} \cell{30} \cell{right-associative}} \row{\cell{\code{=}} \cell{40} \cell{non-associative}} \row{\cell{\code{+}} \cell{50} \cell{left-associative}} @@ -53,7 +57,7 @@ \row{\cell{\code{*}} \cell{60} \cell{left-associative}} } - \p{The \em{only} role of parentheses in f-notation is to clarify binding, so in particular parentheses are always idempotent. That is, \code{(e)} is always the same as \code{((e))} in every context.} + \p{The \em{only} role of parentheses in f-notation is to clarify binding, so in particular parentheses are always idempotent. That is, \code{(e)} is always the same as \code{((e))} in any context.} } \subtree[0012]{ @@ -63,7 +67,7 @@ \pre{\kw{def} x : Int := 5} \p{is a declaration, which could be parenthesized as} \pre{\kw{def} ((x : Int) := 5)} - \p{A declaration may be \em{modified} as well by modification tokens, as in} + \p{\mvrnote{These are unused currently?} A declaration may be \em{modified} by prefixing it with modification tokens, as in} \pre{\kw{pub} \kw{def} x : Int := 5} \p{These modifiers form part of the overall declaration.} diff --git a/manual/trees/0014.tree b/manual/trees/0014.tree index 94b665d6..6f169878 100644 --- a/manual/trees/0014.tree +++ b/manual/trees/0014.tree @@ -16,7 +16,7 @@ \row{\cell{\code{SKeyword}} \cell{Symbolic keyword, used for reserved infix keywords that nonetheless parse normally}} \row{\cell{\code{Decl}} \cell{Used to designate a top-level declaration}} \row{\cell{\code{Modifier}} \cell{Used to modify a top-level declaration}} -\row{\cell{\code{Block}} \cell{Used to designate a block}} +\row{\cell{\code{Block}} \cell{Used to designate the start of a block}} \row{\cell{\code{End}} \cell{Used to end a block}} } @@ -27,20 +27,29 @@ }{ \row{\cell{\code{sig}} \cell{\code{Block}}} \row{\cell{\code{struct}} \cell{\code{Block}}} +\row{\cell{\code{realm}} \cell{\code{Block}}} \row{\cell{\code{end}} \cell{\code{End}}} \row{\cell{\code{theory}} \cell{\code{Decl}}} \row{\cell{\code{def}} \cell{\code{Decl}}} +\row{\cell{\code{let}} \cell{\code{Decl}}} +% \row{\cell{\code{open}} \cell{\code{Decl}}} +% \row{\cell{\code{import}} \cell{\code{Decl}}} \row{\cell{\code{Set}} \cell{\code{AKeyword}}} \row{\cell{\code{Prop}} \cell{\code{AKeyword}}} \row{\cell{\code{Int}} \cell{\code{AKeyword}}} \row{\cell{\code{String}} \cell{\code{AKeyword}}} +% \row{\cell{\code{Inductive}} \cell{\code{AKeyword}}} +% \row{\cell{\code{init}} \cell{\code{AKeyword}}} \row{\cell{\code{:=}} \cell{\code{SKeyword}}} \row{\cell{\code{=}} \cell{\code{SKeyword}}} \row{\cell{\code{:}} \cell{\code{SKeyword}}} +% \row{\cell{\code{*:}} \cell{\code{SKeyword}}} \row{\cell{\code{->}} \cell{\code{SKeyword}}} +% \row{\cell{\code{*->}} \cell{\code{SKeyword}}} \row{\cell{\code{=>}} \cell{\code{SKeyword}}} +\row{\cell{\code{@}} \cell{\code{SKeyword}}} } -\p{Names with no segment found in the above list are classified as identifiers; it is invalid to have a multi-segment name that uses a reserved name segment.} +\p{Names with no segment found in the above list are classified as identifiers; it is invalid to have a multi-segment name that contains a reserved name segment.} -\p{We use boldface for block tokens and decl tokens in code snippets as a very rudimentary form of syntax highlighting.} +\p{We use boldface for \code{Block} tokens and \code{Decl} tokens in code snippets as a very rudimentary form of syntax highlighting.} diff --git a/manual/trees/0015.tree b/manual/trees/0015.tree index 54e9d0e0..04b8c531 100644 --- a/manual/trees/0015.tree +++ b/manual/trees/0015.tree @@ -3,6 +3,6 @@ \p{Putting \code{.} in front of a name turns it into a \defcase{field}, and putting \code{'} in front of a name turns it into a \defcase{tag}.} -\p{Fields are intended for use in accessing a record. For instance \code{a .b} gets the \code{b} field from the record; \code{a.b} is also valid and parses the same.} +\p{Fields are intended for accessing the fields of a record. For instance \code{a .b} gets the \code{b} field from the record.} \p{Tags are intended for use in creating elements of a sum type. For instance \code{'just 1} could be an element of the sum type \code{Maybe Int}. Currently Coln does not have either sum types or tags, however.} diff --git a/manual/trees/0019.tree b/manual/trees/0019.tree index 77353ec1..fed8b8a2 100644 --- a/manual/trees/0019.tree +++ b/manual/trees/0019.tree @@ -3,4 +3,4 @@ \p{Whitespace is generally ignored, though newlines create \code{\verb>|\n>} tokens.} -\p{Line comments starting with \code{#} are considered whitespace.} +\p{Lines starting with \code{#} are comments, and are considered whitespace.} diff --git a/manual/trees/001B.tree b/manual/trees/001B.tree index 30aa54d1..5a1a699e 100644 --- a/manual/trees/001B.tree +++ b/manual/trees/001B.tree @@ -1,49 +1,29 @@ -\title{The theory of sets} +\title{The type of sets} \import{prelude} -\p{\code{Set} is a theory, and models of \code{Set} are collections of things. This corresponds to a very simple kind of database by itself, but we can do many things from this foundation.} +\p{There is a type \code{Set}, whose elements are collections of things.} -\p{We refer to models of \code{Set} as, unsurprisingly, “sets.”} +% In particular we have \code{String : Set} and \code{Int : Set}. -\p{In TypeScript, models of \code{Set} store collections of \code{Value}s, where \code{Value} is defined in the following way} +\p{As a database schema, this produces a table of completely abstract row-ids, with no associated data.} \pre{% -\kw{const} RowId = { - from: DatabaseId, - index: number +\kw{theory} Widget := Set } -\kw{const} Value = - { tag: "row_id", value: RowId } | - { tag: "tuple", value: Record } | - { tag: "int", value: number } | - { tag: "string", value: string } -} - -\p{All elements in the collection should be of the same type (e.g. all row ids, all strings, etc.) but for simplicity all sets share the same untyped API involving \code{Value}s.} - -\p{A TypeScript value \code{m} that refers to a model of \code{Set} satisfies the following interface} - -\pre{% -\kw{interface} ReadonlySet { - has(x: Value): boolean; - values(): Iterator; -} -} - -\p{If \code{m} has read-write permissions, then it will also satisfy the interface} - -\pre{% -\kw{interface} ReadWriteSet \kw{extends} ReadonlySet { - add(): Value; -} -} - -\p{Intuitively, \code{add()} does not take parameters because it adds a \em{fresh} element to the set, an element not equal to any other previous element. This means that a set of integers can never be read-write because it is impossible to create a fresh integer. We will see later on that it is instead possible to store a \em{subset} of the set of all integers; this will look differently however.} - -\p{For a set with read-write permission, the following code should not throw an error.} - -\pre{% -\kw{const} a = m.add() -assert(m.has(a)) +\dbexample{ + \p{\strong{Table \code{Widget}}} + + \table{ + \row{\hcell{RowID}} + }{ + \row{\cell{\code{a}}} + \row{\cell{\code{b}}} + } + + \p{\strong{Constraints:} + \ul{ + \li{None.} + } + } } diff --git a/manual/trees/001C.tree b/manual/trees/001C.tree index 00b248ba..e4f83978 100644 --- a/manual/trees/001C.tree +++ b/manual/trees/001C.tree @@ -1,22 +1,62 @@ -\title{Record types as theories} +\title{Record types} \import{prelude} -\p{Records types are a way of composing multiple theories into one theory. A record type has multiple \em{fields}, each of which is declared to be a model of another theory. For instance:} +\p{Record types compose multiple types into a single type, whose elements consist of elements of each of the individual pieces. A record type declaration consists of a list of \em{fields}, each with its own type. A record is formed by a \code{\kw{sig} ... \kw{end}} block, with one field per line. For instance:} \pre{% -\kw{theory} SantaList := \kw{sig} - naughty : Set - nice : Set +\kw{theory} PersonDeets := \kw{sig} + name : String + age : Int \kw{end} } -\p{\code{SantaList} is a very simple theory, the models of which consist of a pair of a collection of naughty things and a collection of nice things.} +\p{An instance of \code{PersonDeets} stores \em{one person}'s name and age. The two fields become columns in a single table:} + +\dbexample{ + \p{\strong{Table \code{PersonDeets}}} + + \table{ + \row{\hcell{\code{name : String}} \hcell{\code{age : Int}}} + }{ + \row{\cell{\code{"Wonka"}} \cell{38}} + } + + \p{\strong{Constraints:}} + \ul{ + \li{\code{PersonDeets} has exactly one row.} + } +} -\p{More precisely, if we have a model \code{m} of \code{SantaList} in TypeScript, then \code{m.naughty} and \code{m.nice} are both models of \code{Set}. If \code{m} is readonly, then \code{m.naughty} and \code{m.nice} will satisfy \code{ReadonlySet}, and if \code{m} is read-write, then \code{m.naughty} and \code{m.nice} will satisfy \code{ReadWriteSet}. The following TypeScript code should run without errors if \code{m} is a read-write model of \code{SantaList}.} +\p{Fields can also be collections, by giving them the type \code{Set}:} \pre{% -\kw{const} alice = m.nice.add() -\kw{const} bob = m.naughty.add() -assert(m.nice.has(alice)) -assert(!m.nice.has(bob)) +\kw{theory} SantaList := \kw{sig} + Naughty : Set + Nice : Set +\kw{end} } + +\p{Elements of \code{SantaList} consist of a pair of a collection of naughty things and a collection of nice things.} + +\dbexample{ + \p{\strong{Table \code{SantaList.Naughty}}} + + \table{ + \row{\hcell{Row ID}} + }{ + \row{\cell{\code{b1}}} + } + + \p{\strong{Table \code{SantaList.Nice}}} + + \table{ + \row{\hcell{Row ID}} + }{ + \row{\cell{\code{g1}}} + \row{\cell{\code{g2}}} + } + + \p{\strong{Constraints:} None.} +} + +\p{Each element of a collection is represented by a row with its own opaque row-id.} diff --git a/manual/trees/001D.tree b/manual/trees/001D.tree index bf2d44df..f44be2fe 100644 --- a/manual/trees/001D.tree +++ b/manual/trees/001D.tree @@ -1,31 +1,60 @@ -\title{Sets as theories} +\title{Sets as fields} \import{prelude} -\p{A model \code{A : Set} may itself be used as a theory. A model of \code{A} is just an element of \code{A} (remember that a model of \code{Set} is a collection of things). For example, consider the following theory.} +\p{An element \code{A : Set} may be used directly as a type. Elements of \code{Set} are supposed to correspond to collections of things, so an element of \code{A} as a type is just an element of the collection \code{A} is supposed to be. For example, consider the following theory.} \pre{% \kw{theory} PopulatedSantaList := \kw{sig} - list : SantaList - john : list.nice - mary : list.naughty + Naughty : Set + Nice : Set + charlie : Nice + veruca : Naughty \kw{end} } -\p{A model \code{m} of \code{PopulatedSantaList} consists of a model \code{m.list} of \code{SantaList}, along with specific elements \code{m.john} in \code{m.list.nice} and \code{m.mary} in \code{m.list.naughty}.} - -\p{In TypeScript, an element of a set comes along with a getter, and if it is read-write, also a setter. So if \code{m} is a TypeScript variable accessing a model of \code{PopulatedSantaList}, then we should have:} - -\pre{assert(m.list.nice.has(m.john.get()))} - -\p{If \code{m} is \em{incomplete}, then \code{m.john.get()} might return \code{null}. This would be the case in a freshly-created model, as in} - -\pre{\kw{const} m = PopulatedSantaList.create()} - -\p{This can be remedied by using \code{.set()}, as in} - -\pre{% -\kw{const} john = m.list.nice.add() -m.john.set(john) +\p{An element \code{m} of \code{PopulatedSantaList} consists of two collections, \code{m.Naughty} and \code{m.Nice}, along with specific elements \code{m.charlie} in \code{m.Nice} and \code{m.veruca} in \code{m.Naughty}.} + +\dbexample{ + \p{\strong{Table \code{PopulatedSantaList.Naughty}}} + + \table{ + \row{\hcell{Row ID}} + }{ + \row{\cell{\code{b1}}} + } + + \p{\strong{Table \code{PopulatedSantaList.Nice}}} + + \table{ + \row{\hcell{Row ID}} + }{ + \row{\cell{\code{g1}}} + \row{\cell{\code{g2}}} + } + + \p{\strong{Table \code{PopulatedSantaList.charlie}}} + + \table{ + \row{\hcell{\code{root : Nice}}} + }{ + \row{\cell{\code{g1}}} + } + + \p{\strong{Table \code{PopulatedSantaList.veruca}}} + + \table{ + \row{\hcell{\code{root : Naughty}}} + }{ + \row{\cell{\code{b1}}} + } + + \p{\strong{Constraints:}} + \ul{ + \li{The \code{charlie} and \code{veruca} tables each have exactly one row.} + \li{The value in \code{charlie.root} is a row ID in \code{Nice}.} + \li{The value in \code{veruca.root} is a row ID in \code{Naughty}.} + } + \p{Here, \code{charlie} selects \code{g1} from \code{Nice}, and \code{veruca} selects \code{b1} from \code{Naughty}.} } -\p{Note that \code{m.john.set(x)} would throw an exception if \code{x} were not in \code{m.list.nice}.} +\p{In particular, records in Coln may be \em{dependent}: the types of later fields may refer to earlier fields, as is the case for \code{charlie} and \code{veruca}.} diff --git a/manual/trees/001E.tree b/manual/trees/001E.tree index 0ebf2602..e6b0ee64 100644 --- a/manual/trees/001E.tree +++ b/manual/trees/001E.tree @@ -1,29 +1,32 @@ -\title{Function types as theories} +\title{Function types} \import{prelude} -\p{Function types are theories, as long as the domain is a set and the codomain is a theory.} - -\p{Function types can be used in many ways. Here are some examples.} +\p{An element of a function type \code{A -> B} assigns for each element of \code{A}, an element of \code{B}.} \pre{% -\kw{theory} StateMachine := \kw{sig} - state : Set - next : state -> state +\kw{theory} SimpleMachine := \kw{sig} + input : Set + output : Set + next : input -> output \kw{end} } -\p{If we have \code{m : StateMachine}, then \code{m.next} is a function that sends elements of \code{m.state} to other elements of \code{m.state}. The type \code{state -> state} satisfies the criterion for being a theory because its domain is a set and its codomain is a theory (following [[001D]]). Concretely, in TypeScript, we could use this like} +\p{If we have \code{m : StateMachine}, then \code{m.next} is a function that sends elements of \code{m.input} to elements of \code{m.output}.} + +% Instance Example + +\p{These can certainly use the same collection on both sides.} \pre{% -\kw{const} m = StateMachine.create() -\kw{const} [x,y] = [m.state.add(), m.state.add()] -m.next(x).set(y) -m.next(y).set(y) +\kw{theory} StateMachine := \kw{sig} + state : Set + next : state -> state +\kw{end} } -\p{Note that at the point where we have added \code{x} and \code{y} but not yet set the values of \code{next} for them, \code{m} is not a valid instance for \code{StateMachine}. In fact, in general it is inevitable that in the process of building a model one may pass through an invalid state. Thus, validity is only checked at certain points; we discuss validity more in a later section.\todo} +% Instance Example -\p{But that is not all functions can do. As the codomain of a function can be a theory, we could also do the following.} +\p{But that is not all functions can do. Though there are some restrictions (see [[Levels]]), the domain and codomain of a function can be a general type, so we can do the following:} \pre{% \kw{theory} SantaLists := \kw{sig} @@ -32,11 +35,6 @@ m.next(y).set(y) \kw{end} } -\p{From TypeScript, we could use a model \code{m} of \code{SantaLists} in the following way.} - -\pre{% -\kw{const} y2025 = m.year.add() -\kw{const} bob = m.list(y2025).nice.add() -} +% Instance Example \p{Now, there are some ontological problems with this database schema. We cannot ask whether a person is nice one year and naughty the other year, because the nice and naughty sets for each year are disjoint. What we would really like is there to be \em{one} set of people, and then in different years they might be nice or naughty. This can be accomplished with [relations](001G).} diff --git a/manual/trees/001G.tree b/manual/trees/001G.tree index 4731f198..a2550166 100644 --- a/manual/trees/001G.tree +++ b/manual/trees/001G.tree @@ -1,24 +1,14 @@ \title{Propositions and relations} \import{prelude} -\p{There is a theory \code{Prop} which is even more boring than \code{Set}; it is the theory of a set with at most one element. One could think of it also as a truth value: inhabited means true and empty means false. From TypeScript, we have the interface} +\p{There is an additional type-of-types \code{Prop} whose elements are simpler than those of \code{Set}; its elements are collections that themselves have \em{at most one} element. One can think of \code{Prop} as the type of [truth values](TODO): an element which is an inhabited collection means \code{true}, and an element which is an empty collection means \code{false}} -\pre{% -\kw{interface} ReadonlyProp { - isTrue(): boolean; -} - -\kw{interface} ReadWriteProp \kw{extends} ReadonlyProp { - makeTrue(): void; -} -} - -\p{While on its own \code{Prop} is boring, we can combine it with function types to make it more interesting. For instance, we can now rewrite \code{SantaLists} so that the same person may appear on lists in different years.} +\p{While on its own \code{Prop} is boring, we can combine it with function types to make it more interesting. For instance, we can rewrite \code{SantaLists} so that the same person may appear on lists in different years.} \pre{% \kw{theory} SantaListOver (person : Set) := \kw{sig} - naughty : person -> Prop - nice : person -> Prop + is-naughty : person -> Prop + is-nice : person -> Prop \kw{end} \kw{theory} SantaLists := \kw{sig} @@ -28,19 +18,9 @@ \kw{end} } -\p{Here we have also introduced an additional feature: a theory can have \em{parameters}, which are models of other theories. In this case, \code{SantaList} now takes in a parameter \code{person} which is a model of \code{Set}. We instantiate this parameter with \code{children} in \code{SantaLists}.} - -\p{In TypeScript, we could interact with a read-write model \code{m} of this new \code{SantaLists} in the following way.} - -\pre{% -\kw{const} john = m.children.add() -\kw{const} y2025 = m.year.add() -\kw{const} y2026 = m.year.add() -m.list(y2025).nice(john).makeTrue() -m.list(y2026).naughty(john).makeTrue() -} +% Example instance -\p{We call a function whose codomain is \code{Prop} a \defcase{relation}. \code{m.list(y2025).nice} is a \em{unary} relation because it takes in one argument. Here is another example, this time of a \em{binary} relation.} +\p{We call a function whose codomain is \code{Prop} a \defcase{relation}. Here, \code{is-naughty} and \code{is-nice} are \em{unary} relations, because each takes in one argument. Here is another example, this time of a \em{binary} relation.} \pre{% \kw{theory} Drama := \kw{sig} @@ -49,16 +29,9 @@ m.list(y2026).naughty(john).makeTrue() \kw{end} } -\p{From TypeScript, using a model of \code{Drama} would look like:} - -\pre{% -\kw{const} [john, mary] = [m.person.add(), m.person.add()] -m.jealous_of(john)(mary).makeTrue() -} - -\p{Note that because names in fnotation can contain characters like \code{-} that are not allowed in TypeScript, we have to \em{mangle} the Coln name to create the TypeScript API. As \code{person_of} is also a valid name in Coln, a theory could have both \code{person-of} and \code{person_of} fields. In this case, emitting the TypeScript FFI would emit an error. The suggested fix is to not have fields that differ only by choice of hyphen/underscore, because that is bad and confusing in any case.} - -\p{Just like a set is a theory, a proposition is also a theory; a model of the proposition can be thought of as a witness that the proposition is true. We can use this to put \em{laws} in our database. For instance, we can make jealousy be transitive.} +\p{An element of a proposition can be thought of as a witness that the +proposition is true. We can use this to put \em{laws} in our database. +For instance, we can enforce a law that makes jealousy be transitive.} \pre{% \kw{theory} ExtraDrama := \kw{sig} @@ -69,13 +42,4 @@ m.jealous_of(john)(mary).makeTrue() \kw{end} } -\p{We saw [earlier](001E) one way in which a model of a theory might be incomplete; a function might not yet be defined for given values of its inputs. Here we have a similar situation. For instance, we might have written:} - -\pre{% -\kw{const} [john, mary, sue] = - [m.person.add(), m.person.add(), m.person.add()] -m.jealous_of(john)(mary).makeTrue() -m.jealous_of(mary)(sue).makeTrue() -} - -\p{When checking validity of \code{m} after executing this code, Coln will report that \code{jealous-of/is-transitive john mary sue _ _ : jealous-of mary sue} is not satisfied (though, Coln does not know what names we have given to these variables in TypeScript, so it would actually print out the row identifiers instead of the names).\todo Unlike with \code{next} in the [section on functions](001E), to fix this we don't need to touch \code{jealous-of/is-transitive}. Instead, we can just run \code{m.jealous_of(john)(sue).makeTrue()}, and the model will be valid again. This is because if the codomain of a function is a proposition, there is ultimately only one possible way for that function to exist, and thus the function need not be explicitly defined. We discuss how this works in a later section.\todo} +% Example instance diff --git a/manual/trees/001H.tree b/manual/trees/001H.tree index e436957c..acfbddc5 100644 --- a/manual/trees/001H.tree +++ b/manual/trees/001H.tree @@ -1,43 +1,3 @@ \title{Record types as sets} \import{prelude} -\p{Just like we have record types as the theory-level, we also have record types at the set-level. We can use this to define a set in the context of a model of a given theory; this is how to “natively query” an instance of a Coln theory.\todo} - -\pre{% -\kw{def} jealousy-triangle (m : Drama) : Set := \kw{tuple} - a : m.person - b : m.person - c : m.person - a-b : m.jealous-of a b - b-c : m.jealous-of b c - c-a : m.jealous-of c a -\kw{end} -} - -\p{In TypeScript, \code{jealousy-triangle} is compiled to a function that takes in a model of \code{Drama} and returns a \code{ReadonlySet}.\todo The elements \code{v} of this \code{ReadonlySet} are \code{Value}s with the \code{"tuple"} tag, which have fields \code{a},\code{b},\code{c} that are elements of \code{m.person}, such that \code{m.jealous-of(v.value.a)(v.value.b).isTrue()}, and so on. The value \code{v} will also have \code{v.value.a_b}, but it will just be \code{null}, thought of as the unique element of the singleton set.} - -\p{Iterating through the elements of \code{jealousy_triangle(m)} will be faster than the naive approach of a triply-nested for-loop over \code{m.person} and then filtering out using \code{m.jealous-of}, because Coln can \em{plan} the query and take advantage of fast join algorithms on the \code{m.jealous-of} table.\todo} - -\p{This query can be written more compactly in the following way.\todo} - -\pre{% -\kw{def} jealousy-triangle (m : Drama) : Set := \kw{tuple} - a b c : m.person - m.jealous-of a b - m.jealous-of b c - m.jealous-of c a -\kw{end} -} - -\p{We can omit the field names for propositions because we never need to refer to the witnesses of the propositions, we just need the propositions to be true.} - -\p{As a variation on the same theme, we could look for length-3 cycles in a state machine with} - -\pre{% -\kw{def} next-triangle (m : StateMachine) : Set := \kw{tuple} - a b c : m.state - m.next a = b - m.next b = c - m.next c = a -\kw{end} -} diff --git a/manual/trees/001I.tree b/manual/trees/001I.tree index 69bb8824..7880bc9e 100644 --- a/manual/trees/001I.tree +++ b/manual/trees/001I.tree @@ -1,12 +1,12 @@ -\title{Equality types as theories} +\title{Equality types} \import{prelude} -\p{Another way of creating interesting propositions is with \defcase{equality}. Given two elements \code{a0} and \code{a1} of a set \code{A}, there is a proposition \code{a0 = a1} which is true if and only if \code{a0} is equal to \code{a1}.} +\p{Besides using a \code{Prop} asserted as a field, the other method of forming a proposition is \defcase{equality}. Given two elements \code{a0} and \code{a1} of \em{any} set \code{A : Set}, there is a proposition \code{(a0 = a1) : Prop} which is true (i.e. is inhabited) exactly when \code{a0} is equal to \code{a1}.} -\p{We can use this to write down laws in our theories that involve equality. For instance, we can write down the theory of a two-way mapping (mathematically known as a \em{bijection}) in the following way} +\p{We can use this to write down laws in our theories that involve equality. For instance, we can write down the theory of a bijection in the following way:} \pre{% -\kw{theory} TwoWayMapping (X : Set) (Y : Set) := \kw{sig} +\kw{theory} Bijection (X : Set) (Y : Set) := \kw{sig} fwd : X -> Y bwd : Y -> X bwd-fwd : (x : X) -> bwd (fwd x) = x @@ -14,7 +14,9 @@ \kw{end} } -\p{Another example of equality usage is when we assert that a relation is a partial function, by saying that if \code{x} is related to both \code{y0} and \code{y1} then \code{y0} must be equal to \code{y1}.} +% Example instance, for Bijection instantiated + +\p{Another example of equality usage is when we assert that a relation is a partial function, by saying that if \code{x} is related to both \code{y0} and \code{y1}, then \code{y0} must be equal to \code{y1}.} \pre{% \kw{theory} IsPartialFunction (X : Set) (Y : Set) (R : X -> Y -> Prop) := diff --git a/manual/trees/001J.tree b/manual/trees/001J.tree index 739766f1..8ff35bbc 100644 --- a/manual/trees/001J.tree +++ b/manual/trees/001J.tree @@ -10,4 +10,41 @@ \p{\code{\kw{def}} is in fact a much more general construct; any theory can replace \code{Set} on the right, and we can take in multiple arguments.} -\p{In general, this allows one to create a \em{view} of a model one theory, in the form of a model of another theory.} +\p{In general, this allows one to create a \em{view} of a model of one theory, in the form of a model of another theory.} + +\p{Just like we have record types as the theory-level, we also have record types at the set-level. We can use this to define a set in the context of a model of a given theory; this is how to “natively query” an instance of a Coln theory.\todo} + +\pre{% +\kw{def} jealousy-triangle (m : Drama) : Set := \kw{sig} + a : m.person + b : m.person + c : m.person + a-b : m.jealous-of a b + b-c : m.jealous-of b c + c-a : m.jealous-of c a +\kw{end} +} + +\p{This query can be written more compactly in the following way.\todo} + +\pre{% +\kw{def} jealousy-triangle (m : Drama) : Set := \kw{sig} + a b c : m.person + m.jealous-of a b + m.jealous-of b c + m.jealous-of c a +\kw{end} +} + +\p{We can omit the field names for propositions because we never need to refer to the witnesses of the propositions, we just need the propositions to be true.} + +\p{As a variation on the same theme, we could look for length-3 cycles in a state machine with} + +\pre{% +\kw{def} next-triangle (m : StateMachine) : Set := \kw{sig} + a b c : m.state + m.next a = b + m.next b = c + m.next c = a +\kw{end} +} diff --git a/manual/trees/001K.tree b/manual/trees/001K.tree index d2c377cc..8491ecf0 100644 --- a/manual/trees/001K.tree +++ b/manual/trees/001K.tree @@ -16,9 +16,9 @@ \pre{% \kw{def} list-for (m : SantaLists) (y : m.year) : SantaList := \kw{struct} - naughty := \kw{tuple} { child : m.person; m.list y .naughty child } - nice := \kw{tuple} { child : m.person; m.list y .nice child } + naughty := \kw{sig} { child : m.person; m.list y .naughty child } + nice := \kw{sig} { child : m.person; m.list y .nice child } \kw{end} } -\p{Intuitively, this assigns \code{naughty} to the set of children naughty in that year, and similarly with \code{nice}. The \code{\kw{tuple}} syntax is just as in [[001H]], using the curly-brace inline syntax. And \code{m.list y .naughty child} is just a sequence of function applications and field projection. Walking through the types, we have \code{m.list : m.person -> SantaListOver m.person}, so \code{m .list y : SantaListOver m.person} and then \code{m.list y .naughty : m.person -> Prop} and finally \code{m.list y .naughty child : Prop}.} +\p{Intuitively, this assigns \code{naughty} to the set of children naughty in that year, and similarly with \code{nice}. The \code{\kw{sig}} syntax is just as in [[001H]], using the curly-brace inline syntax. And \code{m.list y .naughty child} is just a sequence of function applications and field projection. Walking through the types, we have \code{m.list : m.person -> SantaListOver m.person}, so \code{m .list y : SantaListOver m.person} and then \code{m.list y .naughty : m.person -> Prop} and finally \code{m.list y .naughty child : Prop}.} diff --git a/manual/trees/001N.tree b/manual/trees/001N.tree index dcda8137..32237081 100644 --- a/manual/trees/001N.tree +++ b/manual/trees/001N.tree @@ -1,7 +1,7 @@ \title{Inductive types} \import{prelude} -\p{An interesting fact about [[000L]] the reader may have noticed is that the only model of \code{Set} that one can write down in the empty context is the singleton type \code{\kw{tuple} {}}.} +\p{\mvrnote{The syntax in this section is now out of date} An interesting fact about [[000L]] the reader may have noticed is that the only model of \code{Set} that one can write down in the empty context is the singleton type \code{\kw{sig} {}}.} \p{This is remedied by inductive types. In Coln, inductive types are produced by \em{initial models}. An initial model for a theory \code{T} is a model of \code{T} that makes zero decisions: the only elements in the sets in the model are the ones forced to exist by the laws of the theory.} diff --git a/manual/trees/001T.tree b/manual/trees/001T.tree index 33d63ce5..fa57ca41 100644 --- a/manual/trees/001T.tree +++ b/manual/trees/001T.tree @@ -20,7 +20,7 @@ \transclude{001X} -\p{In this way, although when writing down \code{BagOfGraphs} it appears as if we would store a separate graph database for each graph id, in fact all of the graphs are stored in the same pair of tables. In particular, allocating a new graph id does not imply allocating a whole new graph structure.} +\p{In this way, although when writing down \code{BagOfGraphs} it appears as if we would store a separate graph database for each \code{graph-id}, in fact all of the graphs are stored in the same pair of tables. In particular, allocating a new \code{graph-id} does not imply allocating a whole new set of tables for the new graph.} \p{There is a fairly straightforward algorithm to take a general theory to a theory in #{\Sigma\Pi}-normal form, producing the \code{from-normal} and \code{to-normal} migrations simultaneously, but describing it here would involve a conceptual framework around the [elaborator](000O) which would take a while to get off the ground. Thus, we ask the reader to take as given that we have access to such an algorithm, and we continue on assuming that we are working with theories in #{\Sigma\Pi}-normal form.} diff --git a/manual/trees/001Z.tree b/manual/trees/001Z.tree index 948b2aa7..d58f6b84 100644 --- a/manual/trees/001Z.tree +++ b/manual/trees/001Z.tree @@ -4,7 +4,7 @@ \p{Recall from [[001H]] the query \code{jealousy-triangle} defined by} \pre{% -\kw{def} jealousy-triangle (m : Drama) : Set := \kw{tuple} +\kw{def} jealousy-triangle (m : Drama) : Set := \kw{sig} a b c : m.person m.jealous-of a b m.jealous-of b c @@ -12,4 +12,4 @@ \kw{end} } -\p{} +\p{\mvrnote{TODO unfinished example}} diff --git a/manual/trees/0021.tree b/manual/trees/0021.tree index 2eeb5845..27933177 100644 --- a/manual/trees/0021.tree +++ b/manual/trees/0021.tree @@ -7,5 +7,3 @@ \transclude{0024} \transclude{0026} \transclude{0025} - -\transclude{0027} diff --git a/manual/trees/0026.tree b/manual/trees/0026.tree index 95d3a8db..453cb492 100644 --- a/manual/trees/0026.tree +++ b/manual/trees/0026.tree @@ -2,10 +2,10 @@ \taxon{Definition} \import{prelude} -\p{A \defcase{primary key constraint} is specified by a subset #{K \subseteq \{0,\ldots,k-1\}} of column indices. For each #{K}-indexed tuple of values, a table satisfying the primary key constraint may have at most one row with columns assigned as in that #{K}-tuple.} +\p{A table optionally has a \defcase{primary key constraint}. A primary key constraint is specified by a subset #{K \subseteq \{0,\ldots,k-1\}} of column indices. For each #{K}-indexed tuple of values, a table satisfying the primary key constraint may have at most one row with columns assigned as in that #{K}-tuple.} \p{This can be used in a variety of ways. If #{K = \{0,\ldots,k-1\}}, then the table is a proper \em{relation}. If #{K = \{0,\ldots,\ell-1\}}, then #{K} is a partial function from the first #{\ell} column values to the last #{k - \ell} column values.} -\p{A table with no primary key constraint can be thought of as a bag.} +\p{A table with no primary key constraint can be thought of as a bag. \mvrnote{reference bag}} -\p{As a degenerate case, a table with no columns and a primary key constraint of #{\{\}} has either zero or one row IDs.} +\p{As a degenerate case, a table with a primary key constraint of #{\{\}} has either zero or one row IDs.} diff --git a/manual/trees/0027.tree b/manual/trees/0027.tree deleted file mode 100644 index b2f2f01e..00000000 --- a/manual/trees/0027.tree +++ /dev/null @@ -1 +0,0 @@ -\date{2026-05-23T09:45:40Z} diff --git a/manual/trees/0028.tree b/manual/trees/0028.tree index 9b648bc3..2ec5dd4f 100644 --- a/manual/trees/0028.tree +++ b/manual/trees/0028.tree @@ -12,12 +12,12 @@ \p{The concept of a universal property is formalized in different ways, often using category theory, but we need not bother with formalization at this stage.} -\p{The reader may have heard of “[the Curry-Howard correspondence](curry-howard)”, often informally referred to “propositions as types”. The Curry-Howard correspondence shows how various type formers and logical connectives correspond. With all due respect to Curry-Howard the name “correspondence” is somewhat of a misnomer because it assumes a false equivalence between the two things that are claimed to be in correspondence. In particular, propositional logic is a \em{mathematical domain} in which type theory may be applied to form a convenient syntax; it is by no means the only domain.} +\p{The reader may have heard of “[the Curry-Howard correspondence](curry-howard)”, often informally referred to “propositions as types”. The Curry-Howard correspondence shows how various type formers and logical connectives correspond. With all due respect to Curry-Howard the name “correspondence” is somewhat of a misnomer because it assumes a false equivalence between the two things that are claimed to be in correspondence. In particular, propositional logic is a \em{mathematical domain} in which type theory may be applied to produce a convenient syntax; it is by no means the only domain.} -\p{The reason type theory may be usefully applied to propositional logic because all of the connectives of propositional logic (and, or, not, forall, exists, etc.) satisfy universal properties; this is the same as the reason why type theory may be applied to any other area.} +\p{The reason type theory may be usefully applied to propositional logic is because all the connectives of propositional logic (and, or, not, forall, exists, etc.) satisfy universal properties; this is the same as the reason why type theory may be applied to any other area.} -\p{The way that type theory may be applied to a particular area is via the development of \em{a particular} type theory. Confusion between type theory as a subject and the concept of \em{a type theory} as a mathematical object is an unfortunate side effect of the nomenclature, because “ breaks with the convention that in group theory, we study groups, in field theory we study fields, or in category theory we study categories.} +\p{The way that type theory may be applied to a particular area is via the development of \em{a particular} type theory. Confusion between type theory as a subject and the concept of \em{a type theory} as a mathematical object is an unfortunate side effect of the nomenclature, because the use of “type theory” to describe the field breaks with the convention that in group theory, we study groups, in field theory we study fields, or in category theory we study categories. However, in type theory, we study type theories.} \p{A particular type theory is merely a syntactic formalization of some collection of universal properties, consisting of a collection of \em{rules} by which we judge that a certain piece of syntax is \em{well-typed}. The beauty of universal properties is that each universal property is quite self-contained, so a type theory may be designed by systematically observing which universal properties the objects of interest support, and then adding the standard type-theoretic rules for those universal properties to one's type theory.} -\p{And this is the method that we have followed in order to design the type theory for Coln: observe the universal properties that our domain of interest (relational databases) satisfy, and add rules corresponding to these universal properties. Fortunately, the result of this systematic development seems to produce a language which expresses many of the important database operations.} +\p{And this is the method that we have followed in order to design the type theory for Coln: we observe the universal properties that our domain of interest (relational databases) satisfy, and add rules corresponding to these universal properties. Fortunately, the result of this systematic development seems to produce a language which expresses many of the important database operations.} diff --git a/manual/trees/0029.tree b/manual/trees/0029.tree index 83382c95..c7781b3e 100644 --- a/manual/trees/0029.tree +++ b/manual/trees/0029.tree @@ -13,4 +13,4 @@ \p{In group theory, in order to produce a homomorphism from #{G} to the product group #{H_0 \times H_1}, it suffices to produce a homomorphism from #{G} to #{H_0} and from #{G} to #{H_1}, and vice-versa.} -\p{This list could consider ad nauseum, but the reader should get the point by now; there's a pattern going on.} +\p{This list could continue ad nauseum, but the reader should get the point by now; there's a pattern going on.} diff --git a/manual/trees/002A.tree b/manual/trees/002A.tree index ed3c99ba..36bc5e89 100644 --- a/manual/trees/002A.tree +++ b/manual/trees/002A.tree @@ -3,24 +3,14 @@ \p{(This is meant for [[000C]])} -\p{The ultimate intended semantics for Coln is in arithmetic theories, which are the analogue of geometric theories for [arithmetic universes](arithmetic-universes). However, geometric theories and topoi are both better-studied than arithmetic universes and are additionally closely related, so we give an exposition of the basic type theory in terms of geometric theories. Note that by topos we mean Grothendieck topos, not elementary topos, so in particular all topoi have natural numbers objects.} +\p{The ultimate intended semantics for Coln is in arithmetic theories, which are the analogue of geometric theories for [arithmetic universes](arithmetic-universes). However, geometric theories and topoi are both better-studied than arithmetic universes and are in any case closely related, so we give an exposition of the basic type theory in terms of geometric theories. Note that by “topos” we mean Grothendieck topos, not elementary topos, so in particular all topoi have natural numbers objects.} -\p{Following the principles of this manual, this is \em{not} a mathematical paper; there will be a more formal account of this type theory, but that is in progress. Rather, this is a conceptual account that makes reference to mathematics.} +\p{Following the principles of this manual, this is \em{not} a mathematical paper; in future there will be a more formal account of this type theory, but that remains in progress. Rather, this is a conceptual account that makes reference to mathematics.} -\p{In [The Elephant](johnstone-2002-sketches), Johnstone makes the following definitions for “theory”; we call this an \em{elephant theory} in order to distinguish it from other notions of theory we might consider.} +\transclude{002M} -\transclude{002C} +\transclude{002N} -\transclude{002E} - -\transclude{002F} - -\transclude{002D} - -\transclude{002G} - -\transclude{002I} - -\p{The remainder of this section is simply an investigation of what type formers are supported in #{\ms{ElTh}}.} +\transclude{002S} \transclude{002J} diff --git a/manual/trees/002C.tree b/manual/trees/002C.tree index 49eeed67..8c26bbd1 100644 --- a/manual/trees/002C.tree +++ b/manual/trees/002C.tree @@ -2,10 +2,10 @@ \taxon{Definition} \import{prelude} -\p{For #{\mc{S}} a topos, an \defcase{elephant theory} over #{\mc{S}} is a (pseudo-)functor #{T \colon (\ms{BTop}/\mc{S})\op \to \ms{Cat},} where #{(\ms{BTop}/\mc{S})\op} is the 2-category of bounded geometric morphisms into #{\mc{S}} and #{\ms{Cat}} is the 2-category of large categories.} +\p{For #{\mc{S}} a topos, an \defcase{elephant theory} over #{\mc{S}} is a (pseudo-)functor #{T \colon (\ms{BTop}/\mc{S})\op \to \ms{Cat},} where #{\ms{BTop}/\mc{S}} is the 2-category of bounded geometric morphisms into #{\mc{S}} and #{\ms{Cat}} is the 2-category of large categories. \mvrnote{Should this be #{\ms{CAT}}?}} \p{A morphism of elephant theories is simply an indexed functor.} -\p{We say that #{T} is \defcase{classified} by #{\ms{S}[T] \colon \ms{BTop}/\mc{S}} if #{T} is contravariantly represented by #{\mc{S}[T]}, that is #{T(\mc{E}) \cong \ms{BTop}/\mc{S}(\mc{E}, \mc{S}[T])}. We also call #{\ms{S}[T]} the \defcase{classifying topos} for #{T}.} +\p{We say that #{T} is \defcase{classified} by a bounded topos #{\ms{S}[T] \colon \ms{BTop}/\mc{S}} if #{T} is contravariantly represented by #{\mc{S}[T]}, that is, #{T(\mc{E}) \cong \ms{BTop}/\mc{S}(\mc{E}, \mc{S}[T])}. We also call #{\ms{S}[T]} the \defcase{classifying topos} for #{T}.} \p{(See [Elephant](johnstone-2002-sketches) Definition B4.2.1)} diff --git a/manual/trees/002D.tree b/manual/trees/002D.tree index 573fc285..40798388 100644 --- a/manual/trees/002D.tree +++ b/manual/trees/002D.tree @@ -2,14 +2,6 @@ \taxon{Definition} \import{prelude} -\p{\defcase{Geometric theories} may be consicely defined as the elephant theories built up via a sequence of [product-inserter-equifier limits](pie-limit) starting from the object classifier.} - -\p{We expand this to give more intuition.} - -\p{If #{T} is a theory, a \defcase{simple functional extension} of #{T} is another theory #{T'} given as the \em{inserter} of two geometric constructs #{F,G \colon T \to \bb{O}}. Intuitively, #{T'} is the theory given by freely adding a new morphism between the “objects” #{F} and #{G}.} - -\p{If #{T} is a theory, a \defcase{simple equational extension} of #{T} is another theory #{T'} given as the \em{equifier} of two indexed natural transformations #{\alpha, \beta \colon F \Rightarrow G}, where #{F} and #{G} are geometric constructs. Intuitively, #{T'} is the theory given by adding a new equality between morphisms of “objects”.} - -\p{A \defcase{geometric theory} is a theory built up by a finite sequence #{T_0,\ldots,T_n} of simple functional extensions and simple equational extensions starting from #{T_0 = \bb{O}^m} for some finite #{m}.} +\p{A \defcase{geometric theory} is an elephant theory built up by a finite sequence #{T_0,\ldots,T_n} of [simple functional extensions](002K) and [simple equational extensions](002L) starting from #{T_0 = \bb{O}^m} for some finite #{m}.} \p{(See [Elephant](johnstone-2002-sketches) Definition 4.2.7, note that Johnstone gives a slightly different definition, using \em{simple geometric quotients} in place of simple equational extensions, which use inverters instead of equifiers. The name “simple equational extension” is not known to us to be previously used, but it follows the schema of “simple functional extension.”)} diff --git a/manual/trees/002F.tree b/manual/trees/002F.tree index f09a9b0b..cbb5adf9 100644 --- a/manual/trees/002F.tree +++ b/manual/trees/002F.tree @@ -4,6 +4,6 @@ \p{If #{T} is a geometric theory, then a \defcase{geometric construct} is a #{\ms{BTop}/\mc{S}}-indexed functor #{F \colon T \to \bb{O}}.} -\p{The idea is that #{F}, given a model #{M} of #{T} in an #{\mc{S}}-topos #{\mc{E}}, produces an object of #{\mc{E}}.} +\p{The idea is that #{F}, when given a model #{M} of #{T} in an #{\mc{S}}-topos #{\mc{E}}, produces an object of #{\mc{E}}.} \p{(See [Elephant](johnstone-2002-sketches) Definition B4.2.5)} diff --git a/manual/trees/002H.tree b/manual/trees/002H.tree index d19b5b8d..48f3b157 100644 --- a/manual/trees/002H.tree +++ b/manual/trees/002H.tree @@ -1,7 +1,7 @@ \title{What and why is Coln?} \import{prelude} -\p{Coln is a \em{tool} for \em{logical reasoning}.} +\p{Coln is a dependent type theory that compiles to database schemas and queries, together with a custom database based on [[automerge]] that consumes these definitions. We see Coln as a \em{tool} for \em{logical reasoning}:} \ul{ \li{\defcase{Tool} means that Coln performs routines that answers questions.} @@ -11,7 +11,7 @@ \p{Coln is similar to both existing proof assistants and existing databases.} -\p{One way of looking at Coln is that it is the result of cutting out everything from a dependent type theory that can't fit in a database, and then seeing if database technology (query planning, efficient data structures) can speed up the process of proof search for the problems which are still expressible.} +\p{One way of looking at Coln is that it is the result of cutting out everything from a dependent type theory that can't fit in a database, and then seeing whether database technology (query planning, efficient data structures) can speed up the process of proof search for the problems which are still expressible.} \p{Another way of looking at Coln is that it is a dependently typed approach to databases, derived by first finding a denotational semantics for database languages and then using standard techniques to distill an internal language for that denotational semantics.} @@ -28,3 +28,7 @@ \p{However, the mathematics involved in a proof in a non-well-structured domain does not have this property, and if we want a systematic approach to organizing the lemmas then we should use a database that we can query in flexible ways, rather than relying on a naming convention.} \p{But there are many roads to and from Coln; the core ideas are very elementary in a certain sense and we expect to be surprised by where Coln ends up being applicable or not applicable.} + +\transclude{000B} + +\transclude{000I} diff --git a/manual/trees/002I.tree b/manual/trees/002I.tree index 52503dc9..5cda7e57 100644 --- a/manual/trees/002I.tree +++ b/manual/trees/002I.tree @@ -6,10 +6,10 @@ \p{Intuitively, #{\ms{Ty}(\Gamma)} is “elephant theories relative to #{\Gamma}.” This is because #{\groth \Gamma} is the category of topoi equipped with a model of #{\Gamma}; if #{\Gamma} were a geometric theory then #{\groth \Gamma} would be equivalent to #{\ms{BTop}/\mc{S}[\Gamma]}.} -\p{Then define #{\ms{Tm} \colon (\groth \ms{Ty})\op \to \ms{Set}} by letting #{\ms{Tm}(\Gamma, A)} be the set of \em{sections} of #{A}. A section #{a} is a natural assignment of #{a(\mc{E}, M) \colon A(\mc{E}, M)} for #{(\mc{E},M) \in \groth \Gamma}.} +\p{Then define #{\ms{Tm} \colon (\groth \ms{Ty})\op \to \ms{SET}} by letting #{\ms{Tm}(\Gamma, A)} be the set of \em{sections} of #{A}. A section #{a} is a natural assignment of #{a(\mc{E}, M) \colon A(\mc{E}, M)} for #{(\mc{E},M) \in \groth \Gamma}.} \p{Context extension is given in the following way. Suppose that #{\Gamma \colon (\ms{BTop}/\mc{S})\op \to \ms{Cat}} is a context and #{A \colon \ms{Ty}(\Gamma)}. Then #{\Gamma \ext A \colon (\ms{BTop}/\mc{S})\op \to \ms{Cat}} is defined by #{(\Gamma \ext A)(\mc{E}) = (M \colon \Gamma(\mc{E})) \times A(\mc{E},M)}.} -\p{Then finally we have weakening and the variable rule given by the first and second projections out of #{\Gamma \ext A}.} +\p{Weakening and the variable rule are by the first and second projections out of #{\Gamma \ext A}.} \p{Note that even though topoi and elephant theories are non-trivially 2-categorical, #{(\ms{ElTh},\ms{Ty},\ms{Tm})} forms nevertheless a strict (albeit quite large) category with families.} diff --git a/manual/trees/002J.tree b/manual/trees/002J.tree index 9eb59ccb..9197927d 100644 --- a/manual/trees/002J.tree +++ b/manual/trees/002J.tree @@ -1 +1,12 @@ -\date{2026-05-27T09:54:56Z} +\import{prelude} +\title{Type formers} + +\p{One of the nice things about categorical semantics is that once we have fixed the basic structure (the category with families), the type theory essentially writes itself, in the sense that we may just look through the various standard type formers and ask whether or not the semantics supports the constructions relevant universal property or not.} + +\transclude{002V} + +\transclude{002X} + +\transclude{002Y} + +\transclude{002Z} diff --git a/manual/trees/002K.tree b/manual/trees/002K.tree index f54be495..9b0dcab2 100644 --- a/manual/trees/002K.tree +++ b/manual/trees/002K.tree @@ -1 +1,5 @@ -\title{Developer documentation} +\title{Simple functional extension} +\taxon{Definition} +\import{prelude} + +\p{If #{T} is a theory, a \defcase{simple functional extension} of #{T} is another theory #{T'} given as the \em{inserter} of two geometric constructs #{F,G \colon T \to \bb{O}}. Intuitively, #{T'} is the theory given by freely adding to #{T} a new morphism between the “objects” #{F} and #{G}.} diff --git a/manual/trees/002L.tree b/manual/trees/002L.tree new file mode 100644 index 00000000..beab35fd --- /dev/null +++ b/manual/trees/002L.tree @@ -0,0 +1,5 @@ +\title{Simple equational extension} +\import{prelude} +\taxon{Definition} + +\p{If #{T} is a theory, a \defcase{simple equational extension} of #{T} is another theory #{T'} given as the \em{equifier} of two indexed natural transformations #{\alpha, \beta \colon F \Rightarrow G}, where #{F} and #{G} are geometric constructs. Intuitively, #{T'} is the theory given by adding to #{T} a new equality between morphisms of “objects”.} diff --git a/manual/trees/002M.tree b/manual/trees/002M.tree new file mode 100644 index 00000000..d6d861ee --- /dev/null +++ b/manual/trees/002M.tree @@ -0,0 +1,17 @@ +\title{A refresher on geometric theories} + +\p{In this section, we briefly review the approach to geometric theories followed in [The Elephant](johnstone-2002-sketches).} + +\transclude{002C} + +\transclude{002E} + +\transclude{002F} + +\transclude{002K} + +\transclude{002L} + +\transclude{002D} + +\transclude{002G} diff --git a/manual/trees/002N.tree b/manual/trees/002N.tree new file mode 100644 index 00000000..cf3202b1 --- /dev/null +++ b/manual/trees/002N.tree @@ -0,0 +1,16 @@ +\title{Types and terms} +\import{prelude} + +\p{In this section, we build a [category with families](cwf) #{\mb{E}} out of elephant theories, which gives the semantics of types and terms in our type theory.} + +\p{Categories with families have many parts; we build up the structure in sections. We follow [Kovács](kovacs-2022-typetheoretic) in presenting a category with families as a model of a GAT. As we give the semantics for each part of the GAT, we write out the relevant part of the signature with a \check next to it to signify that this part of the model is now defined.} + +\transclude{002O} + +\transclude{002P} + +\transclude{002Q} + +\transclude{002R} + +\p{This completes the description of the bare category-with-families structure of the model, before the addition of any type formers capturing constructions in this model that possess universal properties.} diff --git a/manual/trees/002O.tree b/manual/trees/002O.tree new file mode 100644 index 00000000..1f3d096e --- /dev/null +++ b/manual/trees/002O.tree @@ -0,0 +1,13 @@ +\import{prelude} +\title{Category structure of #{\mb{E}}} + +\p{The category for #{\mb{E}} is just the category of [elephant theories](002C), where the morphisms are 2-natural transformations.} + +##{\begin{align*} +&\ms{Con} \colon \ms{Type} \quad \check \\ +&\ms{Sub} \colon \ms{Con} \to \ms{Con} \to \ms{Type} \quad \check +\end{align*}} + +\p{We omit some parts of the GAT signature; for instance here we omit the parts which declare that #{\ms{Con}} and #{\ms{Sub}} form a category. We refer to this category overall as #{\bb{C}_{\mb{E}}}.} + +\p{This category has a terminal object given by the functor constant at #{1}, the terminal category; we refer to this by #{\cdot} in light of its role as the empty context.} diff --git a/manual/trees/002P.tree b/manual/trees/002P.tree new file mode 100644 index 00000000..f6c56281 --- /dev/null +++ b/manual/trees/002P.tree @@ -0,0 +1,14 @@ +\import{prelude} +\title{Types in #{\mb{E}}} + +\p{Given a context #{\Gamma}, a type in #{\Gamma} is a 2-functor #{A \colon \left(\groth \Gamma\right)\op \to \ms{CAT}}.} + +##{\ms{Ty} \colon \ms{Con} \to \ms{Type} \quad \check} + +\p{Note that #{\ms{Ty}\,\cdot} is again just the type of elephant theories.} + +\p{In general, #{\groth \Gamma} is the 2-category of topoi equipped with a model of #{\Gamma}. In the case that #{\Gamma} is a geometric theory, this is equivalent to elephant theories where #{\ms{BTop}/\ms{S}} is replaced by #{\ms{BTop}/\ms{S}[\Gamma]}, where #{\ms{S}[\Gamma]} is the classifying topos for #{\Gamma}. Thus, #{\ms{Ty}\,\Gamma} can be thought of as the collection of elephant theories relative to #{\Gamma}.} + +\p{It is not hard to see that #{\ms{Ty}} forms a presheaf over #{\bb{C}_{\mb{E}}} because we can apply the Grothendieck construction to the 2-natural transformation #{\gamma \colon \Delta \To \Gamma} to get #{\groth \gamma \colon \groth \Delta \to \groth \Gamma}, and then precomposition with #{\groth \gamma} gives us the required map from #{\ms{Ty}\,\Gamma} to #{\ms{Ty}\,\Delta}.} + +##{{-}[-] \colon \{\Delta\;\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to (\ms{Sub}\,\Delta\,\Gamma) \to \ms{Ty}\,\Delta \quad \check} diff --git a/manual/trees/002Q.tree b/manual/trees/002Q.tree new file mode 100644 index 00000000..692718fc --- /dev/null +++ b/manual/trees/002Q.tree @@ -0,0 +1,25 @@ +\import{prelude} +\title{Terms in #{\mb{E}}} + +\p{Given a context #{\Gamma} and a type #{A \colon \left(\groth \Gamma\right)\op \to \ms{CAT}}, a term #{a} of type #{A} is a 2-section of #{A}.} + +##{\ms{Tm} \colon (\Gamma \colon \ms{Con}) \to \ms{Ty}\,\Gamma \to \ms{Type} \quad \check} + +\p{The categorical way to define “2-section” would be as a strict 2-functor #{a \colon \groth \Gamma \to \groth A} that is a strict section of the projection. A more type-theoretic way to define “2-section” would be to say a 2-section is a map #{a \colon \left((\mc{E},M) \colon \groth \Gamma\right) \to A(\mc{E},M)} such that #{a(\mc{E},M)} is 2-functorial in #{\mc{E}} and #{M}.} + +\p{Given #{\gamma \colon \Delta \To \Gamma}, we may define #{a[\gamma] \colon \ms{Tm}\,\Delta\,(A[\gamma])} by + +##{ +\begin{align*} +&a[\gamma] : \left((\mc{E}, M) \colon \groth \Delta\right) \to {A[\gamma]}(\mc{E}, M) \\ +&a[\gamma] (\mc{E}, M) = a(\mc{E}, \gamma_{\mc{E}}(M)) +\end{align*} +} +which is well-typed, because #{{A[\gamma]}(\mc{E}, M) = A(\mc{E}, \gamma_{\mc{E}}(M))}} + +\p{This turns #{\ms{Tm}} into an indexed presheaf over #{\ms{Ty}}.} + +##{\begin{align*} + &{-}[-] \colon \{\Delta\;\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \\ + &\quad \ms{Tm}\,\Gamma\,A \to (\gamma \colon \Delta \To \Gamma) \to \ms{Tm}\,\Delta\,(A[\gamma]) \quad \check +\end{align*}} diff --git a/manual/trees/002R.tree b/manual/trees/002R.tree new file mode 100644 index 00000000..e870de19 --- /dev/null +++ b/manual/trees/002R.tree @@ -0,0 +1,28 @@ +\import{prelude} +\title{Context extension in #{\mb{E}}} + +\p{Given a context #{\Gamma} and type #{A}, we define the context extension #{\Gamma \ext A} by} + +##{(\Gamma \ext A)(\mc{E} \colon \ms{BTop}/\mc{S}) = (M \colon \Gamma(\mc{E})) \times A(\mc{E},M)} + +\p{extended suitably to produce a category, and to be 2-functorial.} + +##{{-}\ext{-} \colon (\Gamma \colon \ms{Con}) \to \ms{Ty}\,\Gamma \to \ms{Con} \quad \check} + +\p{We then have the weakening substitution given by first projection and the variable rule given by second projection.} + +##{\begin{align*} +&\ms{p} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to (\Gamma \ext A \To \Gamma) \quad \check \\ +&\ms{q} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \ms{Tm}\,(\Gamma \ext A)\,(A[\ms{p}]) \quad \check +\end{align*}} + +\p{Finally, context comprehension is defined by pairing.} + +##{\begin{align*} + &({-},{-}) \colon \{\Delta\;\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \\ + &\quad (\gamma \colon \Delta \To \Gamma) \to \ms{Tm}\,\Delta\,(A[\gamma]) \to (\Delta \To \Gamma \ext A) \quad \check +\end{align*}} + +\p{Weakening/variable and context comprehension then can be used to form an isomorphism:} + +##{(\Delta \Rightarrow \Gamma \ext A) \cong (\gamma \colon \Delta \Rightarrow \Gamma) \times \ms{Tm}\,\Delta\,(A[\gamma]) \quad \check} diff --git a/manual/trees/002S.tree b/manual/trees/002S.tree new file mode 100644 index 00000000..b16d793b --- /dev/null +++ b/manual/trees/002S.tree @@ -0,0 +1,14 @@ +\title{Levels and universes} +\import{prelude} + +\p{The basic structure of types and terms works for general elephant theories, but we are most concerned with geometric theories. To handle this, we add additional judgments inspired by the approach to levels and universes introduced by Jon Sterling in [[sterling-2025-fuss-free]].} + +\p{Note that Jon uses this for universe levels in MLTT, where the type theory “at each level” is essentially the same. However, in our use of levels, certain rules in the type theory will only apply at certain levels.} + +\transclude{002U} + +\transclude{0030} + +\transclude{002T} + +\transclude{002W} diff --git a/manual/trees/002T.tree b/manual/trees/002T.tree new file mode 100644 index 00000000..460a3362 --- /dev/null +++ b/manual/trees/002T.tree @@ -0,0 +1,16 @@ +\title{Geometric theories} +\import{prelude} + +\p{We introduce a judgment on types capturing when an elephant theory is a geometric theory. Confusingly enough, in Coln we call types where this judgment holds \defcase{theories}; unrestricted types, corresponding to arbitrary elephant theories, are called \defcase{top-level} types.} + +##{\ms{IsTheory} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop}} + +\p{A proof of #{\ms{IsTheory}\,A} is a proof that there merely exists a construction of #{A} as a sequence of simple functional and simple equational extensions of the object classifier, establishing it as a [geometric theory](002D). As #{\ms{IsTheory}\,A} is a proposition, we propositionally truncate the type of such constructions.} + +##{\ms{IsTheory} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop} \quad \check} + +\p{We then internalize this into a universe. The universe #{\ms{Theory} \colon \ms{Ty}\,\cdot} sends a topos #{\mc{E}} to the category of geometric theories #{A \colon (\ms{BTop}/\mc{E})\op \to \ms{CAT}}.} + +##{\ms{Tm}\,\Gamma\,\ms{Theory} \cong (A \colon \ms{Ty}\,\Gamma) \times \ms{IsTheory}\,A \quad \check} + +\p{This is the shakiest part of the semantics for this type theory; it may be that non-strictness or size issues make this universe infeasible. However, this can be fixed by moving to a two-level type theory. “Presheaves over elephant theories” seems a bit absurd though, so hopefully this can work out as is.} diff --git a/manual/trees/002U.tree b/manual/trees/002U.tree new file mode 100644 index 00000000..844d392e --- /dev/null +++ b/manual/trees/002U.tree @@ -0,0 +1,16 @@ +\title{Sets} +\import{prelude} + +\p{We introduce a judgment on types capturing when an elephant theory is a [geometric construct](002F). We call types for whom this judgment holds \defcase{sets}.} + +##{\ms{IsSet} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop}} + +\p{A proof of #{\ms{IsSet}\,A} for #{A \colon \ms{Ty}\,\Gamma} is a natural choice of objects #{((\mc{E},M) \colon \groth \Gamma) \mapsto (X_{A}(\mc{E},M) \colon \mc{E})} such that #{A(\mc{E},M) \cong \mc{E}(1, X_{A}(\mc{E},M))}.} + +##{\ms{IsSet} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop} \quad \check} + +\p{We then have a universe #{\ms{Set}} which is given by the \em{weak} object classifier, which sends a topos #{\mc{E}} to the category of representable presheaves on #{\ms{Sh}(\mc{E})}. This is equivalent to the object classifier, but we use it because it makes the isomorphism below work out.} + +##{\ms{Tm}\,\Gamma\,\ms{Set} \cong (A \colon \ms{Ty}\,\Gamma) \times \ms{IsSet}\,A \quad \check} + +\p{In the above isomorphism, we call the right-to-left direction \defcase{encoding} and the left-to-right direction \defcase{decoding}.} diff --git a/manual/trees/002V.tree b/manual/trees/002V.tree new file mode 100644 index 00000000..be58c3b8 --- /dev/null +++ b/manual/trees/002V.tree @@ -0,0 +1,22 @@ +\title{Record types} +\import{prelude} + +\p{In the Coln implementation, we have general #{n}-ary record types with named fields. However, for the sake of simplicity, here we only cover binary dependent records, also known as #{\Sigma}-types.} + +##{\begin{align*} + &\Sigma \colon \{\Gamma \colon \ms{Con}\} \to (A \colon \ms{Ty}\,\Gamma) \to (\ms{Ty}\,(\Gamma \ext A)) \to \ms{Ty}\,\Gamma \\ + &\ms{Tm}\,\Gamma\,(\Sigma\,A\,B) \cong (a \colon \ms{Tm}\,\Gamma\,A) \times \ms{Tm}\,\Gamma\,(B[(1_\Gamma, a)]) +\end{align*}} + +\p{This is fairly straightforward to give semantics to. Fix some elephant theory #{\Gamma}, and let #{A \colon (\groth \Gamma)\op \to \ms{CAT}}, #{B \colon (\groth \Gamma \ext A)\op \to \ms{CAT}}. Then #{(\Sigma\,A\,B) \colon (\groth \Gamma)\op \to \ms{CAT}} may be defined by} + +##{(\Sigma\,A\,B)(\mc{E},M) = (a \colon A(\mc{E},M)) \times B(\mc{E},(M,a))} + +\p{It is straightforward to then interpret the projections, etc.} + +##{\begin{align*} + &\Sigma \colon \{\Gamma \colon \ms{Con}\} \to (A \colon \ms{Ty}\,\Gamma) \to (\ms{Ty}\,(\Gamma \ext A)) \to \ms{Ty}\,\Gamma \quad \check \\ + &\ms{Tm}\,\Gamma\,(\Sigma\,A\,B) \cong (a \colon \ms{Tm}\,\Gamma\,A) \times \ms{Tm}\,\Gamma\,(B[(1_\Gamma, a)]) \quad \check +\end{align*}} + +\p{Slightly less trivial to verify is that #{\Sigma} preserves the levels of its constituent types.} diff --git a/manual/trees/002W.tree b/manual/trees/002W.tree new file mode 100644 index 00000000..2f2ad7c7 --- /dev/null +++ b/manual/trees/002W.tree @@ -0,0 +1,12 @@ +\title{Sets are geometric theories} +\import{prelude} + +\p{Any [set](002U) is a [theory](002T), in the sense that we have.} + +##{\ms{SetImpliesTheory} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \ms{IsSet}\,A \to \ms{IsTheory}\,A} + +\p{This is because #{\ms{IsSet}\,A} implies that the data of #{A \colon (\groth \Gamma)\op \to \ms{CAT}} is equivalent to a 2-natural transformation #{X_A \colon \Gamma \To \bb{O}} into the object classifier, and thus #{A} is a simple functional extension of the empty theory given by postulating a morphism #{1 \to X_A}. In other words, #{A} is really “the theory of a global element of #{X_A}”. \mvrnote{I may have introduced an error here}} + +##{\ms{SetImpliesTheory} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \ms{IsSet}\,A \to \ms{IsTheory}\,A \quad \check} + +\p{One can use #{\ms{SetImpliesTheory}} along with the encoding and decoding functions for #{\ms{Set}} and #{\ms{Theory}} in order to define a function #{\ms{Tm}\,\Gamma\,\ms{Set} \to \ms{Tm}\,\Gamma\,\ms{Theory}}. The advantage of #{\ms{SetImpliesTheory}} over directly postulating this function is that, in the way we have set things up, promotion from #{\ms{Set}} to #{\ms{Theory}} automatically commutes with encoding/decoding.} diff --git a/manual/trees/002X.tree b/manual/trees/002X.tree new file mode 100644 index 00000000..b8f1b1be --- /dev/null +++ b/manual/trees/002X.tree @@ -0,0 +1,4 @@ +\title{Function types} +\import{prelude} + +\p{\mvrnote{TODO}} diff --git a/manual/trees/002Y.tree b/manual/trees/002Y.tree new file mode 100644 index 00000000..88903a17 --- /dev/null +++ b/manual/trees/002Y.tree @@ -0,0 +1,4 @@ +\title{Equality types} +\import{prelude} + +\p{\mvrnote{TODO}} diff --git a/manual/trees/002Z.tree b/manual/trees/002Z.tree new file mode 100644 index 00000000..1dad414f --- /dev/null +++ b/manual/trees/002Z.tree @@ -0,0 +1,4 @@ +\title{Inductive types} +\import{prelude} + +\p{\mvrnote{TODO}} diff --git a/manual/trees/0030.tree b/manual/trees/0030.tree new file mode 100644 index 00000000..acdaf781 --- /dev/null +++ b/manual/trees/0030.tree @@ -0,0 +1,4 @@ +\title{Propositions} +\import{prelude} + +\p{\mvrnote{TODO}} diff --git a/manual/trees/0031.tree b/manual/trees/0031.tree new file mode 100644 index 00000000..8db20430 --- /dev/null +++ b/manual/trees/0031.tree @@ -0,0 +1,30 @@ +\title{Base types} +\import{prelude} + +\p{Coln includes two base types for demonstration purposes: +\code{String} and \code{Int}. Both are ultimately stored as a single +database column. As we saw previously:} + +\pre{% +\kw{theory} FavouriteNumber := Int +} + +\dbexample{ + \p{\strong{Table \code{FavouriteNumber}}} + + \table{ + \row{\hcell{\code{root : Int}}} + }{ + \row{\cell{19}} + } + +\p{\strong{Constraints:} +\ul{ + \li{\code{FavouriteNumber} has exactly one row.} +} +} +} + +\p{A word of caution: the user is not currently prevented from writing theories that would require an infinite amount of storage to produce a valid instance of, for example, the theory of [functions](001E) \code{String -> String}.} + +% \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. \mvrnote{Has the fix here actually been figured out?}} diff --git a/manual/trees/0032.tree b/manual/trees/0032.tree new file mode 100644 index 00000000..9ce9d1ed --- /dev/null +++ b/manual/trees/0032.tree @@ -0,0 +1,140 @@ +\title{Coln in practice} +\import{prelude} + +\transclude{000O} + +\p{\mvrnote{typescript here}} + +\p{In TypeScript, models of \code{Set} store collections of \code{Value}s, where \code{Value} is defined in the following way} + +\pre{% +\kw{const} RowId = { + from: DatabaseId, + index: number +} + +\kw{const} Value = + { tag: "row_id", value: RowId } | + { tag: "tuple", value: Record } | + { tag: "int", value: number } | + { tag: "string", value: string } +} + +\p{All elements in the collection should be of the same type (e.g. all row ids, all strings, etc.) but for simplicity all sets share the same untyped API involving \code{Value}s.} + +\p{A TypeScript value \code{m} that refers to a model of \code{Set} satisfies the following interface} + +\pre{% +\kw{interface} ReadonlySet { + has(x: Value): boolean; + values(): Iterator; +} +} + +\p{If \code{m} has read-write permissions, then it will also satisfy the interface} + +\pre{% +\kw{interface} ReadWriteSet \kw{extends} ReadonlySet { + add(): Value; +} +} + +\p{Intuitively, \code{add()} does not take parameters because it adds a \em{fresh} element to the set, an element not equal to any other previous element. This means that a set of integers can never be read-write because it is impossible to create a fresh integer. We will see later on that it is instead possible to store a \em{subset} of the set of all integers; this will look differently however.} + +\p{For a set with read-write permission, the following code should not throw an error.} + +\pre{% +\kw{const} a = m.add() +assert(m.has(a)) +} + +\p{More precisely, if we have a model \code{m} of \code{SantaList} in TypeScript, then \code{m.naughty} and \code{m.nice} are both models of \code{Set}. If \code{m} is readonly, then \code{m.naughty} and \code{m.nice} will satisfy \code{ReadonlySet}, and if \code{m} is read-write, then \code{m.naughty} and \code{m.nice} will satisfy \code{ReadWriteSet}. The following TypeScript code should run without errors if \code{m} is a read-write model of \code{SantaList}.} + +\pre{% +\kw{const} alice = m.nice.add() +\kw{const} bob = m.naughty.add() +assert(m.nice.has(alice)) +assert(!m.nice.has(bob)) +} + +\p{In TypeScript, an element of a set comes along with a getter, and if it is read-write, also a setter. So if \code{m} is a TypeScript variable accessing a model of \code{PopulatedSantaList}, then we should have:} + +\pre{assert(m.list.nice.has(m.john.get()))} + +\p{If \code{m} is \em{incomplete}, then \code{m.john.get()} might return \code{null}. This would be the case in a freshly-created model, as in} + +\pre{\kw{const} m = PopulatedSantaList.create()} + +\p{This can be remedied by using \code{.set()}, as in} + +\pre{% +\kw{const} john = m.list.nice.add() +m.john.set(john) +} + +\p{Note that \code{m.john.set(x)} would throw an exception if \code{x} were not in \code{m.list.nice}.} + +\p{Concretely, in TypeScript, we could use this like} + +\pre{% +\kw{const} m = StateMachine.create() +\kw{const} [x,y] = [m.state.add(), m.state.add()] +m.next(x).set(y) +m.next(y).set(y) +} + +\p{Note that at the point where we have added \code{x} and \code{y} but not yet set the values of \code{next} for them, \code{m} is not a valid instance for \code{StateMachine}. In fact, in general it is inevitable that in the process of building a model one may pass through an invalid state. Thus, validity is only checked at certain points; we discuss validity more in a later section.\todo} + +\p{From TypeScript, we could use a model \code{m} of \code{SantaLists} in the following way.} + +\pre{% +\kw{const} y2025 = m.year.add() +\kw{const} bob = m.list(y2025).nice.add() +} + +\p{From TypeScript, using a model of \code{Drama} would look like:} + +\pre{% +\kw{const} [john, mary] = [m.person.add(), m.person.add()] +m.jealous_of(john)(mary).makeTrue() +} + +\p{Note that because names in f-notation can contain characters like \code{-} that are not allowed in TypeScript, we have to \em{mangle} the Coln name to create the TypeScript API. As \code{person_of} is also a valid name in Coln, a theory could have both \code{person-of} and \code{person_of} fields. In this case, emitting the TypeScript FFI would emit an error. The suggested fix is to not have fields that differ only by choice of hyphen/underscore, because that is bad and confusing in any case.} + + +\p{In TypeScript, we could interact with a read-write model \code{m} of this new \code{SantaLists} in the following way.} + +\pre{% +\kw{const} john = m.children.add() +\kw{const} y2025 = m.year.add() +\kw{const} y2026 = m.year.add() +m.list(y2025).nice(john).makeTrue() +m.list(y2026).naughty(john).makeTrue() +} + +\p{We saw [earlier](001E) one way in which a model of a theory might be incomplete; a function might not yet be defined for given values of its inputs. Here we have a similar situation. For instance, we might have written:} + +\pre{% +\kw{const} [john, mary, sue] = + [m.person.add(), m.person.add(), m.person.add()] +m.jealous_of(john)(mary).makeTrue() +m.jealous_of(mary)(sue).makeTrue() +} + +\p{When checking validity of \code{m} after executing this code, Coln will report that \code{jealous-of/is-transitive john mary sue _ _ : jealous-of mary sue} is not satisfied (though, Coln does not know what names we have given to these variables in TypeScript, so it would actually print out the row identifiers instead of the names).\todo Unlike with \code{next} in the [section on functions](001E), to fix this we don't need to touch \code{jealous-of/is-transitive}. Instead, we can just run \code{m.jealous_of(john)(sue).makeTrue()}, and the model will be valid again. This is because if the codomain of a function is a proposition, there is ultimately only one possible way for that function to exist, and thus the function need not be explicitly defined. We discuss how this works in a later section.\todo} + +\p{In TypeScript, \code{jealousy-triangle} is compiled to a function that takes in a model of \code{Drama} and returns a \code{ReadonlySet}.\todo The elements \code{v} of this \code{ReadonlySet} are \code{Value}s with the \code{"tuple"} tag, which have fields \code{a},\code{b},\code{c} that are elements of \code{m.person}, such that \code{m.jealous-of(v.value.a)(v.value.b).isTrue()}, and so on. The value \code{v} will also have \code{v.value.a_b}, but it will just be \code{null}, thought of as the unique element of the singleton set.} + +\p{Iterating through the elements of \code{jealousy_triangle(m)} will be faster than the naive approach of a triply-nested for-loop over \code{m.person} and then filtering out using \code{m.jealous-of}, because Coln can \em{plan} the query and take advantage of fast join algorithms on the \code{m.jealous-of} table.\todo} + +\p{From TypeScript, we have the interface} + +\pre{% +\kw{interface} ReadonlyProp { + isTrue(): boolean; +} + +\kw{interface} ReadWriteProp \kw{extends} ReadonlyProp { + makeTrue(): void; +} +} diff --git a/manual/trees/0033.tree b/manual/trees/0033.tree new file mode 100644 index 00000000..d3c70571 --- /dev/null +++ b/manual/trees/0033.tree @@ -0,0 +1,24 @@ +\title{Levels} +\import{prelude} + +\p{Types cannot be combined in arbitrary ways and still have a sensible database interpretation; the simplest example is the type \code{Set -> String}, which cannot hope to store information for every possible abstract collection. The interpretations that each type in a Coln program supports are tracked in a system of \defcase{type levels}.} + +\p{Every type in a Coln program has a \defcase{level}, which dictates the positions in a Coln program it may appear. Types at all levels use the same syntax, but some operations will only succeed for types of a given level. That is, to be valid a Coln program must be both type-correct (types line up wherever they are used together) and level-correct (inputs to constructions have the permitted levels). This is checked by the compiler, and any issues will produce an error during [elaboration](000O).} + +\p{ +There are four levels in which a type may live: +##{ +\lvl{prop} \subset \lvl{set} \subset \lvl{theory} \subset \lvl{top} +} +Each is included in the next, so a type with level #{\lvl{prop}} may be silently used as a type of level #{\lvl{set}}, and so on. + +To a first approximation (and slightly out of order), a type at each level has the following interpretation: +\ul{ + \li{#{\lvl{set}}: A \defcase{set}, i.e. type with level #{\lvl{set}}, is a type of [plain old data](https://en.wikipedia.org/wiki/Passive_data_structure). A set can ultimately be compiled down to an individual database table, with each element of the set captured by a single row, and a column for each field.} + \li{#{\lvl{prop}}: A \defcase{proposition}, i.e. type with level #{\lvl{prop}}, is a set with at most one element, whose existence we interpret as the proof of the proposition. A proposition may ultimately be represented by a row in a database, or as constraints on the database, depending on the exact form of the proposition.} + \li{#{\lvl{theory}}: A \defcase{theory}, i.e. type with level #{\lvl{theory}}, represents a database schema, possibly involving many tables and rules. We will sometimes refer to an element of a theory as a \defcase{model}, which you can think of as a specific database instance of the schema described by that theory.} + \li{#{\lvl{top}}: A \defcase{top-level type}, i.e. type with level #{\lvl{top}}, is a generic type about which we can make no guarantees in terms of a database interpretation. The type of the contents of a Coln source file is a top-level type, and is permitted to mix definitions with all of the above levels. In particular, this includes theories parameterised by models of another theory, which must wait for a concrete argument before they can be given a database meaning.} +} +} + +\p{The type \code{state -> state} satisfies the criterion for being a theory because its domain is a set and its codomain is a theory (following [[001D]]).} diff --git a/manual/trees/0034.tree b/manual/trees/0034.tree new file mode 100644 index 00000000..a5f82a0c --- /dev/null +++ b/manual/trees/0034.tree @@ -0,0 +1,21 @@ +\title{Parameterised theories} +\import{prelude} + +\p{Coln also provides the facility for functions at the \em{theory} level, which enables code reuse between database schemas. As a simple example:} + +\pre{% +\kw{theory} StateMachineOn (state : Set) := \kw{sig} + next : state -> state +\kw{end} +} + +\pre{% +\kw{theory} Factory := \kw{sig} + steps : Set + chocolate-recipe : StateMachineOn steps + rooms : Set + boat-ride : StateMachineOn rooms +\kw{end} +} + +% Example instance diff --git a/manual/trees/0035.tree b/manual/trees/0035.tree new file mode 100644 index 00000000..cd620c41 --- /dev/null +++ b/manual/trees/0035.tree @@ -0,0 +1,23 @@ +\title{Queries and Views} +\import{prelude} + + +\p{\mvrnote{TODO, something like:} some of the above have alternative useful interpretations. A set, described in the context of a model, is a construction that might mention pieces of the model. This can be interpreted as a \defcase{query} over the database instance described by that model, so that the result of the query is the collection of occurrences of the construction in the model, see [TODO](TODO). Similarly a proposition in the context of a model can be interpreted as \mvrnote{something something datalog}.} + +\p{We go into much more detail about the database interpretation of types in a [later section](000M).} + + +\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{001J} + +\transclude{001K} + +\transclude{001L} + +\transclude{001M} diff --git a/manual/trees/0036.tree b/manual/trees/0036.tree new file mode 100644 index 00000000..cc058730 --- /dev/null +++ b/manual/trees/0036.tree @@ -0,0 +1,4 @@ +\title{Worked Example} +\import{prelude} + +\mvrnote{Trimmed down version of ssa.coln maybe?} diff --git a/manual/trees/glossary/cwf.tree b/manual/trees/glossary/cwf.tree new file mode 100644 index 00000000..7cbaf17a --- /dev/null +++ b/manual/trees/glossary/cwf.tree @@ -0,0 +1,4 @@ +\title{Category with Families} +\taxon{Term} + +\p{See: the [nlab page on categorical semantics of dependent type theory](https://ncatlab.org/nlab/show/categorical+semantics+of+dependent+type+theory#categories_with_families).} diff --git a/manual/trees/people/ambrus-kaposi.tree b/manual/trees/people/ambrus-kaposi.tree new file mode 100644 index 00000000..e3f68935 --- /dev/null +++ b/manual/trees/people/ambrus-kaposi.tree @@ -0,0 +1,2 @@ +\title{Ambrus Kaposi} +\taxon{person} \ No newline at end of file diff --git a/manual/trees/people/szumi-xie.tree b/manual/trees/people/szumi-xie.tree new file mode 100644 index 00000000..8d3a23b9 --- /dev/null +++ b/manual/trees/people/szumi-xie.tree @@ -0,0 +1,2 @@ +\title{Szumi Xie} +\taxon{person} \ No newline at end of file diff --git a/manual/trees/prelude.tree b/manual/trees/prelude.tree index 88f9bb2d..2bdaaa4e 100644 --- a/manual/trees/prelude.tree +++ b/manual/trees/prelude.tree @@ -10,12 +10,37 @@ \def\cell[content]{\{\content}} \def\hcell[content]{\{\content}} +\def\collapsedaside[~body]{ + \scope{ + \put\transclude/expanded{false} + \put\transclude/toc{false} + \put\transclude/numbered{false} + \subtree{\body{}} + } +} + +\def\dbexample[body]{ + \collapsedaside{ + \taxon{Example Instance} + \[class]{database-example}{\body} + } +} + \def\todo{\[class]{smallcaps}{todo}} \def\kw[x]{\strong{\x}} \def\ms[t]{\mathsf{\t}} +\def\mb[t]{\mathbf{\t}} \def\mc[t]{\mathcal{\t}} \def\bb[t]{\mathbb{\t}} \def\op{^\mathrm{op}} -\def\groth{\int} +\def\groth{{\textstyle\int}} \def\ext{\triangleright} + +\def\check{✅} + +\def\To{\Rightarrow} + +\def\mvrnote[~body]{\[style]{color: blue;}{MVRNOTE: \body{}}} + +\def\lvl[name]{\mathfrak{\name}} diff --git a/manual/trees/references/kaposi-2024-secondorder.tree b/manual/trees/references/kaposi-2024-secondorder.tree new file mode 100644 index 00000000..0e2817e9 --- /dev/null +++ b/manual/trees/references/kaposi-2024-secondorder.tree @@ -0,0 +1,22 @@ +\title{Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics} +\author{ambrus-kaposi} +\author{szumi-xie} +\date{2024} +\taxon{reference} +\meta{doi}{10.4230/LIPICS.FSCD.2024.10} +\meta{bibtex}{\verb>>| +@inproceedings{kaposi-2024-secondorder, + doi = {10.4230/LIPICS.FSCD.2024.10}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.10}, + author = {Kaposi, Ambrus and Xie, Szumi}, + keywords = {Type theory, universal algebra, inductive types, quotient inductive types, higher-order abstract syntax, logical framework, Theory of computation → Type theory}, + language = {en}, + title = {Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics}, + journal = {LIPIcs, Volume 299, FSCD 2024}, + volume = {299}, + pages = {10:1-10:24}, + publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik}, + year = {2024}, + copyright = {Creative Commons Attribution 4.0 International license} +} +>>} \ No newline at end of file diff --git a/manual/trees/references/sterling-2025-fuss-free.tree b/manual/trees/references/sterling-2025-fuss-free.tree new file mode 100644 index 00000000..6c8e3497 --- /dev/null +++ b/manual/trees/references/sterling-2025-fuss-free.tree @@ -0,0 +1,4 @@ +\title{Fuss-free universe hierarchies} +\author{jon-sterling} +\taxon{Reference} +\meta{external}{https://www.jonmsterling.com/01HX/}