In a domain and in categories referenced in a domain the notation %
represents "this domain" (or self in some programming languages). So
we commonly write for example:
with
f: (%,%) -> %
to indicate a function f which takes a pair of values in this domain
and returns a value in this same domain - whatever domain we happen
to be talking about in this context.
But what if we are interested in the domain as a functor? Suppose I
was writing an "endofunctor" domain constructor like Set
and I
wanted to treat constructions like Set Set R
, i.e. sets of sets as
something special. E.g.
spad
)abbrev domain MYSET MySet
--#pile
--#include "axiom"
--MonadCat(T:SetCategory,M:SetCategory->SetCategory):Category == with
-- join: M M T -> M T
MySet(T:SetCategory): SetAggregate(T) with
finiteAggregate
join: MySet % -> %
== add
Rep := List T
rep(x:%):Rep == x pretend Rep
per(x:Rep):% == x pretend %
Rep2 == List List T
rep2(x:MySet %):Rep2 == x pretend Rep2
per2(x:Rep2):MySet % == x pretend MySet %
coerce(x:%):OutputForm ==
brace(map(coerce$T, rep x)$ListFunctions2(T,OutputForm))
((x:%) = (y:%)):Boolean == (rep(x) = rep(y))$Rep
construct(x:List T):% == per(removeDuplicates(x)$Rep)
parts(x:%):List T == rep x
join(x:MySet %):% ==
construct(concat(rep2 x)$List(T))$%
copy(x:%):% == per(copy(rep x)$Rep)
empty():% == per(empty()$Rep)
map(f:T->T,x:%):% == per(map(f,rep x)$Rep)
brace():% == empty()$%
brace(x:List(T)):% == construct(x)$%
set():% == empty()$%
set(x:List(T)):% == construct(x)$%
-- dummy exports as required by Aldor
_<(x:%, y:%):Boolean == true
intersect(x:%, y:%):% == empty()$%
difference(x:%, y:%):% == empty()$%
subset?(x:%, y:%):Boolean == true
union(x:%, y:%):% == empty()$%
if T has ConvertibleTo(InputForm) then
convert(x:%):InputForm == convert(rep(x))$Rep
spad
Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8570179011506836244-25px001.spad
using old system compiler.
MYSET abbreviates domain MySet
------------------------------------------------------------------------
initializing NRLIB MYSET for MySet
compiling into NRLIB MYSET
compiling local rep : $ -> Rep
MYSET;rep is replaced by x
Time: 0.01 SEC.
compiling local per : Rep -> $
MYSET;per is replaced by x
Time: 0 SEC.
************* USER ERROR **********
available signatures for Rep2:
NONE
NEED Rep2: () -> ?
****** comp fails at level 1 with expression: ******
((DEF (|Rep2|) (NIL) (NIL) (|List| (|List| T$))))
****** level 1 ******
$x:= (DEF (Rep2) (NIL) (NIL) (List (List T$)))
$m:= $EmptyMode
$f:=
((((|per| #)) ((|per| #) (|rep| #)) ((|rep| #) (|#| #) (< #) (<= #) ...)))
>> Apparent user error:
unspecified error
axiom
)sh MySet
MySet is a domain constructor
Abbreviation for MySet is MYSET
This constructor is not exposed in this frame.
------------------------------- Operations --------------------------------
>> System error:
The function BOOT::|MySet| is undefined.
axiom
MySet(Integer) has MonadCat(Integer,MySet)
MySet is an unknown constructor and so is unavailable. Did you mean
to use -> but type something different instead?
axiom
m1:MySet(Integer) := construct([1,2,3])$MySet(Integer)
MySet is an unknown constructor and so is unavailable. Did you mean
to use -> but type something different instead?
m2:MySet(Integer) := construct([4,5,6])$MySet(Integer)
MySet is an unknown constructor and so is unavailable. Did you mean
to use -> but type something different instead?
ml:=[m1,m2]
axiom
mm:MySet MySet Integer := construct([m1,m2])$MySet(MySet(Integer))
MySet is an unknown constructor and so is unavailable. Did you mean
to use -> but type something different instead?
join mm
There are no exposed library operations named join but there are 2
unexposed operations with that name. Use HyperDoc Browse or issue
)display op join
to learn more about the available operations.
Cannot find a definition or applicable library operation named join
with argument type(s)
Variable(mm)
Perhaps you should use "@" to indicate the required return type,
or "$" to specify which version of the function you need.