This is an experiment to see what the differences are between defining NonNegativeInteger? (NNI) as a SubDomain of Integer, versus defining it simply based on Integer itself.

The surprizing conclusion is that the latter definition of NNI produces nearly identical code as the first definition except for the now required definitions of coerce:%->Integer and convert:Integer->%, but without the extra CategoryFrame datastructure. This would seem to confirm that the SubDomain construct does not have any great advantages over the more direct definition.

First, NNI the usual way:

(1) -> <spad>

)abbrev domain NNI NonNegativeInteger
++ Description: \spadtype{NonNegativeInteger} provides functions for non
++   negative integers.
NonNegativeInteger: Join(OrderedAbelianMonoidSup,Monoid) with
            _quo : (%,%) -> %
              ++ a quo b returns the quotient of \spad{a} and b, forgetting
              ++ the remainder.
            _rem : (%,%) -> %
              ++ a rem b returns the remainder of \spad{a} and b.
            gcd  : (%,%) -> %
              ++ gcd(a,b) computes the greatest common divisor of two
              ++ non negative integers \spad{a} and b.
            divide: (%,%) -> Record(quotient:%,remainder:%)
              ++ divide(a,b) returns a record containing both
              ++ remainder and quotient.
            _exquo: (%,%) -> Union(%,"failed")
              ++ exquo(a,b) returns the quotient of \spad{a} and b, or "failed"
              ++ if b is zero or \spad{a} rem b is zero.
            shift: (%, Integer) -> %
              ++ shift(a,i) shift \spad{a} by i bits.
            random   : % -> %
              ++ random(n) returns a random integer from 0 to \spad{n-1}.
            CommutativeStar
              ++ CommutativeStar means multiplication is commutative : \spad{x*y = y*x}.

  == SubDomain(Integer,#1 >= 0) add
      x,y:%
      sup(x,y) == MAX(x,y)$Lisp
      shift(x:%, n:Integer):% == ASH(x,n)$Lisp
      subtractIfCan(x, y) ==
        c:Integer := (x pretend Integer) - (y pretend Integer)
        c < 0 => "failed"
        c pretend %</spad>

Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4255648489146469329-25px001.spad
      using old system compiler.
   NNI abbreviates domain NonNegativeInteger 
------------------------------------------------------------------------
   initializing NRLIB NNI for NonNegativeInteger 
   compiling into NRLIB NNI 
   compiling exported sup : (%,%) -> %
      NNI;sup;3%;1 is replaced by MAX 

;;;     ***       |NNI;sup;3%;1| REDEFINED
Time: 0 SEC.

   compiling exported shift : (%,Integer) -> %
      NNI;shift;%I%;2 is replaced by ASH 
Time: 0 SEC.

   compiling exported subtractIfCan : (%,%) -> Union(%,failed)
Time: 0 SEC.

(time taken in buildFunctor:  674)

;;;     ***       |NonNegativeInteger| REDEFINED

;;;     ***       |NonNegativeInteger| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor NonNegativeInteger
      Time: 0 seconds

--------------non extending category----------------------
.. NonNegativeInteger of cat 
(|Join| (|OrderedAbelianMonoidSup|) (|Monoid|)
        (CATEGORY |domain| (SIGNATURE |quo| (% % %)) (SIGNATURE |rem| (% % %))
         (SIGNATURE |gcd| (% % %))
         (SIGNATURE |divide|
          ((|Record| (|:| |quotient| %) (|:| |remainder| %)) % %))
         (SIGNATURE |exquo| ((|Union| % "failed") % %))
         (SIGNATURE |shift| (% % (|Integer|))) (SIGNATURE |random| (% %))
         (ATTRIBUTE (|CommutativeStar|))))   has no 
(|IntegerNumberSystem|)    finalizing NRLIB NNI 
   Processing NonNegativeInteger for Browser database:
--------constructor---------
--------(quo (% % %))---------
--------(rem (% % %))---------
--------(gcd (% % %))---------
--------(divide ((Record (: quotient %) (: remainder %)) % %))---------
--------(exquo ((Union % failed) % %))---------
--------(shift (% % (Integer)))---------
--------(random (% %))---------
--------constructor---------
--->/usr/local/lib/fricas/target/x86_64-linux-gnu/../../src/algebra/NNI.spad-->NonNegativeInteger(): Spurious comments: CommutativeStar means multiplication is commutative : \spad{x*y = y*x}.
; compiling file "/var/aw/var/LatexWiki/NNI.NRLIB/NNI.lsp" (written 05 DEC 2024 08:20:18 AM):

; wrote /var/aw/var/LatexWiki/NNI.NRLIB/NNI.fasl
; compilation finished in 0:00:00.012
------------------------------------------------------------------------
   NonNegativeInteger is now explicitly exposed in frame initial 
   NonNegativeInteger will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/NNI.NRLIB/NNI

x1:NNI:=1$NNI

(1)

y1:NNI:=2$NNI

(2)

z1:NNI:=(x1 + y1)$NNI

(3)

z1::INT

(4)

subtractIfCan(y1,x1)$NNI

(5)

(4::INT)::NNI

Compiling function G16 with type Integer -> Boolean

(6)

((-1)::INT)::NNI

   Cannot convert the value from type Integer to NonNegativeInteger .

Now write NNI without using SubDomain:

)abbrev domain NNI2 NonNegativeInteger2
++ Description: \spadtype{NonNegativeInteger} provides functions for non
++   negative integers.
NonNegativeInteger2: Join(OrderedAbelianMonoidSup,Monoid,CoercibleTo(Integer)) with
            _quo : (%,%) -> %
              ++ a quo b returns the quotient of \spad{a} and b, forgetting
              ++ the remainder.
            _rem : (%,%) -> %
              ++ a rem b returns the remainder of \spad{a} and b.
            gcd  : (%,%) -> %
              ++ gcd(a,b) computes the greatest common divisor of two
              ++ non negative integers \spad{a} and b.
            divide: (%,%) -> Record(quotient:%,remainder:%)
              ++ divide(a,b) returns a record containing both
              ++ remainder and quotient.
            _exquo: (%,%) -> Union(%,"failed")
              ++ exquo(a,b) returns the quotient of \spad{a} and b, or "failed"
              ++ if b is zero or \spad{a} rem b is zero.
            shift: (%, Integer) -> %
              ++ shift(a,i) shift \spad{a} by i bits.
            random   : % -> %
              ++ random(n) returns a random integer from 0 to \spad{n-1}.
            CommutativeStar
              ++ commutative("*") means multiplication is commutative : \spad{x*y = y*x}.
            convert: Integer -> %

  == Integer add

      sup(x:%,y:%) == MAX(x,y)$Lisp
      shift(x:%, n:Integer):% == ASH(x,n)$Lisp
      subtractIfCan(x, y) ==
        c:Integer := (x pretend Integer) - (y pretend Integer)
        c < 0 => "failed"
        c pretend %
      coerce(x:%):Integer == x pretend Integer
      convert(x:Integer):% ==
        x >= 0 => x pretend %
        error(["Cannot convert from type Integer to NonNegativeInteger for value",
         string(x)$String])

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2203784355024913414-25px003.spad
      using old system compiler.
   NNI2 abbreviates domain NonNegativeInteger2 
