help links subscribe changes refresh edit

	SandBox
SandBoxCachedFunction ←	↑	→ SandBoxCategoryTerms

SandBoxCategories

Edit detail for SandBoxCategories revision 1 of 1

	1
Editor: Time: 2007/11/18 17:57:08 GMT-8
Note: update tests

changed:
-
This page was renamed to AnonymousCategories. You can delete this one if no longer needed.

Or click 'edit' or Add Comments to make further online tests here.

**On Aug 12, 2007 6:35 PM Weiss, Juergen wrote:**

I found the old document about type equivalence in Scratchpad. It's:
*A New Algebra System, May, 29 th 1984, James H Davenport*. I have only
found a paper version. Maybe someone has an online version.

It states that:

1. Two named types are only equivalent if the names are the same.

2. Anonymous types are equivalent when stucturally equivalent

3. An anonymous type is never equivalent to a named type.

So following 1::

  t1 == List Term
  t2 == List Term
  x : t1
  y : t2
  y := x

is not supposed to work,
![t1 and t2 should be treated as different types]
\begin{spad}
)abbrev package TEST test
test(): with
    main:()->Integer
  == add
    main() ==
      t1:IntegerNumberSystem == Integer
      t2:IntegerNumberSystem == Integer
      x : t1
      x := 1$t1
      y : t2
      y := x
\end{spad}
There should be a compile error above.
\begin{axiom}
main()
\end{axiom}

but following 2::

  x : List Term
  y : List Term
  y := x

is ok,
\begin{spad}
)abbrev package TEST test2
test2(): with
    main2:()->Integer
  == add
    main2()==
      x : Integer
      x := 1
      y : Integer
      y := x
\end{spad}

\begin{axiom}
main2()
\end{axiom}

also
\begin{spad}
)abbrev package TEST test4
test4(): with
    main4:()->Integer
  == add
    main4():Integer ==
      t1():IntegerNumberSystem == Integer
      x : t1
      x := 1$t1
      y : t1
      y := x
      1
\end{spad}
This compiles ok but there is a run-time error. Why?
\begin{axiom}
main4()
\end{axiom}

and following 3::

  t == List Term
  x : List Term
  y : t
  y := x

is not supposed to work as well
\begin{spad}
)abbrev package TEST test3
test3(): with
    main3:()->Integer
  == add
    main3() ==
      t:IntegerNumberSystem == Integer
      x : Integer
      x := 1
      y : t
      y := x
\end{spad}

There should produce a compile error above.
\begin{axiom}
main3()
\end{axiom}


All examples are taken from the paper.

I am not sure how much of this design is preserved in the current
system. But without having had an intense look at the examples,
I got the impression, that they follow the rules above.

Regards

Juergen Weiss

From wyscc Mon Aug 13 01:35:25 -0500 2007
From: wyscc
Date: Mon, 13 Aug 2007 01:35:25 -0500
Subject: test
Message-ID: <20070813013525-0500@wiki.axiom-developer.org>

The failure above is not convincing, since the spad code did not compile. It's not clear where the failure lies. For example, in Test4, the compiler message says |t1| is not defined. A slight modification causes a different error (for example adding () after t1 in test4):

\begin{spad}
)abbrev package TESTFIVE test5
test5(): with
    main5:()->Integer
  == add
    main5():Integer ==
      t1():IntegerNumberSystem == Integer 
      x : t1()
      x := 1$t1()
      y : t1()
      y := x
      1$Integer
\end{spad}

\begin{axiom}
main5()
\end{axiom}

The better way to test equivalence of domains is to actually construct new domains.

\begin{spad}
)abbrev domain TEEONE tee1
tee1():IntegerNumberSystem == Integer

)abbrev domain TEETWO tee2
tee2():IntegerNumberSystem == Integer 

)abbrev package TESTSIX test6
test6(): with
    main6:()->Integer
  == add
    main6():Integer ==
      x : tee1
      x := 1$tee1
      y : tee1
      y := x
      1$Integer
