Bill Page <bill.p...@newsynthesis.org> writes:
| Maybe the OpenAxiom list is an appropriate place to discuss
| foundational issues like this since it seems to have lesser priority
| in other variants of Axiom.
|
| One thing that has bothered me a bit lately when writing Axiom code is
| the use of elt and/or apply to "simulate" a domain which in my opinion
| really ought to inherit such properties from some category to which
| Mapping should also belong, call it MapCat or some such. The main idea
| is that members of some domain, aside from other properties, behave
| like functions. There is a concept of "evaluation", i.e. applying a
| function f (as a member of this domain) to members of some other
| domain to yield a member form a third domain. E.g.
|
| f in Mapping(B,A)
|
| Then we could write
|
| MyFunDom(): Join(MapCat(B,A), ...) ==
|
| and
|
| if R has MapCat(B,A) then ...
|
| etc.
|
| Gaby, I recall that some time ago you made some changes to the way
| OpenAxiom compiles Mapping, perhaps in this direction?. Are there
| plans to do further work on this? Do you see any way to reduce the
| amount of adhocracy in how this is done in Axiom? Maybe MapCat or
| equiv. should export apply? Does it make sense that another similar
| function 'elt' exists and has similar semantics?
There is an n-ary MappingCategory category constructor in OpenAxiom.
I just did not get around to fix the instantiation of Mapping ot use it.
Is that what you had in mind? Yes I plan to fix related issues.
The attached works for me.
-- Gaby
)abbrev domain MYFUN MyFunction
MyFunction(T: Type): Public == Private where
Public == MappingCategory(T,T) with
myFunction: ((T,T) -> T) -> %
Private == add
Rep == Mapping(T,T,T)
myFunction f == per f
elt(f,x) == (rep f)(x,x)
------------------------------------------------------------------------------
Fulfilling the Lean Software Promise
Lean software platforms are now widely adopted and the benefits have been
demonstrated beyond question. Learn why your peers are replacing JEE
containers with lightweight application servers - and what you can gain
from the move. http://p.sf.net/sfu/vmware-sfemails
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
