help links subscribe changes refresh edit

SandBoxThisFunctorFriCAS

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?