\end{spad}

\begin{axiom}
main6()
\end{axiom}

\begin{spad}
)abbrev package TESTSEV test7
test7(): with
    foo7:tee1 -> tee2
    main7:(tee1, tee2) -> tee2
  == add
    foo7(x) == 5$tee2
    main7(x,y) == foo7(x) + y 
\end{spad}

Would you have expected a compile error with test7?  This shows there is no automatic coercion in the compiler from Integer to tee2. 

\begin{spad}
)abbrev package TESTEGT test8
test8(): with
    foo8:tee1 -> tee2
    main8:(tee1, tee2) -> tee2
  == add
    foo8(x) == 1$tee2 + 1$tee2 + 1$tee2 + 1$tee2 + 1$tee2
    main8(x,y) == foo8(x) + y 
\end{spad}

Note that tee2 does have a multiplicative unit without requiring a coercion from Integer!
So test8 compiles okay. Let's see this in action. 

\begin{axiom}
-- expects 6
main8(1$tee1, 1$tee2)
-- expects error
main8(1$tee2, 1$tee1)
-- expects error
main8(1$tee1, 1$tee1)
-- expects error
main8(1$tee2, 1$tee2)
\end{axiom}

So even the interpreter does not coerce tee1 into tee2. Guess the next three:

\begin{axiom}
main8(1$Integer, 1$Integer)
main8(2$tee1, 5$tee2)
main8(3::tee1, (2$tee1)::tee2)
\end{axiom}

The compiler would not recognize 5$tee2, but the interpreter has no problem coercing any integer automatically to tee1 or tee2. This shows Integer is very special for the interpreter, and not treated the same as tee1.

Let's see if we change the name of foo8 to 'convert' and make the converted value to be 4 instead of 5.

\begin{spad}
)abbrev package TESTNINE test9
test9(): with
    convert:tee1 -> tee2
    main9:(tee1, tee2) -> tee2
  == add
    convert(x) == 1$tee2 + 1$tee2 + 1$tee2 + 1$tee2
    main9(x,y) == convert(x) + y 
\end{spad}

test9 also compiles okay. Let's see this in action. Recall that there is a convert: tee1 -> tee2, but no coerce.

\begin{axiom}
-- expects 5
main9(1$tee1, 1$tee2)
-- expects error
main9(1$tee2, 1$tee1)
-- you make a guess :-)
main9(1$tee1, 1$tee1)
-- expects error
main9(1$tee2, 1$tee2)
-- now expecting 5
main9(1$Integer, 1$Integer)
\end{axiom}

Note 'convert' is not automatically used by the interpreter. Now let's change convert to coerce. Even though there is now a coerce, tee1 is not declared to be CoercibleTo(tee2)  (to do so would have made the two domain constructors different in structure). We use a value 1 this time for coerce.


\begin{spad}
)abbrev package TESTTEN test10
test10(): with
    coerce:tee1 -> tee2
    main10:(tee1, tee2) -> tee2
  == add
    coerce(x) == 1$tee2
    main10(x,y) == coerce(x) + y 
\end{spad}






\begin{axiom}
-- expects 2
main10(1$tee1, 1$tee2)
-- expects error
main10(1$tee2, 1$tee1)
-- you make a guess :-)
main10(1$tee1, 1$tee1)
-- expects error
main10(1$tee2, 1$tee2)
-- you know this one
main10(1$Integer, 1$Integer)
-- make a guess
tee1 has CoercibleTo(tee2)
\end{axiom}

Now '1\$tee1' is automatically coerced to '1\$tee2' even though tee1 does not have CoercibleTo(tee2), but this is the interpreter!



The next thing to do would be to test equivalence of categories. Some other time.

This page was renamed to AnonymousCategories?. You can delete this one if no longer needed.

Or click edit or Add Comments to make further online tests here.

