Error Node Extension of STLC and Maybe Compilation Wrapper

Adds an error node of an arbitrary type as a new STLC
constructor. Appropriatelly changes the compilation procedure to Geb
in case an STLC term has an error subterm and wraps the compilation in
a Maybe monad.

src/lambda/lambda.lisp

@@ -46,6 +46,7 @@ to the codomain."
           ((typep f 'lamb)    (mcadr (ttype rec)))
           ((typep f 'app)     (hom-cod ctx (fun f)))
           ((typep f 'index)   (mcadr (ttype rec)))
+          ((typep f 'err)     (mcadr (ttype f)))
           (t                  (error "not a valid STLC exponential term")))))
 
 (-> index-check (fixnum list) cat-obj)
@@ -143,6 +144,7 @@ the context on the left as well. For more info check [LAMB][class]"))
                                  :ttype (hom-cod ctx fun)))
         ((index pos)        (index pos
                                    :ttype (index-check pos ctx)))
+        ((err ttype)        (err ttype))
         ((case-on on ltm rtm)
          (let* ((ann-on     (ann-term1 ctx on))
                 (type-of-on (ttype ann-on))
@@ -208,7 +210,8 @@ occurences - re-annotates the term and its subterms with actual
                                 (mapcar #'ann-term2 term)
                                 :ttype (fun-to-hom (ttype tterm))))
     ((index pos)           (index pos
-                                  :ttype (fun-to-hom (ttype tterm))))))
+                                  :ttype (fun-to-hom (ttype tterm))))
+    ((err ttype)           (err (fun-to-hom ttype)))))
 
 (defun annotated-term (ctx term)
   "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]
@@ -288,7 +291,25 @@ nil"))
                 (and (check fun)
                      (check (reduce #'pair term))))
                (index t)
-               (unit t))))
+               (unit t)
+               (err t))))
     (let ((term (ignore-errors
                  (ann-term1 ctx tterm))))
       (and term (check term)))))
