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.
fricas
(1) -> <spad>
fricas
)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>
fricas
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 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) (|List| (|List| T$))))
****** level 1 ******
$x:= (DEF (Rep2) (NIL) (List (List T$)))
$m:= $EmptyMode
$f:=
((((|per| #)) ((|per| #) (|rep| #)) ((|rep| #) (|#| #) (< #) (<= #) ...)))
>> Apparent user error:
unspecified error
fricas
)sh MySet
You cannot now use MySet in the context you have it.
fricas
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?
fricas
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?