On Aug 12, 2007 6:35 PM Weiss, Juergen wrote:

I found the old document about type equivalence in Scratchpad. It's: A New Algebra System, May, 29 th 1984, James H Davenport. I have only found a paper version. Maybe someone has an online version.

It states that:

Two named types are only equivalent if the names are the same.
Anonymous types are equivalent when stucturally equivalent
An anonymous type is never equivalent to a named type.

So following 1:

  t1 == List Term
  t2 == List Term
  x : t1
  y : t2
  y := x

is not supposed to work, [t1 and t2 should be treated as different types]

spad

)abbrev package TEST test
test(): with
    main:()->Integer
  == add
    main() ==
      t1:IntegerNumberSystem == Integer
      t2:IntegerNumberSystem == Integer
      x : t1
      x := 1$t1
      y : t2
      y := x

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4406049181591081329-25px001.spad
      using old system compiler.
   TEST abbreviates package test 
------------------------------------------------------------------------
   initializing NRLIB TEST for test 
   compiling into NRLIB TEST 
   compiling exported main : () -> Integer
   Semantic Errors: 
      [1] main:  +-> is not a known type

****** comp fails at level 3 with expression: ******
error in function main 

(SEQ (DEF (|t1|) ((|IntegerNumberSystem|)) (NIL) (|Integer|))
     (DEF (|t2|) ((|IntegerNumberSystem|)) (NIL) (|Integer|)) (|:| |x| |t1|)
     (|:=| |x| | << | (|Sel| |t1| 1) | >> |) (|:| |y| |t2|)
     (|exit| 1 (|:=| |y| |x|)))