+
+(defun errorp (tterm)
+  "Evaluates to true iff the term has an error subterm."
+  (cond ((or (typep tterm 'index)
+             (typep tterm 'unit)) nil)
+        ((typep tterm 'err)       t)
+        ((typep tterm 'case-on)   (or (errorp (on tterm))
+                                      (errorp (rtm tterm))
+                                      (errorp (ltm tterm))))
+        ((typep tterm 'pair)      (or (errorp (ltm tterm))
+                                      (errorp (rtm tterm))))
+        ((typep tterm 'app)       (or (errorp (fun tterm))
+                                      (some #'identity
+                                            (mapcar
+                                             (lambda (x) (errorp x))
+                                             (term tterm)))))
+        (t                        (errorp (term tterm)))))

src/lambda/package.lisp

@@ -26,6 +26,7 @@
   (well-defp          pax:generic-function)
   (fun-type           pax:class)
   (fun-type           pax:function)
+  (errorp             pax:function)
 
   (mcar              (pax:method () (fun-type)))
   (mcadr             (pax:method () (fun-type)))

src/lambda/trans.lisp

@@ -47,6 +47,207 @@ calling me"
 (defmethod empty ((class (eql (find-class 'list)))) nil)
 
 (defmethod to-cat (context (tterm <stlc>))
+  "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"
+  (if (errorp tterm)
+      (to-cat-err context tterm)
+      (to-cat-cor context tterm)))
+
+(defun maybe (f)
+  "Takes a morphism f : a -> b in Geb and produces
+Maybe(f) : (1 + a) -> (1 + b)"
+  (coprod-mor so1 f))
+
+(defun maybe-obj (ob)
+  "Wraps a [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with possible fun-type instances
+into a Maybe monad recursively"
+  (cond
+    ((typep ob 'so0)      (coprod so1 so0))
+    ((typep ob 'so1)      (coprod so1 so1))
+    ((typep ob 'coprod)   (coprod so1 (coprod (maybe-obj (mcar ob))
+                                              (maybe-obj (mcadr ob)))))
+    ((typep ob 'prod)     (coprod so1 (prod (maybe-obj (mcar ob))
+                                            (maybe-obj (mcadr ob)))))
+    ((typep ob 'fun-type) (coprod so1 (fun-type (maybe-obj (mcar ob))
+                                                (maybe-obj (mcadr ob)))))))
+
+(defun maybe-obj-comp (ob)
+  "Takes a [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with possible fun-type instances
+and removes them"
+  (fun-to-hom (maybe-obj ob)))
+
+(defun maybe-rest (ob)
+  "Takes a Geb object wrapped in Maybe and gives out the part without the
+error node"
+  (mcadr (maybe-obj-comp ob)))
+
+(defmethod to-cat-err (context (tterm <stlc>))
+  "Compiles a checked term with an error term in an appropriate context into the
+morphism of the GEB category using a Maybe monad wrapper, that is, given a
+context G and a term t of type A produces a morphism with domain
+(stlc-ctx-maybe context) and codomain (maybe-obj A).
+
+Terms come from [STLC][type] with occurences of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ]
+replaced by [FUN-TYPE][class] and should come without the slow of
+[TTYPE][generic-function] accessor filled for any of the subterms. Context should
+be a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with the caveat that instead of
+[SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] we ought to use [FUN-TYPE][class], 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-err (list so1 (fun-type so1 so1)) (app (index 1) (list (error so1))))
+```
+
+while
+
+```lisp
+(to-cat-err (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (error so1))))
+```
+
+produces an error. Error of such kind mind pop up both on the level of evaluating
+[WELL-DEFP][generic-function] and [ANN-TERM1][generic-function].
+
+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][class]
+
+Note that the Maybe wrapper also applies to the context elements due to
+functoriality concerns. Hence if one wanted to check the whether the term
+(case-on (index 0) (err so1) (unit)) with a bool in contexts fails on the
+left entry, one would need to evaluate
+
+```lisp
+LAMBDA> (gapply  (to-cat (list (coprod so1 so1))
+                         (case-on (index 0)
+                                  (err so1)
+                                  (unit)))
+                         (list (geb:right (geb:left (geb:right so1))) so1))
+(left s-1)
+```
+
+and hence get an error part of the wrapper. While evaluating the right branch
+will be done by:
+
+```lisp
+  LAMBDA> (gapply  (to-cat (list (coprod so1 so1))
+                           (case-on (index 0)
+                                    (err so1)
+                                    (unit)))
+                   (list (geb:right (geb:right (geb:right so1))) so1))
+(right s-1)
+```
+
+This follows from the fact that bool arapped in maybe is 1 + (bool + bool)"
+  (labels ((rec (context tterm)
+             (match-of stlc tterm
+               ((absurd tcod term)
+                (comp  (mcase (->left so1 (maybe-rest tcod))
+                              (init (maybe-obj-comp tcod)))
+                       (rec context term)))
+               (unit
+                (comp (->right so1 so1)
+                      (terminal (stlc-ctx-maybe context))))
+               ((left rty term)
+                (comp  (->right so1 (maybe-rest (ttype tterm)))
+                       (comp (->left (maybe-obj-comp (ttype term))
+                                     (maybe-obj-comp rty))
+                             (rec context term))))
+               ((right lty term)
+                (comp (->right so1 (maybe-rest (ttype tterm)))
+                      (comp  (->right (maybe-obj-comp lty)
+                                      (maybe-obj-comp (ttype term)))
+                             (rec context term))))
+               ((case-on on ltm rtm)
+                (let ((mcartoon  (mcar (ttype on)))
+                      (mcadrtoon (mcadr (ttype on)))
+                      (ctx       (stlc-ctx-maybe context)))
+                  (comp (mcase (comp (->left so1 (maybe-rest (ttype tterm)))
+                                     (terminal (prod ctx so1)))
+                               (comp (mcase (commutes-left
+                                             (rec
+                                              (cons mcartoon
+                                                    context)
+                                              ltm))
+                                            (commutes-left
+                                             (rec
+                                              (cons mcadrtoon
+                                                    context)
+                                              rtm)))
+                                     (distribute ctx
+                                                 (maybe-obj-comp mcartoon)
+                                                 (maybe-obj-comp mcadrtoon))))
+                        (comp (distribute ctx
+                                          so1
+                                          (maybe-rest (coprod mcartoon
+                                                              mcadrtoon)))
+                              (geb:pair ctx (rec context on))))))
+               ((pair ltm rtm)
+                (let ((lty  (ttype ltm))
+                      (rty  (ttype rtm)))
+                  (comp (->right so1 (prod (maybe-obj-comp lty)
+                                           (maybe-obj-comp rty)))
+                        (geb:pair (rec context ltm)
+                                  (rec context rtm)))))
+               ((fst term)
+                (let ((mcarttot (mcar (ttype term))))
+                  (comp (mcase (->left so1 (maybe-rest mcarttot))
+                               (<-left (maybe-obj-comp mcarttot)
+                                       (maybe-obj (mcadr (ttype term)))))
+                        (rec context term))))
+               ((snd term)
+                (let ((mcadrttot (mcadr (ttype term))))
+                  (comp (mcase (->left so1 (maybe-rest mcadrttot))
+                               (<-right (maybe-obj-comp (mcar (ttype term)))
+                                        (maybe-obj-comp mcadrttot)))
+                        (rec context term))))
+               ((lamb tdom term)
+                (comp (->right so1 (maybe-rest (fun-to-hom (ttype tterm))))
+                      (apply-n (length tdom)
+                               #'(lambda (x) (curry (commutes-left x)))
+                               (rec (append
+                                     (mapcar #'maybe-obj-comp tdom)
+                                     context) term))))
+               ((app fun term)
+                (let ((tofun (ttype fun)))
+                  (comp
+                   (mcase (->left so1 (maybe-rest tofun))
+                          (commutes-left
+                           (so-eval (maybe-obj-comp (mcar tofun))
+                                    (maybe-obj-comp (mcadr tofun)))))
+                   (comp (distribute (reduce #'prod
+                                             (mapcar #'maybe-obj-comp term)
+                                             :from-end t)
+                                     so1
+                                     (maybe-rest tofun))
+                         (geb:pair (reduce #'geb:pair
+                                           (mapcar #'(lambda (x) (rec context x)) term)
+                                           :from-end t)
+                                   (rec context
+                                        fun))))))
+               ((index pos)
+                (stlc-ctx-proj (mapcar #'maybe-obj context) pos))
+               ((err ttype)
+                (comp (->left so1 (maybe-obj-comp ttype))
+                      (terminal (stlc-ctx-maybe context)))))))
+    (if (not (well-defp context tterm))
+        (error "not a well-defined ~A in said ~A" tterm context)
+        (rec context (ann-term1 context tterm)))))
+
+
+(defmethod to-cat-cor (context (tterm <stlc>))
   "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][type]  with occurences of
@@ -61,13 +262,13 @@ 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))))
+ (to-cat-cor (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))))
+(to-cat-cor (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
@@ -87,7 +288,7 @@ 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][class]
 
 Finally, note that the compilation uncurries the final morphism. That is,
-if the type of the term is an exponential object, [TO-CAT] uncurries the
+if the type of the term is an exponential object, [TO-CAT-COR] uncurries the
 morphism in the Geb category instead producing a morphism into the domain
 of the exponential from a corresponding product. If the exponential is
 iterated, so is the uncurrying."
@@ -98,14 +299,12 @@ iterated, so is the uncurrying."
                       (rec context term)))
                (unit
                 (terminal (stlc-ctx-to-mu context)))
-               ((left term)
-                (let ((tott (ttype tterm)))
-                  (comp (->left (mcar tott) (mcadr tott))
-                        (rec context term))))
-               ((right term)
-                (let ((tott (ttype tterm)))
-                  (comp (->right (mcar tott) (mcadr tott))
-                        (rec context term))))
+               ((left rty term)
+                (comp (->left (ttype term) rty)
+                      (rec context term)))
+               ((right lty term)
+                (comp (->right lty (ttype term))
+                      (rec context term)))
                ((case-on on ltm rtm)
                 (let ((mcartoon  (mcar (ttype on)))
                       (mcadrtoon (mcadr (ttype on)))
@@ -141,7 +340,9 @@ iterated, so is the uncurrying."
                                      (mapcar #'(lambda (x) (rec context x)) term)
                                      :from-end t)))))
                ((index pos)
-                (stlc-ctx-proj context pos)))))
+                (stlc-ctx-proj context pos))
+               (err
+                (error "Not meant for the compiler")))))
     (cond ((not (well-defp context tterm))
            (error "not a well-defined ~A in said ~A" tterm context))
           ((typep (type-of-term-w-fun context tterm) 'fun-type)
@@ -222,6 +423,11 @@ LAMBDA> (stlc-ctx-to-mu (list so1 (fun-to-hom (fun-type geb-bool:bool geb-bool:b
 ```"
   (mvfoldr #'prod (mapcar #'fun-to-hom context) so1))
 
+(defun stlc-ctx-maybe (context)
+  "Takes a context seen as product of appropriate [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]
+and iteratively applies Maybe to its elements."
+  (mvfoldr #'prod (mapcar (lambda (x) (maybe-obj-comp x)) context) so1))
+
 (-> so-hom (substobj substobj) (or t substobj))
 (defun so-hom (dom cod)
   "Computes the hom-object of two [SUBSTMORPH]s"

src/specs/lambda-printer.lisp

@@ -17,3 +17,4 @@
 (easy-printer lamb)
 (easy-printer app)
 (easy-printer index)
+(easy-printer err)

src/specs/lambda.lisp

@@ -10,8 +10,7 @@ unit types as well as coproduct, product, and function types."))
   "Type of untyped terms of [STLC][type]. Each class of a term has a slot for a type,
 which can be filled by auxillary functions or by user. Types are
 represented as [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]."
-  '(or absurd unit left right case-on pair fst snd lamb app index))
-
+  '(or absurd unit left right case-on pair fst snd lamb app index err))
 
 ;; New defgenerics
 
@@ -537,4 +536,23 @@ type-theoretic notation."))
   (values
    (make-instance 'index :pos pos :ttype ttype)))
 
+(defclass err (<stlc>)
+  ((ttype :initarg :ttype
+          :initform nil
+          :accessor ttype
+          :documentation ""))
+  (:documentation
+   "An error term of a type supplied by the user. The formal grammar of
+[ERR][class] is
+```lisp
+(err ttype)
+```
+The intended semantics are as follows: [ERR][class] 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][generic-function] a possibly empty accessor."))
 
+(-> err (cat-obj) err)
+(defun err (ttype)
+  (values
+   (make-instance 'err :ttype ttype)))