diff --git a/README b/README index d08cd935e..d4c5931d6 100644 --- a/README +++ b/README @@ -5,18 +5,12 @@ Welcome to the GEB project. ## Links - - Here is the [official repository](https://github.com/anoma/geb/) and [HTML documentation](https://anoma.github.io/geb/) for the latest version. - - ### code coverage - - For test coverage it can be found at the following links: [SBCL test coverage](./tests/cover-index.html) @@ -34,8 +28,6 @@ I recommend reading the CCL code coverage version, as it has proper tags. Currently they are manually generated, and thus for a more accurate assessment see GEB-TEST:CODE-COVERAGE - - ## Getting Started Welcome to the GEB Project! @@ -291,8 +283,6 @@ conjectures about GEB ## Categorical Model - - Geb is organizing programming language concepts (and entities!) using [category theory](https://plato.stanford.edu/entries/category-theory/), originally developed by mathematicians, @@ -360,31 +350,31 @@ In particular, we shall rely on the following universal constructions: -1. The construction of binary products $A × B$ of sets $A,B$, and the empty product $mathsf{1}$. +1. The construction of binary products $A × B$ of sets $A,B$, and the empty product $\mathsf{1}$. 2. The construction of “function spaces” $B^A$ of sets $A,B$, called *exponentials*, i.e., collections of functions between pairs of sets. 3. The so-called [*currying*](https://en.wikipedia.org/wiki/Currying) of functions, - $C^{(B^A)} cong C^{(A × B)}$, + $C^{(B^A)} \cong C^{(A × B)}$, such that providing several arguments to a function can done either simultaneously, or in sequence. 4. The construction of sums (a.k.a. co-products) $A + B$ of sets $A,B$, corresponding to forming disjoint unions of sets; - the empty sum is $varnothing$. + the empty sum is $\varnothing$. Product, sums and exponentials are the (almost) complete tool chest for writing polynomial expressions, e.g., -$$Ax^{sf 2} +x^{sf 1} - Dx^{sf 0}.$$ +$$Ax^{\sf 2} +x^{\sf 1} - Dx^{\sf 0}.$$ (We need these later to define [“algebraic data types”](https://en.wikipedia.org/wiki/Polynomial_functor_(type_theory)).) In the above expression, we have sets instead of numbers/constants -where $ mathsf{2} = lbrace 1, 2 rbrace$, -$ mathsf{1} = lbrace 1 rbrace$, -$ mathsf{0} = lbrace rbrace = varnothing$, +where $ \mathsf{2} = \lbrace 1, 2 \rbrace$, +$ \mathsf{1} = \lbrace 1 \rbrace$, +$ \mathsf{0} = \lbrace \rbrace = \varnothing$, and $A$ and $B$ are arbitrary (finite) sets. We are only missing a counterpart for the *variable*! Raising an arbitrary set to “the power” of a constant set @@ -407,8 +397,6 @@ Benjamin Pierce's as it is very amenable *and* covers the background we need in 60 short pages. - - ### Morphisms @@ -655,6 +643,21 @@ examples often given in the specific methods ``` +- [generic-function] MAYBE OBJECT + + Wraps the given OBJECT into a Maybe monad The Maybe monad in this + case is simply wrapping the term in a coprod + of so1 + + ```lisp + ;; Before + x + + ;; After + (COPROD SO1 X) + ``` + + - [generic-function] TO-CIRCUIT MORPHISM NAME Turns a MORPHISM into a Vampir circuit. the NAME is the given name of @@ -1668,6 +1671,21 @@ Various utility functions ontop of @GEB-CATEGORIES Gets the name of the moprhism +These utilities are ontop of CAT-OBJ + +- [method] MAYBE (OBJ \) + + I recursively add maybe terms to all terms, + for what maybe means checkout my generic function documentation. + + turning products of A x B into Maybe (Maybe A x Maybe B), + + turning coproducts of A | B into Maybe (Maybe A | Maybe B), + + turning SO1 into Maybe SO1 + + and SO0 into Maybe SO0 + ### Examples PLACEHOLDER: TO SHOW OTHERS HOW EXAMPLES WORK @@ -2770,6 +2788,18 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. Note that we add contexts on the left rather than on the right contra classical type-theoretic notation. +- [class] ERR \ + + An error term of a type supplied by the user. The formal grammar of + ERR is + `lisp + (err ttype) + ` + The intended semantics are as follows: ERR represents an error node + currently having no particular feedback but with functionality to be of an + arbitrary type. Note that this is the only STLC term class which does not + have TTYPE a possibly empty accessor. + - [function] ABSURD TCOD TERM &KEY (TTYPE NIL) - [function] UNIT &KEY (TTYPE NIL) @@ -2792,6 +2822,8 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. - [function] INDEX POS &KEY (TTYPE NIL) +- [function] ERR TTYPE + Accessors of ABSURD - [method] TCOD (ABSURD ABSURD) @@ -2908,6 +2940,10 @@ Accessors of INDEX - [method] TTYPE (INDEX INDEX) +Accessors of ERR + +- [method] TTYPE (ERR ERR) + - [generic-function] TCOD OBJ - [generic-function] TDOM OBJ @@ -3051,18 +3087,30 @@ This covers the main API for the STLC module - [function] FUN-TYPE MCAR MCADR -- [method] MCAR (FUN-TYPE FUN-TYPE) +- [function] ERRORP TTERM -- [method] MCADR (FUN-TYPE FUN-TYPE) + Evaluates to true iff the term has an error subterm. -- [generic-function] MCAR OBJ +- [method] MCAR (FUN-TYPE FUN-TYPE) - Can be seen as calling CAR on a generic CLOS - [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) +- [method] MCADR (FUN-TYPE FUN-TYPE) -- [generic-function] MCADR OBJ +- [method] MAYBE (OBJECT FUN-TYPE) - like MCAR but for the CADR + I recursively add maybe terms to my domain and codomain, and even + return a maybe function. Thus if the original function was + + ``` + f : a -> b + ``` + + we would now be + + ``` + f : maybe (maybe a -> maybe b) + ``` + + for what maybe means checkout my generic function documentation. ### Transition Functions @@ -3079,44 +3127,9 @@ any other transition functions - [method] TO-CAT CONTEXT (TTERM \) - Compiles a checked term in an appropriate context into the - morphism of the GEB category. In detail, it takes a context and a term with - following restrictions: Terms come from STLC with occurences of - SO-HOM-OBJ replaced by FUN-TYPE and should - come without the slow of TTYPE accessor filled for any of - the subterms. Context should be a list of SUBSTOBJ with - the caveat that instead of SO-HOM-OBJ we ought to use - FUN-TYPE, a stand-in for the internal hom object with explicit - accessors to the domain and the codomain. Once again, note that it is important - for the context and term to be giving as per above description. While not - always, not doing so result in an error upon evaluation. As an example of a - valid entry we have - - ```lisp - (to-cat (list so1 (fun-type so1 so1)) (app (index 1) (list (index 0)))) - ``` - - while - - ```lisp - (to-cat (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0)))) - ``` - - produces an error. Error of such kind mind pop up both on the level of evaluating - WELL-DEFP and ANN-TERM1. - - Moreover, note that for terms whose typing needs addition of new context - we append contexts on the left rather than on the right contra usual type - theoretic notation for the convenience of computation. That means, e.g. that - asking for a type of a lambda term as below produces: - - ```lisp - LAMBDA> (ttype (term (ann-term1 nil (lamb (list so1 so0) (index 0))))) - s-1 - ``` - - as we count indeces from the left of the context while appending new types to - the context on the left as well. For more info check LAMB + Compiles a checked term in said context to a Geb morphism. If the term has + an instance of an erorr term, wraps it in a Maybe monad, otherwise, compiles + according to the term model interpretation of STLC - [method] TO-POLY (OBJ \) diff --git a/README.md b/README.md index 7951e5d32..770aac2d1 100644 --- a/README.md +++ b/README.md @@ -75,19 +75,13 @@ Welcome to the GEB project. ## 1 Links - - Here is the [official repository](https://github.com/anoma/geb/) and [HTML documentation](https://anoma.github.io/geb/) for the latest version. - - ### 1.1 code coverage - - For test coverage it can be found at the following links: [SBCL test coverage](./tests/cover-index.html) @@ -105,8 +99,6 @@ I recommend reading the CCL code coverage version, as it has proper tags. Currently they are manually generated, and thus for a more accurate assessment see [`GEB-TEST:CODE-COVERAGE`][417f] - - ## 2 Getting Started @@ -375,8 +367,6 @@ conjectures about GEB ## 5 Categorical Model - - Geb is organizing programming language concepts (and entities!) using [category theory](https://plato.stanford.edu/entries/category-theory/), originally developed by mathematicians, @@ -444,31 +434,31 @@ In particular, we shall rely on the following universal constructions: -1. The construction of binary products $A × B$ of sets $A,B$, and the empty product $mathsf{1}$. +1. The construction of binary products $A × B$ of sets $A,B$, and the empty product $\mathsf{1}$. 2. The construction of “function spaces” $B^A$ of sets $A,B$, called *exponentials*, i.e., collections of functions between pairs of sets. 3. The so-called [*currying*](https://en.wikipedia.org/wiki/Currying) of functions, - $C^{(B^A)} cong C^{(A × B)}$, + $C^{(B^A)} \cong C^{(A × B)}$, such that providing several arguments to a function can done either simultaneously, or in sequence. 4. The construction of sums (a.k.a. co-products) $A + B$ of sets $A,B$, corresponding to forming disjoint unions of sets; - the empty sum is $varnothing$. + the empty sum is $\varnothing$. Product, sums and exponentials are the (almost) complete tool chest for writing polynomial expressions, e.g., -$$Ax^{sf 2} +x^{sf 1} - Dx^{sf 0}.$$ +$$Ax^{\sf 2} +x^{\sf 1} - Dx^{\sf 0}.$$ (We need these later to define [“algebraic data types”](https://en.wikipedia.org/wiki/Polynomial_functor_(type_theory)).) In the above expression, we have sets instead of numbers/constants -where $ mathsf{2} = lbrace 1, 2 rbrace$, -$ mathsf{1} = lbrace 1 rbrace$, -$ mathsf{0} = lbrace rbrace = varnothing$, +where $ \mathsf{2} = \lbrace 1, 2 \rbrace$, +$ \mathsf{1} = \lbrace 1 \rbrace$, +$ \mathsf{0} = \lbrace \rbrace = \varnothing$, and $A$ and $B$ are arbitrary (finite) sets. We are only missing a counterpart for the *variable*! Raising an arbitrary set to “the power” of a constant set @@ -491,8 +481,6 @@ Benjamin Pierce's as it is very amenable *and* covers the background we need in 60 short pages. - - ### 5.1 Morphisms @@ -756,6 +744,22 @@ examples often given in the specific methods ``` + +- [generic-function] **MAYBE** *OBJECT* + + Wraps the given `OBJECT` into a Maybe monad The Maybe monad in this + case is simply wrapping the term in a [coprod][8be5] + of so1([`0`][5cfe] [`1`][f4ba]) + + ```lisp + ;; Before + x + + ;; After + (COPROD SO1 X) + ``` + + - [generic-function] **TO-CIRCUIT** *MORPHISM NAME* @@ -1897,6 +1901,22 @@ Various utility functions ontop of [Core Category][cb9e] Gets the name of the moprhism +These utilities are ontop of [`CAT-OBJ`][74bd] + + +- [method] **MAYBE** *(OBJ \)* + + I recursively add maybe terms to all [][7e58] terms, + for what maybe means checkout [my generic function documentation][65a4]. + + turning [products][06c6] of A x B into Maybe (Maybe A x Maybe B), + + turning [coproducts][8be5] of A | B into Maybe (Maybe A | Maybe B), + + turning `SO1`([`0`][5cfe] [`1`][f4ba]) into Maybe `SO1`([`0`][5cfe] [`1`][f4ba]) + + and `SO0`([`0`][5c7c] [`1`][7088]) into Maybe `SO0`([`0`][5c7c] [`1`][7088]) + ### 7.7 Examples @@ -2030,7 +2050,7 @@ layout of the term, showing what kind of data #### 9.1.1 Aiding the Visualizer One can aid the visualization process a bit, this can be done by -simply placing `ALIAS` around the object, this will place it +simply placing ALIAS around the object, this will place it in a box with a name to better identify it in the graphing procedure. @@ -3131,6 +3151,19 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term Note that we add contexts on the left rather than on the right contra classical type-theoretic notation. + +- [class] **ERR** *[\][b36a]* + + An error term of a type supplied by the user. The formal grammar of + [`ERR`][3a9f] is + `lisp + (err ttype) + ` + The intended semantics are as follows: [`ERR`][3a9f] represents an error node + currently having no particular feedback but with functionality to be of an + arbitrary type. Note that this is the only [`STLC`][e373] term class which does not + have [`TTYPE`][134c] a possibly empty accessor. + - [function] **ABSURD** *TCOD TERM &KEY (TTYPE NIL)* @@ -3164,6 +3197,9 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term - [function] **INDEX** *POS &KEY (TTYPE NIL)* + +- [function] **ERR** *TTYPE* + Accessors of [`ABSURD`][4710] @@ -3309,6 +3345,11 @@ Accessors of [`INDEX`][5b8b] - [method] **TTYPE** *(INDEX INDEX)* +Accessors of [`ERR`][3a9f] + + +- [method] **TTYPE** *(ERR ERR)* + - [generic-function] **TCOD** *OBJ* @@ -3475,22 +3516,34 @@ This covers the main API for the [`STLC`][e373] module - [function] **FUN-TYPE** *MCAR MCADR* + +- [function] **ERRORP** *TTERM* + + Evaluates to true iff the term has an error subterm. + - [method] **MCAR** *(FUN-TYPE FUN-TYPE)* - [method] **MCADR** *(FUN-TYPE FUN-TYPE)* - -- [generic-function] **MCAR** *OBJ* + +- [method] **MAYBE** *(OBJECT FUN-TYPE)* - Can be seen as calling [`CAR`][8c99] on a generic CLOS - [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) - - -- [generic-function] **MCADR** *OBJ* - - like [`MCAR`][f1ce] but for the [`CADR`][74ab] + I recursively add maybe terms to my domain and codomain, and even + return a maybe function. Thus if the original function was + + ``` + f : a -> b + ``` + + we would now be + + ``` + f : maybe (maybe a -> maybe b) + ``` + + for what maybe means checkout [my generic function documentation][65a4]. ### 12.3 Transition Functions @@ -3509,44 +3562,9 @@ any other transition functions - [method] **TO-CAT** *CONTEXT (TTERM \)* - Compiles a checked term in an appropriate context into the - morphism of the GEB category. In detail, it takes a context and a term with - following restrictions: Terms come from [`STLC`][e373] with occurences of - [`SO-HOM-OBJ`][07dd] replaced by [`FUN-TYPE`][8dcc] and should - come without the slow of [`TTYPE`][134c] accessor filled for any of - the subterms. Context should be a list of [`SUBSTOBJ`][3173] with - the caveat that instead of [`SO-HOM-OBJ`][07dd] we ought to use - [`FUN-TYPE`][8dcc], a stand-in for the internal hom object with explicit - accessors to the domain and the codomain. Once again, note that it is important - for the context and term to be giving as per above description. While not - always, not doing so result in an error upon evaluation. As an example of a - valid entry we have - - ```lisp - (to-cat (list so1 (fun-type so1 so1)) (app (index 1) (list (index 0)))) - ``` - - while - - ```lisp - (to-cat (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0)))) - ``` - - produces an error. Error of such kind mind pop up both on the level of evaluating - [`WELL-DEFP`][4fcb] and [`ANN-TERM1`][ac2d]. - - Moreover, note that for terms whose typing needs addition of new context - we append contexts on the left rather than on the right contra usual type - theoretic notation for the convenience of computation. That means, e.g. that - asking for a type of a lambda term as below produces: - - ```lisp - LAMBDA> (ttype (term (ann-term1 nil (lamb (list so1 so0) (index 0))))) - s-1 - ``` - - as we count indeces from the left of the context while appending new types to - the context on the left as well. For more info check [`LAMB`][8cde] + Compiles a checked term in said context to a Geb morphism. If the term has + an instance of an erorr term, wraps it in a Maybe monad, otherwise, compiles + according to the term model interpretation of [`STLC`][e373] - [method] **TO-POLY** *(OBJ \)* @@ -4104,6 +4122,7 @@ features and how to better lay out future tests [365a]: #x-28GEB-2EUTILS-3AELSE-20GENERIC-FUNCTION-29 "GEB.UTILS:ELSE GENERIC-FUNCTION" [3686]: #x-28GEB-DOCS-2FDOCS-3A-40ORIGINAL-EFFORTS-20MGL-PAX-3ASECTION-29 "Original Efforts" [399c]: #x-28GEB-BOOL-3A-40GEB-BOOL-20MGL-PAX-3ASECTION-29 "Booleans" + [3a9f]: #x-28GEB-2ELAMBDA-2ESPEC-3AERR-20CLASS-29 "GEB.LAMBDA.SPEC:ERR CLASS" [3d47]: #x-28GEB-DOCS-2FDOCS-3A-40GETTING-STARTED-20MGL-PAX-3ASECTION-29 "Getting Started" [3f85]: #x-28GEB-2ELAMBDA-2ESPEC-3APOS-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:POS GENERIC-FUNCTION" [3f9d]: #x-28GEB-2ELAMBDA-2ESPEC-3ACASE-ON-20CLASS-29 "GEB.LAMBDA.SPEC:CASE-ON CLASS" @@ -4124,7 +4143,6 @@ features and how to better lay out future tests [4938]: #x-28GEB-2EMIXINS-3A-40MIXIN-EXAMPLES-20MGL-PAX-3ASECTION-29 "Mixins Examples" [49d4]: #x-28GEB-2EMAIN-3A-40GEB-UTILITY-20MGL-PAX-3ASECTION-29 "Utility" [4a87]: #x-28GEB-DOCS-2FDOCS-3A-40OPEN-TYPE-20MGL-PAX-3AGLOSSARY-TERM-29 "GEB-DOCS/DOCS:@OPEN-TYPE MGL-PAX:GLOSSARY-TERM" - [4fcb]: #x-28GEB-2ELAMBDA-2EMAIN-3AWELL-DEFP-20GENERIC-FUNCTION-29 "GEB.LAMBDA.MAIN:WELL-DEFP GENERIC-FUNCTION" [4ffa]: #x-28GEB-2EUTILS-3A-40GEB-UTILS-MANUAL-20MGL-PAX-3ASECTION-29 "Geb Utilities" [56b3]: #x-28GEB-2ELAMBDA-2ESPEC-3ALEFT-20CLASS-29 "GEB.LAMBDA.SPEC:LEFT CLASS" [57dc]: #x-28GEB-2ESPEC-3ASUBSTMORPH-20TYPE-29 "GEB.SPEC:SUBSTMORPH TYPE" @@ -4139,6 +4157,7 @@ features and how to better lay out future tests [603e]: #x-28GEB-GUI-3A-40VISAULIZER-AID-20MGL-PAX-3ASECTION-29 "Aiding the Visualizer" [6228]: #x-28GEB-3A-40GEB-API-20MGL-PAX-3ASECTION-29 "API" [6444]: #x-28GEB-2ESPEC-3ALEFT-20CLASS-29 "GEB.SPEC:LEFT CLASS" + [65a4]: #x-28GEB-2EGENERICS-3AMAYBE-20GENERIC-FUNCTION-29 "GEB.GENERICS:MAYBE GENERIC-FUNCTION" [684b]: http://www.lispworks.com/documentation/HyperSpec/Body/s_if.htm "IF MGL-PAX:MACRO" [6a3c]: http://www.lispworks.com/documentation/HyperSpec/Body/f_bt_sb.htm "BIT FUNCTION" [6b63]: #x-28GEB-2EBITC-3A-40BITC-MANUAL-20MGL-PAX-3ASECTION-29 "Bits (Boolean Circuit) Specification"