****** level 3  ******
$x:= (Sel t1 (One))
$m:= t1
$f:=
((((|x| #) (|t2| #) (|t1| #) (|main| #) ...)))

   >> Apparent user error:
   NoValueMode
    is an unknown mode

There should be a compile error above.

fricas

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
      .

but following 2:

  x : List Term
  y : List Term
  y := x

is ok,

spad

)abbrev package TEST test2
test2(): with
    main2:()->Integer
  == add
    main2()==
      x : Integer
      x := 1
      y : Integer
      y := x

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3154192227704798176-25px003.spad
      using old system compiler.
   TEST abbreviates package test2 
------------------------------------------------------------------------
   initializing NRLIB TEST for test2 
   compiling into NRLIB TEST 
   compiling exported main2 : () -> Integer
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |test2| REDEFINED

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

   Cumulative Statistics for Constructor test2
      Time: 0 seconds

   finalizing NRLIB TEST 
   Processing test2 for Browser database:
--->-->test2(constructor): Not documented!!!!
--->-->test2((main2 ((Integer)))): Not documented!!!!
--->-->test2(): Missing Description
; compiling file "/var/aw/var/LatexWiki/TEST.NRLIB/TEST.lsp" (written 04 APR 2022 05:49:43 PM):

; /var/aw/var/LatexWiki/TEST.NRLIB/TEST.fasl written
; compilation finished in 0:00:00.010
------------------------------------------------------------------------
   test2 is now explicitly exposed in frame initial 
   test2 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/TEST.NRLIB/TEST

fricas

main2()

$\label{eq1}1$

(1)

Type: PositiveInteger?

also

spad

)abbrev package TEST test4
test4(): with
    main4:()->Integer
  == add
    main4():Integer ==
      t1():IntegerNumberSystem == Integer
      x : t1
      x := 1$t1
      y : t1
      y := x
      1

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/346730625682591668-25px005.spad
      using old system compiler.
   TEST abbreviates package test4 
------------------------------------------------------------------------
   initializing NRLIB TEST for test4 
   compiling into NRLIB TEST 
   compiling exported main4 : () -> Integer
   Semantic Errors: 
      [1] main4:  +-> is not a known type

****** comp fails at level 3 with expression: ******
error in function main4 

(SEQ (DEF (|t1|) ((|IntegerNumberSystem|)) (NIL) (|Integer|)) (|:| |x| |t1|)
     (|:=| |x| | << | (|Sel| |t1| 1) | >> |) (|:| |y| |t1|) (|:=| |y| |x|)
     (|exit| 1 1))
****** level 3  ******
$x:= (Sel t1 (One))
$m:= t1
$f:=
((((|x| #) (|t1| #) (|main4| #) (|$DomainsInScope| # # #) ...)))

   >> Apparent user error:
   NoValueMode
    is an unknown mode

This compiles ok but there is a run-time error. Why?

fricas

main4()

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

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

and following 3:

  t == List Term
  x : List Term
  y : t
  y := x

is not supposed to work as well

spad

)abbrev package TEST test3
test3(): with
    main3:()->Integer
  == add
    main3() ==
      t:IntegerNumberSystem == Integer
      x : Integer
      x := 1
      y : t
      y := x

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2232261183027663296-25px007.spad
      using old system compiler.
   TEST abbreviates package test3 
------------------------------------------------------------------------
   initializing NRLIB TEST for test3 
   compiling into NRLIB TEST 
   compiling exported main3 : () -> Integer
   Semantic Errors: 
      [1] main3:  +-> is not a known type

****** comp fails at level 3 with expression: ******
error in function main3 

(SEQ (DEF (|t|) ((|IntegerNumberSystem|)) (NIL) (|Integer|))
     (|:| |x| (|Integer|)) (|:=| |x| 1) (|:| |y| |t|)
     (|exit| 1 | << | (|:=| |y| |x|) | >> |))
****** level 3  ******
$x:= (:= y x)
$m:= (Integer)
$f:=
((((|y| #) (|x| # #) (|t| #) (|main3| #) ...)))

   >> Apparent user error:
   CANNOT ASSIGN: x
   OF MODE: (Integer)
   TO: y
   OF MODE: t

There should produce a compile error above.

fricas

main3()

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

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

All examples are taken from the paper.

I am not sure how much of this design is preserved in the current system. But without having had an intense look at the examples, I got the impression, that they follow the rules above.

Regards

Juergen Weiss

test --wyscc, Mon, 13 Aug 2007 01:35:25 -0500 reply

The failure above is not convincing, since the spad code did not compile. It's not clear where the failure lies. For example, in Test4, the compiler message says |t1| is not defined. A slight modification causes a different error (for example adding () after t1 in test4):

spad

)abbrev package TESTFIVE test5
test5(): with
    main5:()->Integer
  == add
    main5():Integer ==
      t1():IntegerNumberSystem == Integer 
      x : t1()
      x := 1$t1()
      y : t1()
      y := x
      1$Integer

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3611641870102941622-25px009.spad
      using old system compiler.
   TESTFIVE abbreviates package test5 
------------------------------------------------------------------------
   initializing NRLIB TESTFIVE for test5 
   compiling into NRLIB TESTFIVE 
   compiling exported main5 : () -> Integer
   Internal Error
   Error while instantiating type t1

fricas

main5()

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

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

The better way to test equivalence of domains is to actually construct new domains.

spad

)abbrev domain TEEONE tee1
tee1():IntegerNumberSystem == Integer

)abbrev domain TEETWO tee2
tee2():IntegerNumberSystem == Integer 

)abbrev package TESTSIX test6
test6(): with
    main6:()->Integer
  == add
    main6():Integer ==
      x : tee1
      x := 1$tee1
      y : tee1
      y := x
      1$Integer

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5058510425788394140-25px011.spad
      using old system compiler.
   TEEONE abbreviates domain tee1 
------------------------------------------------------------------------
   initializing NRLIB TEEONE for tee1 
   compiling into NRLIB TEEONE 
(time taken in buildFunctor:  10)

;;;     ***       |tee1| REDEFINED

;;;     ***       |tee1| REDEFINED
Time: 0.01 SEC.

   Cumulative Statistics for Constructor tee1
      Time: 0.01 seconds

--------------non extending category----------------------
.. tee1 of cat 
(|IntegerNumberSystem|)   has no 
(|LinearlyExplicitOver| (|Integer|))    finalizing NRLIB TEEONE 
   Processing tee1 for Browser database:
--->-->tee1(): Missing Description
; compiling file "/var/aw/var/LatexWiki/TEEONE.NRLIB/TEEONE.lsp" (written 04 APR 2022 05:49:44 PM):

; /var/aw/var/LatexWiki/TEEONE.NRLIB/TEEONE.fasl written
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
   tee1 is now explicitly exposed in frame initial 
   tee1 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/TEEONE.NRLIB/TEEONE

   TEETWO abbreviates domain tee2 
------------------------------------------------------------------------
   initializing NRLIB TEETWO for tee2 
   compiling into NRLIB TEETWO 
(time taken in buildFunctor:  0)

;;;     ***       |tee2| REDEFINED

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

   Cumulative Statistics for Constructor tee2
      Time: 0 seconds

--------------non extending category----------------------
.. tee2 of cat 
(|IntegerNumberSystem|)   has no 
(|LinearlyExplicitOver| (|Integer|))    finalizing NRLIB TEETWO 
   Processing tee2 for Browser database:
--->-->tee2(): Missing Description
; compiling file "/var/aw/var/LatexWiki/TEETWO.NRLIB/TEETWO.lsp" (written 04 APR 2022 05:49:44 PM):

; /var/aw/var/LatexWiki/TEETWO.NRLIB/TEETWO.fasl written
; compilation finished in 0:00:00.007
------------------------------------------------------------------------
   tee2 is now explicitly exposed in frame initial 
   tee2 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/TEETWO.NRLIB/TEETWO

   TESTSIX abbreviates package test6 
------------------------------------------------------------------------
   initializing NRLIB TESTSIX for test6 
   compiling into NRLIB TESTSIX 
   compiling exported main6 : () -> Integer
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |test6| REDEFINED

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

   Cumulative Statistics for Constructor test6
      Time: 0 seconds

   finalizing NRLIB TESTSIX 
   Processing test6 for Browser database:
--->-->test6(constructor): Not documented!!!!
--->-->test6((main6 ((Integer)))): Not documented!!!!
--->-->test6(): Missing Description
; compiling file "/var/aw/var/LatexWiki/TESTSIX.NRLIB/TESTSIX.lsp" (written 04 APR 2022 05:49:44 PM):

; /var/aw/var/LatexWiki/TESTSIX.NRLIB/TESTSIX.fasl written
; compilation finished in 0:00:00.007
------------------------------------------------------------------------
   test6 is now explicitly exposed in frame initial 
   test6 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/TESTSIX.NRLIB/TESTSIX

fricas

main6()

$\label{eq2}1$

(2)

Type: PositiveInteger?

spad

)abbrev package TESTSEV test7
test7(): with
    foo7:tee1 -> tee2
    main7:(tee1, tee2) -> tee2
  == add
    foo7(x) == 5$tee2
    main7(x,y) == foo7(x) + y

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5193838586659015839-25px013.spad
      using old system compiler.
   TESTSEV abbreviates package test7 
------------------------------------------------------------------------
   initializing NRLIB TESTSEV for test7 
   compiling into NRLIB TESTSEV 
   compiling exported foo7 : tee1 -> tee2
****** comp fails at level 1 with expression: ******
error in function foo7 

((|Sel| (|tee2|) 5))
****** level 1  ******
$x:= (Sel (tee2) 5)
$m:= (tee2)
$f:=
((((|x| # #) (|main7| #) (|foo7| #) (|$DomainsInScope| # # #) ...)))

   >> Apparent user error:
   unspecified error

Would you have expected a compile error with test7? This shows there is no automatic coercion in the compiler from Integer to tee2.

spad

)abbrev package TESTEGT test8
test8(): with
    foo8:tee1 -> tee2
    main8:(tee1, tee2) -> tee2
  == add
    foo8(x) == 1$tee2 + 1$tee2 + 1$tee2 + 1$tee2 + 1$tee2
    main8(x,y) == foo8(x) + y

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2052161184486383446-25px014.spad
      using old system compiler.
   TESTEGT abbreviates package test8 
------------------------------------------------------------------------
   initializing NRLIB TESTEGT for test8 
   compiling into NRLIB TESTEGT 
   compiling exported foo8 : tee1 -> tee2
Time: 0 SEC.

   compiling exported main8 : (tee1,tee2) -> tee2
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |test8| REDEFINED

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

   Cumulative Statistics for Constructor test8
      Time: 0 seconds

   finalizing NRLIB TESTEGT 
   Processing test8 for Browser database:
--->-->test8(constructor): Not documented!!!!
--->-->test8((foo8 ((tee2) (tee1)))): Not documented!!!!
--->-->test8((main8 ((tee2) (tee1) (tee2)))): Not documented!!!!
--->-->test8(): Missing Description
; compiling file "/var/aw/var/LatexWiki/TESTEGT.NRLIB/TESTEGT.lsp" (written 04 APR 2022 05:49:44 PM):

; /var/aw/var/LatexWiki/TESTEGT.NRLIB/TESTEGT.fasl written
; compilation finished in 0:00:00.013
------------------------------------------------------------------------
   test8 is now explicitly exposed in frame initial 
   test8 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/TESTEGT.NRLIB/TESTEGT

Note that tee2 does have a multiplicative unit without requiring a coercion from Integer! So test8 compiles okay. Let's see this in action.

fricas

-- expects 6
main8(1$tee1, 1$tee2)

$\label{eq3}6$

(3)

Type: tee2

fricas

-- expects error
main8(1$tee2, 1$tee1)

   There are 1 exposed and 0 unexposed library operations named main8 
      having 2 argument(s) but none was determined to be applicable. 
      Use HyperDoc Browse, or issue
                              )display op main8
      to learn more about the available operations. Perhaps 
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.

   Cannot find a definition or applicable library operation named main8
      with argument type(s) 
                                    tee2
                                    tee1

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

So even the interpreter does not coerce tee1 into tee2. Guess the next three:

fricas

main8(1$Integer, 1$Integer)

$\label{eq4}6$

(4)

Type: tee2

fricas

main8(2$tee1, 5$tee2)

$\label{eq5}10$

(5)

Type: tee2

fricas

main8(3::tee1, (2$tee1)::tee2)

   Cannot convert the value from type tee1 to tee2 .

The compiler would not recognize 5$tee2, but the interpreter has no problem coercing any integer automatically to tee1 or tee2. This shows Integer is very special for the interpreter, and not treated the same as tee1.

Let's see if we change the name of foo8 to convert and make the converted value to be 4 instead of 5.

spad

)abbrev package TESTNINE test9
test9(): with
    convert:tee1 -> tee2
    main9:(tee1, tee2) -> tee2
  == add
    convert(x) == 1$tee2 + 1$tee2 + 1$tee2 + 1$tee2
    main9(x,y) == convert(x) + y

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8608886520085933680-25px017.spad
      using old system compiler.
   TESTNINE abbreviates package test9 
------------------------------------------------------------------------
   initializing NRLIB TESTNINE for test9 
   compiling into NRLIB TESTNINE 
   compiling exported convert : tee1 -> tee2
Time: 0 SEC.

   compiling exported main9 : (tee1,tee2) -> tee2
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |test9| REDEFINED

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

   Cumulative Statistics for Constructor test9
      Time: 0 seconds

   finalizing NRLIB TESTNINE 
   Processing test9 for Browser database:
--->-->test9(constructor): Not documented!!!!
--->-->test9((convert ((tee2) (tee1)))): Not documented!!!!
--->-->test9((main9 ((tee2) (tee1) (tee2)))): Not documented!!!!
--->-->test9(): Missing Description
; compiling file "/var/aw/var/LatexWiki/TESTNINE.NRLIB/TESTNINE.lsp" (written 04 APR 2022 05:49:44 PM):

; /var/aw/var/LatexWiki/TESTNINE.NRLIB/TESTNINE.fasl written
; compilation finished in 0:00:00.013
------------------------------------------------------------------------
   test9 is now explicitly exposed in frame initial 
   test9 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/TESTNINE.NRLIB/TESTNINE

test9 also compiles okay. Let's see this in action. Recall that there is a convert: tee1 -> tee2, but no coerce.

fricas

-- expects 5
main9(1$tee1, 1$tee2)

$\label{eq6}5$

(6)

Type: tee2

fricas

-- expects error
main9(1$tee2, 1$tee1)

   There are 1 exposed and 0 unexposed library operations named main9 
      having 2 argument(s) but none was determined to be applicable. 
      Use HyperDoc Browse, or issue
                              )display op main9
      to learn more about the available operations. Perhaps 
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.

   Cannot find a definition or applicable library operation named main9
      with argument type(s) 
                                    tee2
                                    tee1

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

Note convert is not automatically used by the interpreter. Now let's change convert to coerce. Even though there is now a coerce, tee1 is not declared to be CoercibleTo?(tee2) (to do so would have made the two domain constructors different in structure). We use a value 1 this time for coerce.

spad

)abbrev package TESTTEN test10
test10(): with
    coerce:tee1 -> tee2
    main10:(tee1, tee2) -> tee2
  == add
    coerce(x) == 1$tee2
    main10(x,y) == coerce(x) + y

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/7317946861256718720-25px019.spad
      using old system compiler.
   TESTTEN abbreviates package test10 
------------------------------------------------------------------------
   initializing NRLIB TESTTEN for test10 
   compiling into NRLIB TESTTEN 
   compiling exported coerce : tee1 -> tee2
Time: 0.01 SEC.

   compiling exported main10 : (tee1,tee2) -> tee2
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |test10| REDEFINED

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

   Cumulative Statistics for Constructor test10
      Time: 0.01 seconds

   finalizing NRLIB TESTTEN 
   Processing test10 for Browser database:
--->-->test10(constructor): Not documented!!!!
--->-->test10((coerce ((tee2) (tee1)))): Not documented!!!!
--->-->test10((main10 ((tee2) (tee1) (tee2)))): Not documented!!!!
--->-->test10(): Missing Description
; compiling file "/var/aw/var/LatexWiki/TESTTEN.NRLIB/TESTTEN.lsp" (written 04 APR 2022 05:49:44 PM):

; /var/aw/var/LatexWiki/TESTTEN.NRLIB/TESTTEN.fasl written
; compilation finished in 0:00:00.010
------------------------------------------------------------------------
   test10 is now explicitly exposed in frame initial 
   test10 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/TESTTEN.NRLIB/TESTTEN

fricas

-- expects 2
main10(1$tee1, 1$tee2)

$\label{eq7}2$

(7)

Type: tee2

fricas

-- expects error
main10(1$tee2, 1$tee1)

   There are 1 exposed and 0 unexposed library operations named main10 
      having 2 argument(s) but none was determined to be applicable. 
      Use HyperDoc Browse, or issue
                             )display op main10
      to learn more about the available operations. Perhaps 
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.

   Cannot find a definition or applicable library operation named 
      main10 with argument type(s) 
                                    tee2
                                    tee1

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

Now 1$tee1 is automatically coerced to 1$tee2 even though tee1 does not have CoercibleTo?(tee2), but this is the interpreter!

The next thing to do would be to test equivalence of categories. Some other time.