|
|
last edited 13 years ago by Bill Page |
1 | ||
Editor: Bill Page
Time: 2011/12/11 13:57:24 GMT-8 |
||
Note: |
changed: - 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. \begin{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 \end{spad} \begin{axiom} )sh MySet )di op join \end{axiom} \begin{axiom} MySet(Integer) has MonadCat(Integer,MySet) \end{axiom} \begin{axiom} m1:MySet(Integer) := construct([1,2,3])$MySet(Integer) m2:MySet(Integer) := construct([4,5,6])$MySet(Integer) ml:=[m1,m2] mm:MySet MySet Integer := construct([m1,m2])$MySet(MySet(Integer)) join mm \end{axiom}
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.
(1) -> <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 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
)sh MySet
You cannot now use MySet in the context you have it.
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?
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?