------------------------------------------------------------------------
   initializing NRLIB NNI2 for NonNegativeInteger2 
   compiling into NRLIB NNI2 
   compiling exported sup : (%,%) -> %
      NNI2;sup;3%;1 is replaced by MAX 
Time: 0 SEC.

   compiling exported shift : (%,Integer) -> %
      NNI2;shift;%I%;2 is replaced by ASH 
Time: 0 SEC.

   compiling exported subtractIfCan : (%,%) -> Union(%,failed)
Time: 0 SEC.

   compiling exported coerce : % -> Integer
      NNI2;coerce;%I;4 is replaced by x 
Time: 0 SEC.

   compiling exported convert : Integer -> %
(compiling call to error  ((construct Cannot convert from type Integer to NonNegativeInteger for value ((Sel (String) string) x))))
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |NonNegativeInteger2| REDEFINED

;;;     ***       |NonNegativeInteger2| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor NonNegativeInteger2
      Time: 0 seconds

--------------non extending category----------------------
.. NonNegativeInteger2 of cat 
(|Join| (|OrderedAbelianMonoidSup|) (|Monoid|) (|CoercibleTo| (|Integer|))
        (CATEGORY |domain| (SIGNATURE |quo| (% % %)) (SIGNATURE |rem| (% % %))
         (SIGNATURE |gcd| (% % %))
         (SIGNATURE |divide|
          ((|Record| (|:| |quotient| %) (|:| |remainder| %)) % %))
         (SIGNATURE |exquo| ((|Union| % "failed") % %))
         (SIGNATURE |shift| (% % (|Integer|))) (SIGNATURE |random| (% %))
         (ATTRIBUTE (|CommutativeStar|)) (SIGNATURE |convert| (% (|Integer|)))))   has no 
