From 68f084deb620dbcb8d6ae7ee51bb5cdf6d1ef803 Mon Sep 17 00:00:00 2001 From: Artem Gureev Date: Tue, 30 May 2023 14:21:20 +0800 Subject: [PATCH] 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 | 25 +++- src/lambda/package.lisp | 1 + src/lambda/trans.lisp | 230 ++++++++++++++++++++++++++++++++-- src/specs/lambda-printer.lisp | 1 + src/specs/lambda.lisp | 22 +++- src/specs/package.lisp | 5 + test/lambda-trans.lisp | 40 ++++++ 7 files changed, 308 insertions(+), 16 deletions(-) diff --git a/src/lambda/lambda.lisp b/src/lambda/lambda.lisp index 8a4da47cb..c3e5d9f93 100644 --- a/src/lambda/lambda.lisp +++ b/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))))) diff --git a/src/lambda/package.lisp b/src/lambda/package.lisp index ced7cdf71..8d54a5338 100644 --- a/src/lambda/package.lisp +++ b/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))) diff --git a/src/lambda/trans.lisp b/src/lambda/trans.lisp index c433523dd..bf7d0c643 100644 --- a/src/lambda/trans.lisp +++ b/src/lambda/trans.lisp @@ -47,6 +47,207 @@ calling me" (defmethod empty ((class (eql (find-class 'list)))) nil) (defmethod to-cat (context (tterm )) + "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 )) + "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 )) "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" diff --git a/src/specs/lambda-printer.lisp b/src/specs/lambda-printer.lisp index 53202022f..fdc1b71bb 100644 --- a/src/specs/lambda-printer.lisp +++ b/src/specs/lambda-printer.lisp @@ -17,3 +17,4 @@ (easy-printer lamb) (easy-printer app) (easy-printer index) +(easy-printer err) diff --git a/src/specs/lambda.lisp b/src/specs/lambda.lisp index 1b0a3d3e9..1259fb390 100644 --- a/src/specs/lambda.lisp +++ b/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 () + ((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))) diff --git a/src/specs/package.lisp b/src/specs/package.lisp index fdf43a74c..b1e060dd5 100644 --- a/src/specs/package.lisp +++ b/src/specs/package.lisp @@ -158,6 +158,7 @@ constructors" (lamb pax:class) (app pax:class) (index pax:class) + (err pax:class) (absurd pax:function) (unit pax:function) @@ -170,6 +171,7 @@ constructors" (lamb pax:function) (app pax:function) (index pax:function) + (err pax:function) "Accessors of [ABSURD][class]" @@ -223,6 +225,9 @@ constructors" (pos (pax:method () (index))) (ttype (pax:method () (index))) + "Accessors of [ERR][class]" + (ttype (pax:method () (err))) + (tcod pax:generic-function) (tdom pax:generic-function) (term pax:generic-function) diff --git a/test/lambda-trans.lisp b/test/lambda-trans.lisp index 8029514ff..78ecef022 100644 --- a/test/lambda-trans.lisp +++ b/test/lambda-trans.lisp @@ -37,6 +37,26 @@ (def bool-id (lambda:lamb (list (coprod so1 so1)) (geb.lambda:index 0))) +(def case-error-left + (lambda:case-on (lambda:left so1 (lambda:unit)) + (lambda:err so1) + (lambda:unit))) + +(def case-error-right + (lambda:case-on (lambda:left so1 (lambda:unit)) + (lambda:unit) + (lambda:err so1))) + +(def case-error-top + (lambda:case-on (lambda:err (coprod so1 so1)) + (lambda:unit) + (lambda:unit))) + +(def context-dependent-case + (lambda:case-on (lambda:index 0) + (lambda:err so1) + (lambda:unit))) + (def issue-58-circuit (to-circuit (lambda:case-on @@ -103,6 +123,26 @@ (is equalp #*0 (gapply (to-bitc proper-not) #*1)) (is equalp #*1 (gapply (to-bitc proper-not) #*0))) +(define-test error-handling-case :parent lambda.trans-eval + (is obj-equalp (left so1) (gapply (to-cat nil case-error-left) + (list so1))) + (is obj-equalp (right so1) (gapply (to-cat nil case-error-right) + (list so1))) + (is obj-equalp (left so1) (gapply (to-cat nil case-error-top) + (list so1))) + (is obj-equalp (left so1) (gapply (to-cat (list (coprod so1 so1)) + context-dependent-case) + (list (right + (left + (right so1))) + so1))) + (is obj-equalp (right so1) (gapply (to-cat (list (coprod so1 so1)) + context-dependent-case) + (list (right + (right + (right so1))) + so1)))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Compile checked term tests ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;