"Bill Page" <[EMAIL PROTECTED]> writes:
[...]
| >>>
| >>> In Implicit System F, or in a forall-quantified style I would write
| >>>
| >>> forall(T: Type) .
| >>> Associative(Modemap(T,T,T): op): Category == with nil
| >>>
| >>> so that when I say Associative(_+$Integer), T gets deduced to
| >>> Integer. You can see how this relates to the issue Stephen and
| >>> I discussed at the workshop in Hagenber.
| >>>
| >>
| >> Yes, I thought it was an interesting discussion but this machinery
| >> strikes me as being to "heavy" for what seems to me to be a relatively
| >> simple problem. I am afraid that such changes lead away from the
| >> original intend of Spad/Aldor as fundamentally an *algebraic*
| >> language. But my ideas about this are only partially formed, so I do
| >> want to keep an open mind.
| >
| > That is interesting.
| > I would be highly interested in knowing what you think is not algebraic
| > about a universally quantified type.
| >
|
| Well, to start with the construction 'Associative(_+$Integer)' is
| rather strange.
`Strange' as in `I have never seen it before', or as in ...?
| A category is a predicate which identifies a specific
| subset of domains (subdomain of Domain), namely those which explicitly
| include 'Associative(something)' in a 'Join' or 'with' clause.
That is one interpretation of category.
I find it more useful to view a category as a specification, freeing
my mind of whether it should be tied to a domain or not.
| The
| expression '_+$Integer' on the other hand is evaluated as a specific
| function exported by the domain 'Integer'.
Not in the model I showed. Rather it evaluated to a modemap: an
abstract description of an operation. E.g. it says what its domain of
computation is, what is its name, and what is its signature. Exactly,
all I need to identifier a specific operation.
| How are we to use this to
| imply that the operation exported by Integer is associative? Maybe you
| would write:
|
| Integer():Join(Associative(_+$%),...)
Nope, my opinion about something like
Ring(a:Symbol,z:Symbol,m:Symbol,o:Symbol) == Join(Associative(a),
Commutative(a), Identity(a,z), Associative(m), Commutative(m),
Identity(m,o), ... etc.
is unimprintable, so I did not engage in that road.
Rather, my approach is that algebraic properties such as associativitity
or commutativity are properties of *operations* or collection of
*operations*. Consequently, their expressions in computer program
should ideally directly reflect their mathematical notions. So, in my
scheme, once _+$Integer is defined, one can augment the working
environment with the idea that it is commutative and associative:
assume Associative _+$Integer
assume Commutative _+$Integer with
neutralElement == 0$Integer
(the category Commutative _+Integer exports the constant/operation
neutralElement).
It is a simple extensible scheme. I does not require excessive
oversight from my part to know all the possible operations that are
going to be defined for a given domain and and list them in the
exports of the domain.
| If so, then I do not see why you would prefer this over the semantics
| of simply passing a symbol.
See above.
-- Gaby
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
open-axiom-devel mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