(|IntegerNumberSystem|)    finalizing NRLIB NNI2 
   Processing NonNegativeInteger2 for Browser database:
--------constructor---------
--------(quo (% % %))---------
--------(rem (% % %))---------
--------(gcd (% % %))---------
--------(divide ((Record (: quotient %) (: remainder %)) % %))---------
--------(exquo ((Union % failed) % %))---------
--------(shift (% % (Integer)))---------
--------(random (% %))---------
--->-->NonNegativeInteger2((convert (% (Integer)))): Not documented!!!!
--------constructor---------
--->-->NonNegativeInteger2(): Spurious comments: commutative(\spad{"*"}) means multiplication is commutative : \spad{x*y = y*x}.
; compiling file "/var/aw/var/LatexWiki/NNI2.NRLIB/NNI2.lsp" (written 05 DEC 2024 08:20:18 AM):

; wrote /var/aw/var/LatexWiki/NNI2.NRLIB/NNI2.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   NonNegativeInteger2 is now explicitly exposed in frame initial 
   NonNegativeInteger2 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/NNI2.NRLIB/NNI2

The behaviour is identical to NNI

x2:NNI2:=1$NNI2

(7)

y2:NNI2:=2$NNI2

(8)

z2:NNI2:=(x2+y2)$NNI2

(9)

z2::INT

(10)

subtractIfCan(y2,x2)$NNI2

(11)

(4::INT)::NNI2

(12)

((-1)::INT)::NNI2

   >> Error detected within library code:
   "Cannot convert from type Integer to NonNegativeInteger for value""-1"

The generated lisp code for NNI is:

)lisp (system "cat < /var/zope2/var/LatexWiki/NNI.NRLIB/NNI.lsp | tee /tmp/NNI.lsp")

   Your user access level is compiler and this command is therefore not
      available. See the )set userlevel command for more information.

Compared NNI (-) to NNI2 (+):

)lisp (system "cat < /var/zope2/var/LatexWiki/NNI2.NRLIB/NNI2.lsp | diff -au /tmp/NNI.lsp -")

   Your user access level is compiler and this command is therefore not
      available. See the )set userlevel command for more information.

SubDomain written in Aldor:

#include "axiom.as"
SubSetDom(X:Type, E:X->Boolean):
with {
  convert: X -> %;
  coerce: % -> X;
} == X add {
  coerce(x:%):X == x pretend X;
  convert(x:X):% == {
    E(x) => x pretend %;
    error("Cannot convert");
  }
}

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3345325303575885968-25px007.as
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3345325303575885968-25px007.as", line 1: 
#include "axiom.as"
^
[L1 C1] #1 (Error) Could not open file `axiom.as'.

   The )library system command was not called after compilation.

)sh SubSetDom

   The )show system command is used to display information about types 
      or partial types. For example, )show Integer will show 
      information about Integer .

      SubSetDom is not the name of a known type constructor. If you 
      want to see information about any operations named SubSetDom , 
      issue
                        )display operations SubSetDom 

)set functions compile on

