login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for SandBoxThisFunctorFriCAS revision 1 of 1

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.

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?