Test the new subdomain.

E:Integer->Boolean

E(z) == (z >= 0)

E(3)

Compiling function E with type Integer -> Boolean

(13)

)sh SubSetDom(Integer, E)

   The )show system command is used to display information about types 
      or partial types. For example, )show Integer will show 
      information about Integer .

      SubSetDom is not the name of a known type constructor. If you 
      want to see information about any operations named SubSetDom , 
      issue
                        )display operations SubSetDom 

      Integer is not the name of a known type constructor. If you want 
      to see information about any operations named Integer , issue
                         )display operations Integer 

      E is not the name of a known type constructor. If you want to see
      information about any operations named E , issue
                            )display operations E 
N:SubSetDom(Integer, E)

   There are no library operations named SubSetDom 
      Use HyperDoc Browse or issue
                             )what op SubSetDom
      to learn if there is any operation containing " SubSetDom " in 
      its name.

   Cannot find a definition or applicable library operation named 
      SubSetDom with argument type(s) 
                                    Type
                              FunctionCalled(E)

      Perhaps you should use "@" to indicate the required return type, 
      or "$" to specify which version of the function you need.

Now define NNI the using the new SubSetDom?:

For some unknown reason this fails:

#include "axiom.as"
#pile
NNI3: Join(OrderedAbelianMonoidSup,Monoid, CoercibleTo(Integer))
   with
     convert: Integer -> %
   == SubSetDom(Integer, (z:Integer):Boolean +-> (z >= 0)) add

      sup(x:%,y:%):% ==
         x>y => x
         y

      subtractIfCan(x:%, y:%):Union(ok:%,failed:'failed') ==
         c:Integer == (x pretend Integer) - (y pretend Integer)
         c < 0 => return [failed]
         [c pretend %]

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3694095911335604383-25px010.as
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3694095911335604383-25px010.as", line 1: 
#include "axiom.as"
^
[L1 C1] #1 (Error) Could not open file `axiom.as'.

   The )library system command was not called after compilation.

But this works:

#include "axiom.as"
#pile
NNI4: Join(OrderedAbelianMonoidSup,Monoid, CoercibleTo(Integer))
   with
     convert: Integer -> %
-- == SubSetDom(Integer, (z:Integer):Boolean +-> (z >= 0)) add
   == Integer add

      coerce(x:%):Integer == x pretend Integer;

      convert(x:Integer):% ==
         x>=0 => return x pretend %
         error "Cannot convert"

      sup(x:%,y:%):% ==
         x>y => x
         y

      subtractIfCan(x:%, y:%):Union(ok:%,failed:'failed') ==
         c:Integer == (x pretend Integer) - (y pretend Integer)
         c < 0 => return [failed]
         [c pretend %]

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/84397582143168417-25px011.as
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/84397582143168417-25px011.as", line 1: 
#include "axiom.as"
^
[L1 C1] #1 (Error) Could not open file `axiom.as'.

   The )library system command was not called after compilation.

)set message bottomup on

   Your user access level is compiler and this set option is therefore 
      not available. See the )set userlevel command for more 
      information.
x4:NNI4:=1$NNI4

   NNI4 is not a valid type.

#pile
#include "axiom"
--)abbrev package TEST test
NNI ==> NonNegativeInteger2
test(): with
    main: ()-> NNI
  == add
    n1:NNI:=1
    n2:NNI:=2
    main():NNI == n1-n2

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5451681632571730514-25px013.as
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5451681632571730514-25px013.as", line 2: 
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.

   The )library system command was not called after compilation.

)show TEST

   The )show system command is used to display information about types 
      or partial types. For example, )show Integer will show 
      information about Integer .

      TEST is not the name of a known type constructor. If you want to 
      see information about any operations named TEST , issue
                          )display operations TEST

main()

   There are no library operations named main 
      Use HyperDoc Browse or issue
                                )what op main
      to learn if there is any operation containing " main " in its 
      name.

   Cannot find a no-argument definition or library operation named main
      .