coercion and retraction
Ralf Hemmecke
> http://axiom-wiki.newsynthesis.org/SandBoxNonZeroInteger#msg20081202...@axiom-wiki.newsynthesis.org
Bill, you have implemented 'retract' and friends, but there is no
'RetractableTo(NonZeroInteger)'.
Since the interpreter does not seem to find 'retract', my question to
the people who know the interpreter is, when will the interpreter
*automatically* apply 'retract'?
What is it actually the interpreter looks up. Does it look for the
'CoercibleTo' category or simply for the existance of an appropriate
'coerce' function?
As far as I remember, the interpreter never applies 'convert' or
'retract' automatically. But how does it find out about a possible coercion?
Ralf
Bill Page
>
> Some words to
>
>> http://axiom-wiki.newsynthesis.org/SandBoxNonZeroInteger
>
> Bill, you have implemented 'retract' and friends, but there is no
> 'RetractableTo(NonZeroInteger)'.
>
Yes. Presumably 'RetractableTo(NonZeroInteger)' would have to be
specified in 'Integer'. This is awkward when domains are defined as
SubDomains and in FriCAS there is no extend.
> Since the interpreter does not seem to find 'retract', my
> question to the people who know the interpreter is, when
> will the interpreter *automatically* apply 'retract'?
>
Yes, that is what I is exactly what I was trying to determine.
> What is it actually the interpreter looks up. Does it look for
> the 'CoercibleTo' category or simply for the existance of an
> appropriate 'coerce' function?
>
You need to look at 'src/interp/i-coerce.boot':
As usual there are very few comments. :-( but while browsing take note
of the comment
-- retract is new name for *pullback*
coerceOrRetract(T,m) ==
(t' := coerceInteractive(T,m)) => t'
t := T
ans := nil
repeat
ans => return ans
t := retract t -- retract is new name for pullback
t = 'failed => return ans
ans := coerceInteractive(t,m)
ans
--
See especially the routine 'retractByFunction'. It is apparently
looking for the category 'RetractableTo'.
> As far as I remember, the interpreter never applies 'convert'
> or 'retract' automatically. But how does it find out about a
> possible coercion?
I am still uncertain, however I think that there maybe something
missing in the code that is supposed to treat SubDomain as a special
case.
Regards,
Bill Page.
Bill Page
>> As far as I remember, the interpreter never applies 'convert'
>> or 'retract' automatically. But how does it find out about a
>> possible coercion?
>
> I am still uncertain, however I think that there maybe something
> missing in the code that is supposed to treat SubDomain as a
> special case.
>
I found at least two places where critical knowledge of sub-domains is
built into FriCAS as a special case.
See: 'Built-in' section of:
http://axiom-wiki.newsynthesis.org/SandBoxNonZeroInteger
In general I think the FriCAS library compiler support for SubDomain
should be more complete so that such built-in knowledge is
unnecessary.
Comments would be most appreciated.
Regards,
Bill Page.
Ralf Hemmecke
> See: 'Built-in' section of:
>
> http://axiom-wiki.newsynthesis.org/SandBoxNonZeroInteger
>
> In general I think the FriCAS library compiler support for SubDomain
> should be more complete so that such built-in knowledge is
> unnecessary.
> Comments would be most appreciated.
You know that I rather like to do without the SubDomain constructor. Why
do you want to support SubDomain? That would make for a new keyword in SPAD.
Actually, Stephen Watt said something with respect to SubDomain.
1) SubDomain(X, p?) should not export anything. It cannot inherit any
function from X since as with your NonZeroInteger, there is actually no
relation between the categories of INT and NZINT. The latter is not an
AbelianMonoid anymore.
2) The only knowledge that the SubDomain constructor states is that X
and SubDomain(X, p?) have exactly the same representation. So there
SubDomain(X, p?) could be made to export
coerce: % -> X
retractIfCan: X -> Union(%, "failed")
retract: X -> % -- actually that might throw an exception
with the obvious default implementation.
So what advantage does the (undocumented) SubDomain constructor bring
for you?
One can easily do without, as the Aldor libraries show. The only thing
that SubDomain adds is the "p?" in ist argument which is accessible to
the compiler. But I rather opt for a general mechanism to incorporate a
specification language into SPAD than to just allow a hack for SubDomain.
Other opinions?
Ralf
Bill Page
>> See: 'Built-in' section of:
>>
>> http://axiom-wiki.newsynthesis.org/SandBoxNonZeroInteger
>>
On Wed, Dec 3, 2008 at 2:44 PM, Ralf Hemmecke wrote:
> You know that I rather like to do without the SubDomain constructor. Why
> do you want to support SubDomain?
I can answer this at several different levels.
At the most basic and abstract level the reason why I want there to be
a concept of "sub-domain" in FriCAS is so that FriCAS can be formally
modeled as a topos. This means that FriCAS must have limits (e.g.
products such as Record), co-limits (co-products such as Union),
exponentiation (Mapping) and a sub-object classifier. Unions and
sub-objects is where (Boolean) logic enters the system. Modern ideas
about the semantics of programming languages implies that any general
purpose (i.e. sufficiently complete) programming languages it is
possible implement these essential algebraic features. Topos theory
(and category theory in general) has been proposed as an appropriate
foundation for all (or at least a very large part) of mathematics. So
since the purpose of SPAD is to facilitate the general expression of
mathematical algorithms, it seems suitable that SPAD should implement
these universal features in the most direct manner possible.
Other people have suggested that it is not necessary for the object
language (e.g. SPAD or Aldor or even Python) to directly support the
mathematical structures one might wish to implement in a target
mathematical library, but I am strongly of the opinion that the tools
one uses determines to a very large degree the character and type of
solutions one is most likely to implement.
Another reason for wanting something like subdomain is because it is
often much easier and more efficient to implement directly in computer
hardware a complex domain of computation such as Integer or even
Float. Then one can define simpler domains such as the
PositiveIntegers, simply as a forgetful subset. Compare this for
example to the problem of defining Integer from more primitive domains
that we discussed at the last Axiom/Aldor Workshop in RISC:
http://axiom-wiki.newsynthesis.org/SandBoxDefineInteger
> That would make for a new keyword in SPAD.
SubDomain is already a keyword in SPAD (or more accurately a built-in
domain constructor like Record, Union and Mapping).
Unfortunately it is not fully and generally implemented. Union also
has some known flaws and I have argued that the notation used for
Record is not as general as it could be (Union should export injective
maps, i.e. injections and Record should export projective maps, i.e
projections). Mapping is also missing some critical exports.
>
> Actually, Stephen Watt said something with respect to SubDomain.
>
> 1) SubDomain(X, p?) should not export anything. It cannot inherit
> any function from X since as with your NonZeroInteger, there is
> actually no relation between the categories of INT and NZINT. The
> latter is not an AbelianMonoid anymore.
>
> 2) The only knowledge that the SubDomain constructor states is
> that X and SubDomain(X, p?) have exactly the same representation.
> So there SubDomain(X, p?) could be made to export
>
> coerce: % -> X
> retractIfCan: X -> Union(%, "failed")
> retract: X -> % -- actually that might throw an exception
>
> with the obvious default implementation.
>
I agree with this. Right now these things are implemented as special
purpose built-in logic in the interpreter. This makes accessing these
features from the FriCAS library rather difficult. It would be much
better and more general to implement these features in the manner
suggested by Stephen.
> So what advantage does the (undocumented) SubDomain constructor
> bring for you?
>
See above. I hope that this discussion and my experiments on the
axiom-wiki will contribute to the available documentation, eventually
leading to a better implementation in FriCAS.
> One can easily do without, as the Aldor libraries show.
I do not agree that the Aldor libraries show that it is "easy" - but
"possible", yes.
> The only thing that SubDomain adds is the "p?" in ist argument
> which is accessible to the compiler.
Since p? is a Boolean function that must interact with 'case' of Union
and programming logic in general I think that it adds a lot!
> But I rather opt for a general mechanism to incorporate a
> specification language into SPAD than to just allow a hack
> for SubDomain.
>
I do not want a "hack for SubDomain". I think the idea of a
specification language for SPAD is an interesting but separate issue.
> Other opinions?
>
I hope so! :-)
Regards,
Bill Page.
Ralf Hemmecke
> a concept of "sub-domain" in FriCAS is so that FriCAS can be formally
> modeled as a topos. This means that FriCAS must have limits (e.g.
> products such as Record), co-limits (co-products such as Union),
> exponentiation (Mapping) and a sub-object classifier. Unions and
> sub-objects is where (Boolean) logic enters the system.
So be it. But then there is the general problem. In category theory
everything happens 'up to isomorphism', in particular uniqueness.
Do you have a suggestion how you would handle that
Record(a: A, b: B)
is 'isomorphic' with
Record(b: B, a: A)?
Or, if you like take Cross and don't include the tags a and b.
Similarly you had this isomorphism problem in your last mail...
NonNegativeInteger = Union(Zero(Integer),PositiveInteger)
You must give the compiler a chance to generate exactly the same code
for both sides.
Until I read a paper that rigorously proves that the topos view on SPAD
makes for a better language, I don't believe it.
Ralf
Bill Page
>
> ...
> But then there is the general problem. In category theory
> everything happens 'up to isomorphism', in particular uniqueness.
>
That is not entirely true. There are many statements about morphisms
that involve strict equality, e.g. any commutative diagram is such a
statement. In addition, universal properties like limits specifically
require that certain morphisms exist and are *unique*. For example,
consider the definition of 'coerce' as "the pullback of an injection
along a retraction". The relationship between such a coercion and
retraction is exact.
Perhaps it is true that the relationship between domains (objects) in
a given category is defined only "up to an isomorphism". But there are
alternative descriptions/categories where this is not true. See:
http://planetmath.org/encyclopedia/CategoryTheory.html
"Isomorphism is in fact a central notion in category theory: most
categorical constructions cannot distinguish between isomorphic
objects. Frequently, this is exactly what is desired, since equality
of objects is in general a tricky concept: if we take a group and
replace each element with a pair, that element and a "tag", do we have
the same group? Strictly speaking, no, but they are certainly
isomorphic. Of course, sometimes one wants to distinguish between
isomorphic objects: the different Sylow $ p$-subgroups of a finite
group, for example. In such a case, the category-theoretic solution is
to work in a different category (called an arrow category) where the
objects are now morphisms of the original category (in the example of
subgroups of a given group, the objects would be injections of a
subgroup into a larger group). This allows one to describe exactly the
difference between the isomorphic objects: they are embedded in a
larger group in different ways."
> Do you have a suggestion how you would handle that
>
> Record(a: A, b: B)
>
> is 'isomorphic' with
>
> Record(b: B, a: A)?
>
> Or, if you like take Cross and don't include the tags a and b.
>
This is a consequence of the definition of Record as a categorical product.
> Similarly you had this isomorphism problem in your last mail...
>
> NonNegativeInteger = Union(Zero(Integer),PositiveInteger)
>
> You must give the compiler a chance to generate exactly the same
> code for both sides.
>
Thanks for correcting the example. Yes I agree that here it is a
problem. I do not know how to proceed to make this literally true. But
a domain construction like that used with SubDomain seems like it
should be possible.
> Until I read a paper that rigorously proves that the topos view on SPAD
> makes for a better language, I don't believe it.
>
I think it is necessary to explain what you mean by "a better
language". It seems obvious to me that a language that has a clear and
well-defined semantics is (usually) better than one in which the
various linguistic constructions are simply ad hoc. Even better it
seems to me is if this semantics has a clear relationship to the
immediate intended application of the language, i.e. to the expression
of mathematical concepts.
Regards,
Bill Page.
Waldek Hebisch
>
> http://axiom-wiki.newsynthesis.org/SandBoxNonZeroInteger
>
> In general I think the FriCAS library compiler support for SubDomain
> should be more complete so that such built-in knowledge is
> unnecessary.
>
> Comments would be most appreciated.
>
SubDomain is related to concept of subtyping. Unfortunatly,
proper handling of subtyping is problematic, in particular
in a languange allowing dependent types. IIRC when one
uses quite standard definition of dependent types and adds
subtyping then even _type checking_ becomes undecidable.
Type checking means that all variables (and constants) have
declared types and compiler should "just" assign types
to intermediate expressions.
I would like to have good support for subtyping, but
given that problem is hard do not expect quick results
-- such support is just a dream.
Concerning immediate future I must admit that I considered
removing SubDomain: as it is almost useless (except for
hardcoded cases of PositiveInteger and NonNegativeInteger)
but causes some complications. Actually more troubles
is caused by SubsetCategory -- I think that mere _existence_
of SubsetCategory is responsible for about 30% of current
compile time (and there is not so small code to support it).
SubsetCategory represents different variant of subtyping
-- it is category of subdomains of given domain, without
specifing exact domain but promising that you can coerce/
retract back and forth.
So, as I wrote I would like to have subtyping, but given
our current code the best tactic may be just to remove
current implementation and start from scratch.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Ralf Hemmecke
> mere _existence_ of SubsetCategory is responsible for about 30% of
> current compile time (and there is not so small code to support it).
> SubsetCategory represents different variant of subtyping -- it is
> category of subdomains of given domain, without specifing exact
> domain but promising that you can coerce/ retract back and forth.
Where is this in the code?
Are the files mentioned in
http://www.mail-archive.com/open-axi...@lists.sourceforge.net/msg00682.html
the only place related to SubsetCategory?
I wonder whether we could get rid of it. A grep of the algebra sources
just yields 'fraction.spad.pamphlet'. Perhaps simply replacing
Localize(M:Module R,
R:CommutativeRing,
S:SubsetCategory(Monoid, R)): Module R with
by
SubMonoid(R: Monoid): Category == Monoid with
coerce: % -> R
retract: R -> %
Localize(M:Module R,
R:CommutativeRing,
S:SubMonoid(R)): Module R with
(or something like that) should do. Am I wrong?
I guess one would have to add some explicit calls to 'coerce', but if
that improves the overall compilation time then <10 additional explicit
coercions is a small price.
Another related link...
http://axiom-wiki.newsynthesis.org/SandBoxSubsetCategory
Ralf
Bill Page
>> Actually more troubles is caused by SubsetCategory -- I think that
>> mere _existence_ of SubsetCategory is responsible for about 30% of
>> current compile time (and there is not so small code to support it).
>> SubsetCategory represents different variant of subtyping -- it is
>> category of subdomains of given domain, without specifing exact
>> domain but promising that you can coerce/ retract back and forth.
>
On Thu, Dec 4, 2008 at 5:01 AM, Ralf Hemmecke wrote:
> Where is this in the code?
>
> Are the files mentioned in
> http://www.mail-archive.com/open-axi...@lists.sourceforge.net/msg00682.html
> the only place related to SubsetCategory?
>
> I wonder whether we could get rid of it. A grep of the algebra sources
> just yields 'fraction.spad.pamphlet'. Perhaps simply replacing
>
> Localize(M:Module R,
> R:CommutativeRing,
> S:SubsetCategory(Monoid, R)): Module R with
>
> by
>
> SubMonoid(R: Monoid): Category == Monoid with
> coerce: % -> R
> retract: R -> %
>
> Localize(M:Module R,
> R:CommutativeRing,
> S:SubMonoid(R)): Module R with
>
> (or something like that) should do. Am I wrong?
>
Let's try it! I do not see any fundamental role played by
'SubsetCategory'. But the domain constructor 'SubDomain' is a
completely different thing. That I believe, should be a fundamental
part of the language.
> I guess one would have to add some explicit calls to 'coerce', but if
> that improves the overall compilation time then <10 additional explicit
> coercions is a small price.
>
> Another related link...
> http://axiom-wiki.newsynthesis.org/SandBoxSubsetCategory
>
I agree.
Regards,
Bill Page.
Bill Page
>>
>> Are the files mentioned in
>> http://www.mail-archive.com/open-axi...@lists.sourceforge.net/msg00682.html
>> the only place related to SubsetCategory?
>>
>> I wonder whether we could get rid of it. A grep of the algebra sources
>> just yields 'fraction.spad.pamphlet'. Perhaps simply replacing
>>
>> Localize(M:Module R,
>> R:CommutativeRing,
>> S:SubsetCategory(Monoid, R)): Module R with
>>
>> by
>>
>> SubMonoid(R: Monoid): Category == Monoid with
>> coerce: % -> R
>> retract: R -> %
>>
>> Localize(M:Module R,
>> R:CommutativeRing,
>> S:SubMonoid(R)): Module R with
>>
>> (or something like that) should do. Am I wrong?
>>
On Thu, Dec 4, 2008 at 8:38 AM, Bill Page wrote:
> Let's try it! I do not see any fundamental role played by
> 'SubsetCategory'. But the domain constructor 'SubDomain'
> is a completely different thing. That I believe, should be a
> fundamental part of the language.
>
I would like to partially withdraw my comment above. I recall now
another aspect of SubsetCategory. As Waldek said:
>> ...
>> SubsetCategory represents different variant of subtyping -- it
>> is category of subdomains of given domain, without specifying
>> exact domain
The implication is that as the *category of subdomains*, this
construction does something that is currently very inconvenient to do
otherwise in FriCAS - it gives domains that are declared to satisfy
this category the same exports as the domain R. So when we write:
Localize(M:Module R,
R:CommutativeRing,
S:SubsetCategory(Monoid, R)): Module R with
we mean that the domain S must belong to the same categories as R. I
expect that computing exactly what these categories are is a large
part of the 30% of the compile time that Waldek cited. But as pointed
out here:
http://axiom-wiki.newsynthesis.org/SandBoxSubsetCategory
For example:
)abbrev category GSUBS GroupSubset
GroupSubset(R:Type):Category == SubsetCategory(Group,R)
- spad
Compiling OpenAxiom source code from file
/var/zope2/var/LatexWiki/6559111561929448642-25px001.spad using
Spad compiler.
GSUBS abbreviates category GroupSubset
------------------------------------------------------------------------
initializing NRLIB GSUBS for GroupSubset
compiling into NRLIB GSUBS
>> System error:
Caught fatal error [memory may be damaged]
--
(This error occurs in all current versions and forks of Axiom.)
This feature of 'SubsetCategory' does not quite work in as general a
manner as we might expect.
This is related to a new feature of the SPAD language for which I have
argued elsewhere: singleton categories, that is a category as a set of
domains consisting of just one domain. For example '{Integer}' would
be the category which contains only the domain 'Integer'. Then what
Ralf called 'SubMonoid' above, could be written:
SubMonoid(R: Monoid): Category == Join({R},Monoid) with
coerce: % -> R
retract: R -> %
Note: I am not necessarily advocating '{Integer}' as an appropriate
notation for singleton category.
Regards,
Bill Page.
Bill Page
On Thu, Dec 4, 2008 at 5:01 AM, you wrote:
> ...
> Are the files mentioned in
> http://www.mail-archive.com/open-axi...@lists.sourceforge.net/msg00682.html
> the only place related to SubsetCategory?
>
> I wonder whether we could get rid of it. A grep of the algebra sources
> just yields 'fraction.spad.pamphlet'. Perhaps simply replacing
>
> Localize(M:Module R,
> R:CommutativeRing,
> S:SubsetCategory(Monoid, R)): Module R with
>
> ...
Do you know if any domain constructor like 'Localize' has ever been
implemented in the Aldor libraries?
Regards,
Bill Page.
Ralf Hemmecke
>> R:CommutativeRing,
>> S:SubsetCategory(Monoid, R)): Module R with
>>
>> ...
>
> Do you know if any domain constructor like 'Localize' has ever been
> implemented in the Aldor libraries?
Let's look... No. No Localize and nothing that looks similar. Fraction
is implemented directly.
Ralf
Waldek Hebisch
> I would like to partially withdraw my comment above. I recall now
> another aspect of SubsetCategory. As Waldek said:
>
> >> ...
> >> SubsetCategory represents different variant of subtyping -- it
> >> is category of subdomains of given domain, without specifying
> >> exact domain
>
> The implication is that as the *category of subdomains*, this
> construction does something that is currently very inconvenient to do
> otherwise in FriCAS - it gives domains that are declared to satisfy
> this category the same exports as the domain R. So when we write:
>
> Localize(M:Module R,
> R:CommutativeRing,
> S:SubsetCategory(Monoid, R)): Module R with
>
> we mean that the domain S must belong to the same categories as R. I
> expect that computing exactly what these categories are is a large
> part of the 30% of the compile time that Waldek cited.
I do not think SubsetCategory implies that S itself belongs to
some other category. Rather, SubsetCategory means that elements
of S may by coerced to R without executing any code. In other
words given element of S you can use it as an argument to any
function defined for R (and get result in R).
I would rather say that SubsetCategory is a dual of SubDomain.
Namely, assume that you want to allow any SubDomain of R
as an argument to a functor. In pseudo code:
Foo(S: Meet(Category(SubDomain(c_1,R)), Category(SubDomain(c_2,R)),
...)) :...
where you will need a infinite list of possible conditions.
Insted, you can write:
Foo(S: SubsetCategory(R)):...
and than
Foo(SubDomain(c_1,R)), Foo(SubDomain(c_2,R)),...
is legal. Note: I did not test if this works, but I believe
it was the intended use.
The compile time cost comes from checking which signatures
are applicable to arguments: for each argument of a call you
need to check if domain of this argument is a subset of some
other domain. Such checks 99.999% of times say no, but
unfortunatly with naive implementation of symbol table
searches which give the 'no' answer are the most expensive
ones. Let me add that we search such information not only
for function calls but also when generating domanis/categries
or importing domains (in such cases we need to check if some
signature is more general than another one and this again
requires checking if function having argument of type T1 can
be applied to argument of type T2) and when searching for
coercions. I have optimized searches using hash table to
be able to quickly deliver 'no' answer, but while we got
nice speedup searches are still expensive (in particular
positive searches pay extra cost of hash table lookup).
> But as pointed
> out here:
>
> http://axiom-wiki.newsynthesis.org/SandBoxSubsetCategory
>
> For example:
>
> )abbrev category GSUBS GroupSubset
> GroupSubset(R:Type):Category == SubsetCategory(Group,R)
>
<snip>
>
> >> System error:
> Caught fatal error [memory may be damaged]
>
Probably unimplemented case (to say the truth, at first glance
this looks tricky with current complilation scheme).
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Ralf Hemmecke
> some other category. Rather, SubsetCategory means that elements
> of S may by coerced to R without executing any code.
I don't think this is very important. More important is that it declares
S to be a subset of R. That one cannot do by any other means. (In Aldor
that is not expressible.)
> Foo(S: Meet(Category(SubDomain(c_1,R)), Category(SubDomain(c_2,R)),
> ...)) :...
>
> where you will need a infinite list of possible conditions.
Not a good example for me. The category of SubDomain(X, p?) does not
have anything to do with the category of X. Don't you agree?
> Insted, you can write:
>
> Foo(S: SubsetCategory(R)):...
I don't see the advantage of this. Suppose you define a Foo like this
and now you are going to explicitly write the "add" part. Which
functionality of S can you now actually use inside Foo? You always have
to wrap things with if's like
if S has AbelianGroup then ...
because statically you (and the compiler) have no knowledge about the
category of R.
> The compile time cost comes from checking which signatures
> are applicable to arguments: for each argument of a call you
> need to check if domain of this argument is a subset of some
> other domain. Such checks 99.999% of times say no, but
> unfortunatly with naive implementation of symbol table
> searches which give the 'no' answer are the most expensive
> ones. Let me add that we search such information not only
> for function calls but also when generating domanis/categries
> or importing domains (in such cases we need to check if some
> signature is more general than another one and this again
> requires checking if function having argument of type T1 can
> be applied to argument of type T2) and when searching for
> coercions. I have optimized searches using hash table to
> be able to quickly deliver 'no' answer, but while we got
> nice speedup searches are still expensive (in particular
> positive searches pay extra cost of hash table lookup).
Let's get rid of SubsetCategory. See
http://axiom-wiki.newsynthesis.org/SandBoxSubsetCategoryRemoved
Ralf
Waldek Hebisch
>
> > Foo(S: Meet(Category(SubDomain(c_1,R)), Category(SubDomain(c_2,R)),
> > ...)) :...
> >
> > where you will need a infinite list of possible conditions.
>
> Not a good example for me. The category of SubDomain(X, p?) does not
> have anything to do with the category of X. Don't you agree?
>
OK, I think you found yet another hole in this concept.
> > Insted, you can write:
> >
> > Foo(S: SubsetCategory(R)):...
>
> I don't see the advantage of this. Suppose you define a Foo like this
> and now you are going to explicitly write the "add" part. Which
> functionality of S can you now actually use inside Foo? You always have
> to wrap things with if's like
>
Actually SubsetCategory has extra argument, so it specifies
subset which is of specific category. However, since for
SubDomain I see no such extra category argument, this breaks
relation between SubDomain and SubsetCategory
> if S has AbelianGroup then ...
>
> because statically you (and the compiler) have no knowledge about the
> category of R.
>
I think that Localize actually presents intened use: in Localize
you know that R is a CommutativeRing, so category of R is
known. I believe that intended use was to pass SubDomain,
like NonZeroInteger to Localize and get (indirectly) rational
numbers. Or one would pass NumbersRelativelyPrimeTo(5) and
get apropriate local ring. AFAICS such defnitions would
allow more static checking than we have now and some dynamic
checks would be inserted automatically by the compiler.
However given current state of both SubDomain and
SubsetCategory this is not going to work.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Bill Page
My conclusion:
I agree that SubDomain needs to be re-written and that SubsetCategory
should be eliminated. I hope that it will be possible to make
incremental improvements to SubDomain rather than having to completely
re-write it. In particular I would like to make sure that members of
Union are properly treated as sub-domains of the Union,e.g. Float and
String should be recognized as sub-domains of Union(Float,String).
The rest of this message is mostly just a log of my attempt to better
understand what is going on.
On Thu, Dec 4, 2008 at 9:11 PM, you wrote:
> ...
> Actually SubsetCategory has extra argument, so it specifies
> subset which is of specific category. However, since for
> SubDomain I see no such extra category argument, this
> breaks relation between SubDomain and SubsetCategory
>
I agree. I do not see any direct relationship between relation between
SubsetCategory and SubDomain.
Also earlier I wrote:
>> The implication is that as the *category of subdomains*, this
>> construction does something that is currently very inconvenient
>> to do otherwise in FriCAS - it gives domains that are declared
>> to satisfy this category the same exports as the domain R.
But you objected:
> I do not think SubsetCategory implies that S itself belongs to
> some other category. Rather, SubsetCategory means that
> elements of S may by coerced to R without executing any
> code. In other words given element of S you can use it as an
> argument to any function defined for R (and get result in R).
I agree that you are correct. My earlier claim was wrong.
Ralf wrote:
>> more important is that it declares S to be a subset of R
The actual code says:
--% SUBSET CATEGORY
compSubsetCategory(["SubsetCategory",cat,R],m,e) ==
--1. put "Subsets" property on R to allow directly coercion to subset;
-- allow automatic coercion from subset to R but not vice versa
e:= put(R,"Subsets",[[$lhsOfColon,"isFalse"]],e)
--2. give the subset domain modemaps of cat plus 3 new functions
comp(["Join",cat,C'],m,e) where
C'() ==
substitute($lhsOfColon,"$",C'') where
C''() ==
["CATEGORY","domain",["SIGNATURE","coerce",[R,"$"]],["SIGNATURE",
"lift",[R,"$"]],["SIGNATURE","reduce",["$",R]]]
---
Is it correct to interpret this as modifying R, as a _side-effect_ of
this declaration of S, by giving domain R some new property named
"Subsets" with value "isFalse"? I do not understand "isFalse" and I do
not see however how S itself is involved in this change to R. But
perhaps the intent was to create a situation in which
R has Subsets
is be true? The property "Subsets" then being an indication to look
for domains which inherit from the SubDomain(R,...) constructor?
Is this closer to the truth?
Rather than having SubsetCategory force this property at the time
SubsetCategory is used, I think it would make better sense for this to
be done by the compiler when compiling SubDomain.
But I see that for the two uses of SubDomain in the library this
property is already statically set by:
property.lisp:(MAKEPROP '|Integer| '|Subsets|
property.lisp:(MAKEPROP '|NonNegativeInteger| '|Subsets| '(
property.lisp:(MAKEPROP '|NonPositiveInteger| '|Subsets| '(
'NonNegativeInteger' is defined as SubDomain of Integer. And
'PositiveInteger' is defined as s SubDomain of 'NonNegativeInteger'
but so far as I know there actually is no domain 'NonPositiveInteger'
nor any subdomains of it.
But in the current version of FriCAS I get the error:
(1) -> Integer has Subsets
>> System error:
newHasTest expects category from
I guess this error message contains a typo: from -> form?
The same message is produced for any token that is not a category.
While in OpenAxiom I get
(1) -> Integer has Subsets
(1) false
Type: Boolean
I expected to see true... but I guess OpenAxiom still treats all
tokens that do not match a property or a category as "false".
Maybe this "property" has nothing to do with 'has'?
In 'interp/category.boot' I read:
SourceLevelSubset(a,b) ==
--true if a is a source-level subset of b
a=b => true
$noSubsumption=true => false
b is ["Union",:blist] and member(a,blist) => true
BOUNDP '$noSubsets and $noSubsets => false
atom b and assoc(a,GETL(b,"Subsets")) => true
a is [a1] and b is [b1] and assoc(a1,GETL(b1,"Subsets")) => true
nil
--
Was this 'assoc(a,GETL(b,"Subsets"))' actually created from
'property.lisp'? Is this what the code in 'compSubsetCategory'
actually doing?
It makes sense to me that the members of a Union are "Subsets"
(sub-domains) of that Union. But this does not mean that their values
can be coerced without a change of representation!
Regards,
Bill Page.
Waldek Hebisch
>
> --% SUBSET CATEGORY
>
> compSubsetCategory(["SubsetCategory",cat,R],m,e) ==
> --1. put "Subsets" property on R to allow directly coercion to subset;
> -- allow automatic coercion from subset to R but not vice versa
> e:= put(R,"Subsets",[[$lhsOfColon,"isFalse"]],e)
> --2. give the subset domain modemaps of cat plus 3 new functions
> comp(["Join",cat,C'],m,e) where
> C'() ==
> substitute($lhsOfColon,"$",C'') where
> C''() ==
> ["CATEGORY","domain",["SIGNATURE","coerce",[R,"$"]],["SIGNATURE",
> "lift",[R,"$"]],["SIGNATURE","reduce",["$",R]]]
>
> ---
>
> Is it correct to interpret this as modifying R, as a _side-effect_ of
> this declaration of S, by giving domain R some new property named
> "Subsets" with value "isFalse"? I do not understand "isFalse" and I do
> not see however how S itself is involved in this change to R.
AFAIK the exact value does not matter, just either property is
set or not.
> But
> perhaps the intent was to create a situation in which
>
> R has Subsets
>
> is be true? The property "Subsets" then being an indication to look
> for domains which inherit from the SubDomain(R,...) constructor?
>
No, "Subsets" is internat to the compiler.
> (1) -> Integer has Subsets
>
> >> System error:
> newHasTest expects category from
>
> I guess this error message contains a typo: from -> form?
>
Yes, fixed now.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Ralf Hemmecke
>> I don't see the advantage of this. Suppose you define a Foo like this
>> and now you are going to explicitly write the "add" part. Which
>> functionality of S can you now actually use inside Foo? You always have
>> to wrap things with if's like
> Actually SubsetCategory has extra argument, so it specifies
> subset which is of specific category.
Sorry that I made that mistake, but that extra argument does not really
matter much. Why? If I write
Foo(S: SubsetCategory(Monoid, R): ...
then (as far as I understand now) is the same as saying
Foo(S: Monoid): ...
with the additional (otherwise not specifiable) understanding that S is
a subset of R and that S and R share the same representation.
Actually, above I forgot even more.
===============
1) If I specify
Foo(S: SubsetCategory(Monoid, R): ...
then R and its explicit category must be known outside Foo. Let us say
the domain R is specified like
R: CatOfR == add ...
or R is an argument to a domain in which Foo is locally defined. Also
then we have at least
WrapperDomain(R: CatOfR, ...): ... == add
...
Foo(S: SubsetCategory(Monoid, R): ...
So the category part of S would be clear. It is
Join(Monoid, CatOfR)
And that is known at compile time. So I could equally well have written
explicitly
Foo(S: Join(Monoid, CatOfR)): ...
================
2) R is also a parameter of Foo. Then we have
Foo(R: CatOfR, S: SubsetCategory(Monoid, R)): ...
But also here I know the category of R explicitly and could have written
Foo(R: CatOfR, S: Join(Monoid, CatOfR)): ...
================
Of course the R and S that one actually plugs into Foo might have more
functionality. But the code cannot rely on that and thus *must* be
started with a statement like
if S has SomeFunctionality then ...
So for me that says that the only thing that is really encoded in
SubsetCategory is that one requires the parameter R, S really to be in a
subset relation.
But now in some sense Bill might be right. Without the SubDomain
constructor I don't see any other way to construct subsets of a domain.
Otherwise SPAD lets me do is to specify a new domain that inherits its
implementation from some given domain. But since (except SubDomain)
there is no mechanism to state that two domains have the same
representation, I am not able to even create a domain that would fulfil
the SubsetCategory(Monoid, R).
Sharing the representation and state this by some language constructs
might be a good idea, but I somehow think this needs more elaboration.
I am still for removing SubsetCategory (and actually also SubDomain).
I have nothing against introducing similar concepts later, but only with
a clear specification of their meaning and a discussion of their pros
and cons.
Has someone already checked
http://axiom-wiki.newsynthesis.org/SandBoxSubsetCategoryRemoved ?
Ralf
Bill Page
> 1) If I specify
>
> Foo(S: SubsetCategory(Monoid, R): ...
>
> then R and its explicit category must be known outside Foo. Let us
> say the domain R is specified like
>
> R: CatOfR == add ...
Of course it can also include 'with' and/or 'Join' clauses.
> So the category part of S would be clear. It is
>
> Join(Monoid, CatOfR)
>
> And that is known at compile time. So I could equally well have
> written explicitly
>
> Foo(S: Join(Monoid, CatOfR)): ...
>
'CatOfR' is what I earlier called the "singleton category" of R or
{R}. You say that it is "known at compile time", but as far as I can
see if all we know is R, we have to syntactical means (other than
perhaps SubsetCategory) to tell the compiler that this is the category
that we are talking about. I think that being able to specify this
independently of SubsetCategory is a good idea. If not {R} then why
not make 'CatOf(R)' or something like thatsomehow special?
But recall that Waldek claimed that that it is not really true that
SubsetCategory constructs this Join involving CatOfR. After reviewing
the code again, I agree with Waldek. CatOfR is apparently not needed
here.
> ================
> 2) R is also a parameter of Foo. Then we have
>
> Foo(R: CatOfR, S: SubsetCategory(Monoid, R)): ...
>
> But also here I know the category of R explicitly and could have written
>
> Foo(R: CatOfR, S: Join(Monoid, CatOfR)): ...
>
How do you "know the category of R explicitly"? Do you mean manually
copying the category definition used in the source code of R?
> ...
> But now in some sense Bill might be right. Without the SubDomain
> constructor I don't see any other way to construct subsets of a
> domain. Otherwise SPAD lets me do is to specify a new domain
> that inherits its implementation from some given domain. But since
> (except SubDomain) there is no mechanism to state that two
> domains have the same representation, I am not able to even
> create a domain that would fulfil the SubsetCategory(Monoid, R).
>
Perhaps it is correct to want that 'SubsetCategory(M, R)' be the
category to which the domains 'SubDomain(R,b)' belong and where
'SubsetCategory(M,R)' is special itself inherits the category
structure of M (i.e. is a sub-category of M). I think this would
essentially make the 'Subset' property that is now internal to the
compiler, available directly to the programmer.
I hope I am not saying anything stupid here...
> Sharing the representation and state this by some language constructs
> might be a good idea, but I somehow think this needs more elaboration.
>
I think it would be a good idea to completely and accurately describe
the desired model of sub-domain that we want in FriCAS. I have a
feeling that in spite of how bad it looks, what is implemented in
FriCAS already may not be that far off the mark and might be
salvagable.
> I am still for removing SubsetCategory (and actually also SubDomain).
>
> I have nothing against introducing similar concepts later, but only
> with a clear specification of their meaning and a discussion of their
> pros and cons.
>
As I said, I agree with the need for a clear specification, but I do
not like the strategy of removing something just because we do not
completely understand it. If we were to take this approach more
generally, I think we would end up throwing away many other parts of
Axiom as well. :-(
> Has someone already checked
> http://axiom-wiki.newsynthesis.org/SandBoxSubsetCategoryRemoved ?
>
I have looked at it and I do not see anything wrong with your
proposal. I think we/you should apply this change to a local copy of
FriCAS and run the full regression tests. I think you have given good
reasons as to why we should not expect any regressions in the current
FriCAS library code.
Regards,
Bill Page.
Bill Page
paragraph more intelligible.
On Fri, Dec 5, 2008 at 8:51 PM, I wrote:
>
> 'CatOfR' is what I earlier called the "singleton category" of R or
> {R}. You say that it is "known at compile time", but as far as I can
> see if all we know is R, we have to syntactical means (other than
> perhaps SubsetCategory) to tell the compiler that this is the
> category that we are talking about. I think that being able to
> specify this independently of SubsetCategory is a good idea. If
> not {R} then why not make 'CatOf(R)' or something like that
> somehow special?
>
I intended to write:
... if all we know is R, we have *no* syntactical means (other than
perhaps SubsetCategory) to tell the compiler that this is the
category ...
Regards,
Bill Page.
Ralf Hemmecke
> On Fri, Dec 5, 2008 at 11:22 AM, Ralf Hemmecke wrote:
>> 1) If I specify
>>
>> Foo(S: SubsetCategory(Monoid, R): ...
>>
>> then R and its explicit category must be known outside Foo. Let us
>> say the domain R is specified like
>>
>> R: CatOfR == add ...
> Of course it can also include 'with' and/or 'Join' clauses.
CatOfR was meant to be the exact category expression that is used in the
definition of R.
>> So the category part of S would be clear. It is
>>
>> Join(Monoid, CatOfR)
>>
>> And that is known at compile time. So I could equally well have
>> written explicitly
>>
>> Foo(S: Join(Monoid, CatOfR)): ...
> 'CatOfR' is what I earlier called the "singleton category" of R or
> {R}.
I am sorry, but that is exactly *not* what I had in mind. To make it
more concrete, replace
R: CatOfR == add ...
everywhere with
SparseUnivariatePolynomial(T:Ring): UnivariatePolynomialCategory(T) with
outputForm : (%,OutputForm) -> OutputForm
fmecg: (%,NonNegativeInteger,T,%) -> %
== PolynomialRing(T,NonNegativeInteger)
add
...
i.e. with the concrete definition of a domain.
As you probably realize here.
UnivariatePolynomialCategory(T) with ...
is certainly not a "one-element category".
> You say that it is "known at compile time", but as far as I can
> see if all we know is R, we have to syntactical means (other than
> perhaps SubsetCategory) to tell the compiler that this is the category
> that we are talking about.
Also if I take the correction of that paragraph in your other mail
http://groups.google.com/group/fricas-devel/msg/7e29d803d32f549b
into account, I really mean "known at "compile time". I speak about that
"SubsetCategory" appearing in a .spad file. There you always know about
the type of R statically. If you think otherwise, you should give a
concrete example of an identifier R that appears in a .spad file and
from which you wouldn't know its type.
> I think that being able to specify this
> independently of SubsetCategory is a good idea. If not {R} then why
> not make 'CatOf(R)' or something like thatsomehow special?
Because it is not needed. What you want is to compute with category
expression. That is not really a such a bad idea, but leads to problems
as you certainly know from
http://axiom-portal.newsynthesis.org/refs/articles/define.pdf
in particular (see page 5) when the CatOfR from above is
CatOfR: Category ==
if random() then
with {a: SingleInteger}
else
with {a: Float}
>> ================
>> 2) R is also a parameter of Foo. Then we have
>>
>> Foo(R: CatOfR, S: SubsetCategory(Monoid, R)): ...
>>
>> But also here I know the category of R explicitly and could have written
>>
>> Foo(R: CatOfR, S: Join(Monoid, CatOfR)): ...
> How do you "know the category of R explicitly"? Do you mean manually
> copying the category definition used in the source code of R?
Basically, yes. Do you see a problem with that? When you are going to
program Foo, you are not interested in the exact category of R. All you
need is certain properties that R must have. In
Foo(R: CatOfR, S: Join(Monoid, CatOfR)): ...
CatOfR is actually the wrong name. I should better have chosen
"FoosRequirementForR". The actual category is really not interesting.
All that Foo cares about is that its parameter has to fulfil a certain
set of properties which is encoded in the type of the parameter
specification. I hope I could make that now clear enough.
>> I am still for removing SubsetCategory (and actually also SubDomain).
> As I said, I agree with the need for a clear specification, but I do
> not like the strategy of removing something just because we do not
> completely understand it. If we were to take this approach more
> generally, I think we would end up throwing away many other parts of
> Axiom as well. :-(
I only heard Waldek saying that SubsetCategory causes 30% of all the
compile time. There should be a better implementation of the concepts
SubsetCategory and SubDomain anyway. I think they are better started
from scratch if someone sees need for having them. My experience with
Aldor where these concepts do not exist, is, that I never felt the need
to reintroduce them. Just let's take a pragmatic approach here and have
faster compile time now.
I'll start testing my changes locally and will propose a patch
(hopefully this weekend).
Ralf
Bill Page
>
> On 12/06/2008 02:51 AM, Bill Page wrote:
> ...
>> 'CatOfR' is what I earlier called the "singleton category" of R
>> or {R}.
>
> I am sorry, but that is exactly *not* what I had in mind. To make it
> more concrete, replace
>
> R: CatOfR == add ...
>
> everywhere with
>
> SparseUnivariatePolynomial(T:Ring): UnivariatePolynomialCategory(T) with
> outputForm : (%,OutputForm) -> OutputForm
> fmecg: (%,NonNegativeInteger,T,%) -> %
> == PolynomialRing(T,NonNegativeInteger)
> add
> ...
>
> i.e. with the concrete definition of a domain.
>
> As you probably realize here.
>
> UnivariatePolynomialCategory(T) with ...
>
> is certainly not a "one-element category".
>
Au contraire, I do believe that if you include *everything* between :
and ==, i.e.
UnivariatePolynomialCategory(T) with
outputForm : (%,OutputForm) -> OutputForm
fmecg: (%,NonNegativeInteger,T,%) -> %
then given some value for T e.g. 'Integer', this is indeed a category
that is satisfied by only one domain, namely:
'SparseUnivariatePolynomial(Integer)'. If you do not agree, could you
give me an example of another domain that has this category?
I think it is important distinguish when one is simply referring to a
category by name and when one wants a category *value*. A category
value is required to the right of the ':'. The operators 'Join' and
'with' form category expressions that need to be evaluated by the
compiler to a category value.
In Aldor 'with' clauses are said to form anonymous categories and one
anonymous category is never equal to another, even if they include the
same exports.
For example, the domains A1 and A2
A1:with f:B->C ==
and
A2:with f:B->C ==
necessarily belong to different categories. That is
A1 has CatOfA2
and
A2 has CatOfA1
are necessarily false.
>> You say that it is "known at compile time", but as far as I can
>> see if all we know is R, we have to syntactical means (other than
>> perhaps SubsetCategory) to tell the compiler that this is the
>> category that we are talking about.
>
> Also if I take the correction of that paragraph in your other mail
> http://groups.google.com/group/fricas-devel/msg/7e29d803d32f549b
> into account, I really mean "known at "compile time". I speak about
> that "SubsetCategory" appearing in a .spad file. There you always
> know about the type of R statically. If you think otherwise, you should
> give a concrete example of an identifier R that appears in a .spad file
> and from which you wouldn't know its type.
>
Since Spad is strongly typed, of course that is not what I meant. By:
... if all we know is R, we have *no* syntactical means (other than
perhaps SubsetCategory) to tell the compiler that this is the
category ...
I meant there is no construct in the Spad language that I can use to
tell the compiler that I am referring to the *category* to which R
belongs and not the domain R itself. I do not want to manually copy
the category part of the definition of R into my new source code every
time I need something that should belong to the same category as R. I
would like to be able to change the definition of R in just one place
and still expect everything to work.
>> I think that being able to specify this independently of
>> SubsetCategory is a good idea. If not {R} then why not make
>> 'CatOf(R)' or something like that somehow special?
>
> Because it is not needed.
I now agree that this is not needed for SubsetCategory but I do not
agree that it is not needed in general. I have given examples of how
singleton categories can be useful in another thread.
But there is still an issue with 'SubsetCategory'. After 'S:' in the code:
Foo(S: SubsetCategory(Monoid, R)): ...
we expect to see a category. This is the category denoted by
SubsetCategory(Monoid,R)
and depends on 'Monoid' but it is not just 'Monoid' it is some
subcategory of Monoid. (Although as you have shown, taking it to just
be Monoid is almost sufficient for the way that SubsetCategory is used
in the current FriCAS library.) As far as I can see, there is no way
to write such a category constructor in FriCAS. We migh try:
SubsetCategory(M:Category, R:Domain):Category == M with
coerce: % -> R
...
But I am quite sure this will not compile in FriCAS.
> What you want is to compute with category expression. That is
> not really a such a bad idea, but leads to problems as you certainly
> know from
> http://axiom-portal.newsynthesis.org/refs/articles/define.pdf
> in particular (see page 5) when the CatOfR from above is
>
> CatOfR: Category ==
> if random() then
> with {a: SingleInteger}
> else
> with {a: Float}
>
No. As I said above anonymous categories formed from 'with' clauses
are never equal. But named categories are equal if their *names* are
the same. As you have defined it abouve 'CatOfR' is a constant whose
value is determined just once at the start of the program. It can be a
different value each time the program is run, but within an instance
of the program it always refers to the same category.
>>> ================
>>> 2) R is also a parameter of Foo. Then we have
>>>
>>> Foo(R: CatOfR, S: SubsetCategory(Monoid, R)): ...
>>>
>>> But also here I know the category of R explicitly and could have
>>> written
>>>
>>> Foo(R: CatOfR, S: Join(Monoid, CatOfR)): ...
>
>> How do you "know the category of R explicitly"? Do you mean
>> manually copying the category definition used in the source code
>> of R?
>
> Basically, yes. Do you see a problem with that?
Yes I do see a problem with that as I described above.
> When you are going to program Foo, you are not interested in the
> exact category of R. All you need is certain properties that R must
> have. In
>
> Foo(R: CatOfR, S: Join(Monoid, CatOfR)): ...
>
> CatOfR is actually the wrong name. I should better have chosen
> "FoosRequirementForR". The actual category is really not interesting.
I agree. The interesting situation is more like this:
Bar(R: Ring, S: CatOfR): ...
Here I mean that I require S to be from the *same category* as R.
Because R can belong to many other categories besides Ring this is not
quite the same thing as saying
Bar(R: Ring, S: Ring): ...
> All that Foo cares about is that its parameter has to fulfil a
> certain set of properties which is encoded in the type of the
> parameter specification. I hope I could make that now clear
> enough.
>
I think what you wrote is clear. You seem to be saying that you do not
think that constructions like 'Bar' are needed in Spad. I am making
the opposite claim.
>>> I am still for removing SubsetCategory (and actually also SubDomain).
>
>> As I said, I agree with the need for a clear specification, but I do
>> not like the strategy of removing something just because we do
>> not completely understand it. If we were to take this approach
>> more generally, I think we would end up throwing away many
>> other parts of Axiom as well. :-(
>
> I only heard Waldek saying that SubsetCategory causes 30% of all
> the compile time.
I would like to understand better this claim of "30% of all compile
time". Afterall, 'SubsetCategory' only occurs in one source file in
the FriCAS library. Now that you have shown that this use can be
eliminated without any regression in FriCAS functionality, what
remains in order to remove the the compiler's treatment of
'SubsetCategory'? I am sure that Waldek has good reasons for making
this claim, but it is not clear to me what can now be changed in the
compiler to recover this 30%.
> There should be a better implementation of the concepts
> SubsetCategory and SubDomain anyway. I think they are better
> started from scratch if someone sees need for having them. My
> experience with Aldor where these concepts do not exist, is, that
> I never felt the need to reintroduce them. Just let's take a pragmatic
> approach here and have faster compile time now.
>
I would like a faster compile time, but I do not want to compromise on
the power of the Spad language. As much as I admire your programming
skills in Aldor, I do not think that observations like "My experience
with Aldor where these concepts do not exist, is, that I never felt
the need to reintroduce them." is sufficient justification for
removing features from Spad. I would much prefer that we have some
theory and a model for Spad for which we can (at least in principle)
prove that it provides at least the generality that is necessary to
express a very large part of modern mathematics. As you know, I have
frequently promoted the idea that mathematical category theory
provides such a model. And it turns out that the concept of SubDomain
is a very critical part of such a model.
Regards,
Bill Page.
Ralf Hemmecke
>>
>> UnivariatePolynomialCategory(T) with ...
>>
>> is certainly not a "one-element category".
>>
>
> Au contraire, I do believe that if you include *everything* between :
> and ==, i.e.
>
> UnivariatePolynomialCategory(T) with
> outputForm : (%,OutputForm) -> OutputForm
> fmecg: (%,NonNegativeInteger,T,%) -> %
>
> then given some value for T e.g. 'Integer', this is indeed a category
> that is satisfied by only one domain, namely:
> 'SparseUnivariatePolynomial(Integer)'. If you do not agree, could you
> give me an example of another domain that has this category?
Enter UnivariatePolynomialCategory into HyperDoc. Then click on
"domains". (But that is probably not what you mean.)
Let's abbreviate the above category (*) with T replaced by Integer by
Cat. Then you are probably right that in the current Algebra of
panAxiom, there is only one domain that exactly has these exports. But
in the next version of FriCAS I might have added
RalfPolynomials: Cat == SparseUnivariatePolynomial(Integer);
RalfPolynomials2: Cat == SparseUnivariatePolynomial(Integer) add
foo(x: %): % == x;
These are two more domains with exactly Cat as exports. If you still
don't like that they are basically the same as
SparseUnivariatePolynomial(Integer), then let's build a domain with
exports Cat and another representation.
RalfPolynomial3(n: Integer): Cat == add
Rep == Record(pol: SparseUnivariatePolynomial(Integer), tag: Integer)
coerce(i: Integer): % == [i::SparseUnivariatePolynomial(Integer), n]
_-(x: %): % == [-(rep(x).pol), n]
...
Now whether you count that RalfPolynomial3 is just one new domain that
fulfils Cat or whether that gives one domain for every integer n doesn't
matter. It is at least saying that Cat is not a one-element-category.
> I think it is important distinguish when one is simply referring to a
> category by name and when one wants a category *value*. A category
> value is required to the right of the ':'. The operators 'Join' and
> 'with' form category expressions that need to be evaluated by the
> compiler to a category value.
>
> In Aldor 'with' clauses are said to form anonymous categories and one
> anonymous category is never equal to another, even if they include the
> same exports.
Where did you find this statement in the Aldor User Guide? Aldor gives
me no way to compare categories anyway. And where would it matter
anyway. What is important is the type satisfaction (see Section 7.7 (and
7.5) in the AUG).
> For example, the domains A1 and A2
>
> A1:with f:B->C ==
>
> and
>
> A2:with f:B->C ==
>
> necessarily belong to different categories. That is
>
> A1 has CatOfA2
>
> and
>
> A2 has CatOfA1
>
> are necessarily false.
If you mean a constructor CatOf and say CatOfA1=CatOf(A1), then I might
agree, but why do you think that is important. Give a concrete program
where you would like to have this feature.
<snip>
> Since Spad is strongly typed, of course that is not what I meant. By:
>
> ... if all we know is R, we have *no* syntactical means (other than
> perhaps SubsetCategory) to tell the compiler that this is the
> category ...
>
> I meant there is no construct in the Spad language that I can use to
> tell the compiler that I am referring to the *category* to which R
> belongs and not the domain R itself. I do not want to manually copy
> the category part of the definition of R into my new source code every
> time I need something that should belong to the same category as R. I
> would like to be able to change the definition of R in just one place
> and still expect everything to work.
Please give a conrete use case.
>> What you want is to compute with category expression. That is
>> not really a such a bad idea, but leads to problems as you certainly
>> know from
>> http://axiom-portal.newsynthesis.org/refs/articles/define.pdf
>> in particular (see page 5) when the CatOfR from above is
>>
>> CatOfR: Category ==
>> if random() then
>> with {a: SingleInteger}
>> else
>> with {a: Float}
>>
>
> No. As I said above anonymous categories formed from 'with' clauses
> are never equal. But named categories are equal if their *names* are
> the same. As you have defined it abouve 'CatOfR' is a constant whose
> value is determined just once at the start of the program. It can be a
> different value each time the program is run, but within an instance
> of the program it always refers to the same category.
OK. Then write a domain that belongs to my CatOfR from above. As you
know you can only write that domain before you run the program.
<Rest skipped for now>
Ralf
Ralf Hemmecke
>> exact category of R. All you need is certain properties that R must
>> have. In
>>
>> Foo(R: CatOfR, S: Join(Monoid, CatOfR)): ...
>>
>> CatOfR is actually the wrong name. I should better have chosen
>> "FoosRequirementForR". The actual category is really not interesting.
>
> I agree. The interesting situation is more like this:
>
> Bar(R: Ring, S: CatOfR): ...
>
> Here I mean that I require S to be from the *same category* as R.
> Because R can belong to many other categories besides Ring this is not
> quite the same thing as saying
>
> Bar(R: Ring, S: Ring): ...
I agree with this observation, but I still would like to see a concrete
example where the situation
Bar(R: Ring, S: CatOf(R)): ...
is really necessary. All I can think of for this abstract setting is
that knowing that S belongs to exactly the same category as R means that
if in Bar there is something like
if R has Monoid then SomeCode;
then in SomeCode the compiler would not complain if you write
s: S := s1 * s2;
where s1 and s2 are of type S. I don't consider that a really big
advantage, since I could easily have written
if R has Monoid and S has Monoid then SomeCode;
in order to make everything totally clear in SomeCode. (And I would even
prefer this explicit "and S has Monoid".)
>> All that Foo cares about is that its parameter has to fulfil a
>> certain set of properties which is encoded in the type of the
>> parameter specification. I hope I could make that now clear
>> enough.
>>
>
> I think what you wrote is clear. You seem to be saying that you do not
> think that constructions like 'Bar' are needed in Spad. I am making
> the opposite claim.
OK. Nothing is bad with opposite opinions, the only problem I have is
that I cannot give an example that the 'Bar' construction with CatOf(R)
is not needed. That is why I like *you* to give a concrete example (not
an abstract one) to support your claim.
>> I only heard Waldek saying that SubsetCategory causes 30% of all
>> the compile time.
> I would like to understand better this claim of "30% of all compile
> time".
True. But in the end, that is not my main point why I would like to
remove SubsetCategory.
>> There should be a better implementation of the concepts
>> SubsetCategory and SubDomain anyway. I think they are better
>> started from scratch if someone sees need for having them. My
>> experience with Aldor where these concepts do not exist, is, that
>> I never felt the need to reintroduce them. Just let's take a pragmatic
>> approach here and have faster compile time now.
>>
>
> I would like a faster compile time, but I do not want to compromise on
> the power of the Spad language. As much as I admire your programming
> skills in Aldor, I do not think that observations like "My experience
> with Aldor where these concepts do not exist, is, that I never felt
> the need to reintroduce them." is sufficient justification for
> removing features from Spad.
Of course that is not a proof. I just lobby for the removal of
SubsetCategory. If Waldek finally accepts my patch, fine, if not then
that doesn't hurt me so much either. I will have learned something about
the internals of FriCAS by then.
> I would much prefer that we have some
> theory and a model for Spad for which we can (at least in principle)
> prove that it provides at least the generality that is necessary to
> express a very large part of modern mathematics. As you know, I have
> frequently promoted the idea that mathematical category theory
> provides such a model. And it turns out that the concept of SubDomain
> is a very critical part of such a model.
Can you somehow turn your ideas into code? Suppose you have a perfect
SPAD (call it SPAD-CAT). How would a polynomial domain in infinitely
many variables over some coefficient ring look like. Make it concrete.
Of course it will not compile since SPAD is not yet as categorical as
you would like. But maybe from your code one sees how SPAD should
develop. I don't know whether a polynomial domain is sufficiently
complex enough to show the advantage of what you have in mind, but I
guess doing it with infinitely many variables might involve some Limit
construction.
Best regards
Ralf
Waldek Hebisch
> Of course that is not a proof. I just lobby for the removal of
> SubsetCategory. If Waldek finally accepts my patch, fine, if not then
> that doesn't hurt me so much either. I will have learned something about
> the internals of FriCAS by then.
>
I had a little problem applying your patch: what I received
in mail did not apply cleanly (I am not sure why, after looking
at patch and source did see any problem). I am now testing
modifed version of your patch (just to see if/how possible
variants work).
One remark: if we want just preserve existing functionality,
then the simplest way is probably to remove the third argument to
Localize and LocalAlgebra. Namely, currentlty there is probably
no way to create nontrivial domain of SubsetCategory, so the
in working code third argument will be the same as the second
one. Your patch actually makes Localize more general, because
it allows different representation for S -- AFAICS you can
use
Localize(M, Polynomial Integer, MyInteger)
where MyInteger is Integer with extra coercion to Polynomial Integer.
Extra generality may be good, but I wonder if gain (possibility
to use different representation and checking that denominators
really belong to S) is worth the cost (possible performance loss).
Also, it is not clear how well S different from R would work
-- I must admit that current Localize and LocalAlgebra look
half-baked to me.
BTW: While LocalAlgebra is mentioned in solverad.spad.pamphlet
AFAICS it is actually unused. So it seems that the only current
use of Localize and LocalAlgebra is via Fraction.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Ralf Hemmecke
> then the simplest way is probably to remove the third argument to
> Localize and LocalAlgebra. Namely, currentlty there is probably
> no way to create nontrivial domain of SubsetCategory, so the
> in working code third argument will be the same as the second
> one.
Oh, good that you yourself say this. I was exactly thinking in this
direction and wanted to create a two parameter Localize and LocalAlgebra
(*in addition*, in order not to break other people's code that relies on
3-parameter version).
But yes, I am very much in favour of removing the third parameter. Or
rather to replace it with a boolean function in the following sense
(It's similar to SubDomain.):
Instead of
Localize(M:Module R,
R:CommutativeRing,
S:SubsetCategory(Monoid, R)): Module R with
we would have
Localize(M:Module R,
R:CommutativeRing,
denominator?: R -> Boolean): Module R with
where denominator is the characteristic function for the subset S of R
that can be used for denominators.
Of course, there is a big problem: It cannot be ensured that the set of
all r for which denominator?(r) returns true is indeed a sub-monoid of
R. But in some way that is as troublesome as is the second parameter of
SubDomain. Nothing would currently prevent me to define
MyPosInt: AbelianMonoid == SubDomain(Integer, #1>0) add (x:%)
So this 'denominator?' parameter would not make things much worse.
> Your patch actually makes Localize more general, because
> it allows different representation for S -- AFAICS you can
> use
>
> Localize(M, Polynomial Integer, MyInteger)
>
> where MyInteger is Integer with extra coercion to Polynomial Integer.
Yes.
> Extra generality may be good, but I wonder if gain (possibility
> to use different representation and checking that denominators
> really belong to S) is worth the cost (possible performance loss).
The most common domain like Fraction should not suffer. But with my
change it possibly does (adding a coerce: %->% panelty that is avoidable
by a two-parameter Localize).
> Also, it is not clear how well S different from R would work
> -- I must admit that current Localize and LocalAlgebra look
> half-baked to me.
>
> BTW: While LocalAlgebra is mentioned in solverad.spad.pamphlet
> AFAICS it is actually unused.
Oh, good observation.
> So it seems that the only current
> use of Localize and LocalAlgebra is via Fraction.
In this case, I would even go to the extreme and remove LocalAlgebra and
Localize completely. If somebody later sees some need for their
reimplementation then we have someone who is familiar with all the
issues and who knows probably some use cases that should work.
Ralf
PS: It seems that I am trying to get rid of FriCAS functionality. I hope
nobody beats me for that... ;-)
Martin Rubey
> PS: It seems that I am trying to get rid of FriCAS functionality. I hope
> nobody beats me for that... ;-)
Don't worry! If you want to make me a Christmas present: plunge into the
Categories of FriCAS and redesign them - yes: only the categories. I know that
you are quite good at that, and it's probably the one thing FriCAS needs most
badly currently.
I started to look at three different areas, but I admit that I mostly failed,
although I now know at least some of the issues involved and documented the
current situation a tiny little bit.
* make power series and polynomial categories consistent and "nice"
* improve the matrix categories
* improve the aggregate world
* create good categories for function spaces. (what a pity FunctionSpace is
already taken...)
And, in my opinion, do not worry about breaking user code. There aren't that
many users of FriCAS currently anyway, and I think most of them will happily
spend a little bit of time updating their code in exchange for more
consistency.
Martin
Ralf Hemmecke
> Ralf Hemmecke <ra...@hemmecke.de> writes:
>
>> PS: It seems that I am trying to get rid of FriCAS functionality. I hope
>> nobody beats me for that... ;-)
>
> Don't worry! If you want to make me a Christmas present: plunge into the
> Categories of FriCAS and redesign them - yes: only the categories.
Do you mean a present for 2011? ;-) That's a lot of work. And I want
"extend" first.
> And, in my opinion, do not worry about breaking user code.
I wouldn't anyway. ;-)
But I think I first need a better compiler. Unfortunately, I am probably
not of much help there.
Ralf
Martin Rubey
> On 12/10/2008 12:06 AM, Martin Rubey wrote:
> > Ralf Hemmecke <ra...@hemmecke.de> writes:
> >
> >> PS: It seems that I am trying to get rid of FriCAS functionality. I hope
> >> nobody beats me for that... ;-)
> >
> > Don't worry! If you want to make me a Christmas present: plunge into the
> > Categories of FriCAS and redesign them - yes: only the categories.
>
> Do you mean a present for 2011? ;-) That's a lot of work.
I didn't mean *all* Categories. Real progress in one of these areas would
already make me happy...
> And I want "extend" first.
I see that extend is nice, but actually, within FriCAS I don't see whether it's
such a big issue? Maybe for the coercion definitions, but actually, that's one
place where I think that Aldor is missing functionality, i.e., allow something
like
forall A if A has MyCat then CoercibleTo A
or perhaps
CoercibleTo A where A has MyCat.
> > And, in my opinion, do not worry about breaking user code.
>
> I wouldn't anyway. ;-)
> But I think I first need a better compiler. Unfortunately, I am probably
> not of much help there.
I think that FriCAS missed one thing: some people thought "Oh dear, I have to
do everything myself", not realising that others will happily follow if
somebody starts with enough energy.
Sage got that one right. Sage does not work very well in comparison with
FriCAS (although it meanwhile covers more mathematics), but it got so brilliant
marketing, that many many people joined. And it allow people to contribute who
are not mathematicians. In FriCAS, even the emacs mode is done by
mathematicians... I think that's quite suboptimal.
I truly hope that there will be another wave of interest for FriCAS soon.
Martin
Bill Page
> Bill Page wrote:
>> The interesting situation is more like this:
>>
>> Bar(R: Ring, S: CatOfR): ...
>>
>> Here I mean that I require S to be from the *same category* as R.
>> Because R can belong to many other categories besides Ring this
>> is not quite the same thing as saying
>>
>> Bar(R: Ring, S: Ring): ...
>
> I agree with this observation, but I still would like to see a concrete
> example where the situation
>
> Bar(R: Ring, S: CatOf(R)): ...
>
> is really necessary.
The original use case that I presented in another thread involved a
different use of "CatOf(R)". If it were possible to refer directly to
the category to which a domain belongs, then implementing something
similar to Aldor 'extend' would be easy in Spad
MyInteger():CatOf(Integer) with
...
== Integer add
...
The domain MyInteger is then an extension of Integer. Note: Trying to
use 'SubsetCategory' in the same position as CatOf above leads to a
compiler abort.
> All I can think of for this abstract setting is that knowing that S
> belongs to exactly the same category as R means that if in Bar
> there is something like
>
> if R has Monoid then SomeCode;
>
> then in SomeCode the compiler would not complain if you write
>
> s: S := s1 * s2;
>
> where s1 and s2 are of type S. I don't consider that a really big
> advantage, since I could easily have written
>
> if R has Monoid and S has Monoid then SomeCode;
>
> in order to make everything totally clear in SomeCode. (And I would even
> prefer this explicit "and S has Monoid".)
>
In less abstract terms 'S:CatOf(Integer)' simply means that everywhere
I use 'S' I can treat it exactly like 'Integer' even though it may be
a conceptually distinct domain. An example of something like this
already in the the FriCAS library is 'RomanNumeral'.
>> I would much prefer that we have some theory and a model for Spad
>> for which we can (at least in principle) prove that it provides at least
>> the generality that is necessary to express a very large part of modern
>> mathematics. As you know, I have frequently promoted the idea that
>> mathematical category theory provides such a model. And it turns out
>> that the concept of SubDomain is a very critical part of such a model.
>
> Can you somehow turn your ideas into code? Suppose you have a
> perfect SPAD (call it SPAD-CAT).
Yes, I am continuing to think about that. For example I have given an
example on axiom-wiki of Spad code that implements data structures
similar to Record and Union based on categorical products and
co-products.
http://axiom-wiki.newsynthesis.org/LimitsAndColimits
> How would a polynomial domain in infinitely many variables over
> some coefficient ring look like. Make it concrete.
Re: "polynomial domain in infinitely many variables" ??? Isn't that
exactly what the domain 'Polynomial' is FriCAS is already? I don't see
that as a concrete example of what I am talking about.
> Of course it will not compile since SPAD is not yet as categorical
> as you would like. But maybe from your code one sees how SPAD
> should develop. I don't know whether a polynomial domain is
> sufficiently complex enough to show the advantage of what you
> have in mind, but I guess doing it with infinitely many variables
> might involve some Limit construction.
>
No, not so far as I understand what you mean.
The concept of limits (and co-limits) in category theory involve what
are known as universal constructions. These are situations where the
axioms allow one to specify that some operation exists and is uniquely
defined.
http://en.wikipedia.org/wiki/Universal_construction
For example, in the case of 'Product(X,Y)' the operation that is
required to exist and be uniquely defined is
product: (A:Type, A->X,A->Y) -> (A->%)
for any domain A and functions A->X, A->Y.
Regards,
Bill Page.
Bill Page
>
> I see that extend is nice, but actually, within FriCAS I don't see whether
> it's such a big issue? Maybe for the coercion definitions, but actually,
> that's one place where I think that Aldor is missing functionality, i.e.,
> allow something like
>
> forall A if A has MyCat then CoercibleTo A
>
> or perhaps
>
> CoercibleTo A where A has MyCat.
>
I presume that you mean that one might write this in the context of
some domain, say B.
Isn't this essentially what one might do in defining a package? E.g.
MyCoercePac(A:MyCat,X:CatOf(B)): CoercibleTo(A)
== add
coerce(x:X):A == ...
At least in the interpreter if 'MyCoercePac' is exposed than the
interpreter can expect to find a function 'coerce' for all domains A
in MyCat.
Regards,
Bill Page.
Ralf Hemmecke
>> it's such a big issue? Maybe for the coercion definitions, but actually,
>> that's one place where I think that Aldor is missing functionality, i.e.,
>> allow something like
>>
>> forall A if A has MyCat then CoercibleTo A
>>
>> or perhaps
>>
>> CoercibleTo A where A has MyCat.
> I presume that you mean that one might write this in the context of
> some domain, say B.
>
> Isn't this essentially what one might do in defining a package? E.g.
>
> MyCoercePac(A:MyCat,X:CatOf(B)): CoercibleTo(A)
> == add
> coerce(x:X):A == ...
You probably meant CatOf(A)...
But why so complicated? Shouldn't
MyCoercePac(A:MyCat,X:MyCat): CoercibleTo(A)
== add
coerce(x:X):A == ...
do the thing? Where exactly would you need CatOf(A)?
Ralf
Ralf Hemmecke
> different use of "CatOf(R)". If it were possible to refer directly to
> the category to which a domain belongs, then implementing something
> similar to Aldor 'extend' would be easy in Spad
> MyInteger():CatOf(Integer) with
> ...
> == Integer add
> ...
OK, that should work if CatOf exists. But now suppose I want MyInteger
to have a representation that is given by sticks, i.e. the integer 5 is
represented in MyInteger as 11111 (or rather as the string "11111". Now,
please implement MyInteger with this representation. (You are not
allowed to look up the source code of Integer in order to find out what
exports Integer provides. All you have is CatOf.
If you manage to get MyInteger done, I will be surprised.
> The domain MyInteger is then an extension of Integer.
Yes that would be one use of CatOf, but "extend" is better. (IMHO)
> In less abstract terms 'S:CatOf(Integer)' simply means that everywhere
> I use 'S' I can treat it exactly like 'Integer' even though it may be
> a conceptually distinct domain. An example of something like this
> already in the the FriCAS library is 'RomanNumeral'.
And why not write IntegerNumberSystem instead of CatOf(Integer)? I don't
see the gain of CatOf.
>>> I would much prefer that we have some theory and a model for Spad
>>> for which we can (at least in principle) prove that it provides at least
>>> the generality that is necessary to express a very large part of modern
>>> mathematics. As you know, I have frequently promoted the idea that
>>> mathematical category theory provides such a model. And it turns out
>>> that the concept of SubDomain is a very critical part of such a model.
>> Can you somehow turn your ideas into code? Suppose you have a
>> perfect SPAD (call it SPAD-CAT).
>
> Yes, I am continuing to think about that. For example I have given an
> example on axiom-wiki of Spad code that implements data structures
> similar to Record and Union based on categorical products and
> co-products.
>
> http://axiom-wiki.newsynthesis.org/LimitsAndColimits
Now, I guess you are saying that Product and Sum should be taken as
primitives in SPAD-CAT and not Record and Union. Your implementation is
not really what I was asking for. Now take your Product and Sum and show
some code where it is superior to Record and Union. (If you like you can
assume that Product and Sum work for arbitrarily many arguments. It's
compiler supported in SPAD-CAT.)
>> How would a polynomial domain in infinitely many variables over
>> some coefficient ring look like. Make it concrete.
>
> Re: "polynomial domain in infinitely many variables" ??? Isn't that
> exactly what the domain 'Polynomial' is FriCAS is already? I don't see
> that as a concrete example of what I am talking about.
OK. I want a polynomial domain where every integer i is a variable (for
better readability denote the variable i by x_i. Coefficients can come
from any ring. No other variables are allowed. So in some sense the
polynomial domain I am asking for does not allow kernels to count as
variables. And you should program it in SPAD-CAT, not in SPAD. In SPAD
we know. But how would it look like in a more categorical oriented
language SPAD-CAT (the language you dream of)?
> For example, in the case of 'Product(X,Y)' the operation that is
> required to exist and be uniquely defined is
>
> product: (A:Type, A->X,A->Y) -> (A->%)
>
> for any domain A and functions A->X, A->Y.
But I don't see how that helps me with programming. I don't just want to
model a language but also use it later for concrete programs.
Ralf
Martin Rubey
But A has CoercibleTo B will be false...
(we had this discussion very recently)
Martin
Bill Page
>> >
>> > forall A if A has MyCat then CoercibleTo A
>> >
> Bill Page writes:
>> I presume that you mean that one might write this in the context
>> of some domain, say B.
>>
>> Isn't this essentially what one might do in defining a package?
>> E.g.
>>
>> MyCoercePac(A:MyCat,X:CatOf(B)): CoercibleTo(A)
>> == add
>> coerce(x:X):A == ...
>>
>> At least in the interpreter if 'MyCoercePac' is exposed than the
>> interpreter can expect to find a function 'coerce' for all domains
>> A in MyCat.
>
There is an error my example. We can not just use 'CoercibleTo(A)'
here since it refers to %. Also there is no 'CatOf' category
constructor in FriCAS. So we have to write:
MyCatCoercePac(A:MyCat, B:SetCategory): with
coerce:B->A
== add
coerce(x:B):A == ...
On Wed, Dec 10, 2008 at 9:21 AM, Martin Rubey wrote:
> But A has CoercibleTo B will be false...
Perhaps you meant to write: "But B has CoercibleTo A will be
false..."? If so, in my proposal that is correct.
You want to create a situation where a given domain, say B, is known
to be coercible to any domain in some category MyCat without having to
explicitly list all the domains that have MyCat, e.g.
Join(CoercibleTo(A1), CoercibleTo(A2), ... )
where A1 has MyCat and A2 has MyCat, etc. In B you also provide an
implementation for all of these coercions.
Right?
Now in some new domain or in the interpreter instead of checking for
'B has CoercibleTo(A)' you could just check for 'A has MyCat' and
import MyCatCoercePac.
> (we had this discussion very recently)
I thought that discussion ended without any definite conclusion.
Regards,
Bill Page.
Bill Page
>>> forall A if A has MyCat then CoercibleTo A
>
>> I presume that you mean that one might write this in the context
>> of some domain, say B.
>>
>> Isn't this essentially what one might do in defining a package?
>> E.g.
>>
>> MyCoercePac(A:MyCat,X:CatOf(B)): CoercibleTo(A)
>> == add
>> coerce(x:X):A == ...
>
On Wed, Dec 10, 2008 at 6:41 AM, Ralf Hemmecke wrote:
> You probably meant CatOf(A)...
>
No. I meant 'X:CatOf(B)', i.e. X is a domain that has the same
category as the domain B. Martin's original example did not specify
the domain where the statement:
forall A if A has MyCat then CoercibleTo A
occurs. I just said, let the domain that uses this expression be
called B. Then I want to make a kind of "extension" of B via a
package.
> But why so complicated? Shouldn't
>
> MyCoercePac(A:MyCat,X:MyCat): CoercibleTo(A)
> == add
> coerce(x:X):A == ...
>
> do the thing?
Well,
MyCoercePac(A:MyCat,X:SetCategory): CoercibleTo(A)
== add
coerce(x:X):A == ...
would be almost the same time, but it is no longer specific to B so I
can not depend on using much of the functionality that is exported by
B.
> Where exactly would you need CatOf(A)?
That is the reason why it has to be 'CatOf(B)'
Regards,
Bill Page.
Ralf Hemmecke
> category as the domain B. Martin's original example did not specify
> the domain where the statement:
>
> forall A if A has MyCat then CoercibleTo A
>
> occurs. I just said, let the domain that uses this expression be
> called B. Then I want to make a kind of "extension" of B via a
> package.
>
>> But why so complicated? Shouldn't
>>
>> MyCoercePac(A:MyCat,X:MyCat): CoercibleTo(A)
>> == add
>> coerce(x:X):A == ...
>>
>> do the thing?
>
> Well,
>
> MyCoercePac(A:MyCat,X:SetCategory): CoercibleTo(A)
> == add
> coerce(x:X):A == ...
>
> would be almost the same time, but it is no longer specific to B so I
> can not depend on using much of the functionality that is exported by
> B.
Really? But at the time you write the code you know the definition of B,
i.e. you know its type (which is, for example, SomeCat). Why can't you
write "X: SomeCat" instead of your "X: SetCategory" above?
>> Where exactly would you need CatOf(A)?
> That is the reason why it has to be 'CatOf(B)'
I am still not convinced. I must be missing something in your
argumentation. I simply don't see how it is possible to have (at the
time I write a program) a domain B defined somewhere and I would be
unable to explicitly write down its type. The only thing I would need is
"grep" but no SPAD compiler.
That is why I constantly try to rewrite your code and remove CatOf with
something that I would deem possible. I need an example that I cannot
rewrite in order to understand the need of CatOf. (Connection with
"extend" I don't accept since I'd rather like to stay as compatible with
Aldor as possible.)
Ralf
Bill Page
>> The original use case that I presented in another thread involved a
>> different use of "CatOf(R)". If it were possible to refer directly to
>> the category to which a domain belongs, then implementing
>> something similar to Aldor 'extend' would be easy in Spad
>
>> MyInteger():CatOf(Integer) with
>> ...
>> == Integer add
>> ...
On Wed, Dec 10, 2008 at 7:02 AM, Ralf Hemmecke wrote:
> OK, that should work if CatOf exists. But now suppose I want
> MyInteger to have a representation that is given by sticks, i.e. the
> integer 5 is represented in MyInteger as 11111 (or rather as the
> string "11111". Now, please implement MyInteger with this
> representation. (You are not allowed to look up the source code
> of Integer in order to find out what exports Integer provides.
> All you have is CatOf.
Since this is supposed to be an *extension* of Integer the underlying
representation can not change. Therefore I suppose that you do not
mean "representation" but rather "presentation", i.e. how a value of
MyInteger is to be displayed. That's easy - just override the coercion
to OutputForm.
(1) -> )sys cat myint.spad
)abbrev domain MYINT MyInteger
MyInteger(): Join(IntegerNumberSystem, ConvertibleTo String, OpenMath,_
Canonical, canonicalsClosed) with
coerce: % -> OutputForm
coerce: % -> Integer
== Integer add
coerce(x:%):OutputForm == message(concat(["1" for i in
1..abs(x)::Integer]))$OutputForm
coerce(x:%):Integer == x pretend Integer
(1) -> )co myint.spad
Compiling FriCAS source code from file /home/wspage/myint.spad using
old system compiler.
MYINT abbreviates domain MyInteger
------------------------------------------------------------------------
MyInteger is already explicitly exposed in frame frame0
MyInteger will be automatically loaded when needed from
/home/wspage/MYINT.NRLIB/MYINT
(1) -> 3$MyInteger
Loading /home/wspage/MYINT.NRLIB/MYINT for domain MyInteger
(1) 111
Type: MyInteger
>
> If you manage to get MyInteger done, I will be surprised.
>
Perhaps I misunderstood your request. :-(
>> The domain MyInteger is then an extension of Integer.
>
> Yes that would be one use of CatOf, but "extend" is better. (IMHO)
>
Yes, agree. But my point is that 'CatOf' at least makes this much possible.
>> In less abstract terms 'S:CatOf(Integer)' simply means that
>> everywhere I use 'S' I can treat it exactly like 'Integer' even though
>> it may be a conceptually distinct domain. An example of something
>> like this already in the the FriCAS library is 'RomanNumeral'.
>
> And why not write IntegerNumberSystem instead of CatOf(Integer)?
> I don't see the gain of CatOf.
>
Because 'CatOf(Integer)' is
Join(IntegerNumberSystem, ConvertibleTo String, OpenMath, Canonical,
canonicalsClosed)
>>
>> http://axiom-wiki.newsynthesis.org/LimitsAndColimits
>
> Now, I guess you are saying that Product and Sum should be taken
> as primitives in SPAD-CAT and not Record and Union.
Yes.
> Your implementation is not really what I was asking for. Now take
> your Product and Sum and show some code where it is superior
> to Record and Union. (If you like you can assume that Product
> and Sum work for arbitrarily many arguments. It's compiler supported
> in SPAD-CAT.)
>
If Product and Sum where built-in to some new version of SPAD they
would include the 'product' and 'sum' operations as an inherent part
of their definition. The existence of these operations is dictated by
describing them as categorical limits. So for example
f:Sum(Integer,Float)->Integer:=sum(abs$Integer,wholePart$Float)
That takes either an Integer or Float as argument and evaluates either
'abs' or 'wholePart' respectively to return an Integer.
(9) -> f(-1)
1
Type: PositiveInteger
(10) -> f(3.14)
3
Type: PositiveInteger
See: http://axiom-wiki.newsynthesis.org/LimitsAndColimits
This is written in Aldor because Aldor has somewhat better support for
Union than FriCAS.
Then for example the definition of a simple piecewise function might
look like this:
p:Sum(NegativeInteger,ZeroInteger,PositiveInteger)->Integer :=
sum(Integer,x +-> -(x^2), x +-> 0,x +-> x^2)
>>> How would a polynomial domain in infinitely many variables over
>>> some coefficient ring look like. Make it concrete.
>>
>> Re: "polynomial domain in infinitely many variables" ??? Isn't that
>> exactly what the domain 'Polynomial' is FriCAS is already? I don't
>> see that as a concrete example of what I am talking about.
>
> OK. I want a polynomial domain where every integer i is a variable
> (for better readability denote the variable i by x_i. Coefficients can
> come from any ring. No other variables are allowed. So in some
> sense the polynomial domain I am asking for does not allow kernels
> to count as variables. And you should program it in SPAD-CAT, not
> in SPAD. In SPAD we know. But how would it look like in a more
> categorical oriented language SPAD-CAT (the language you dream
> of)?
>
What makes you think that polynomials of the kind you describe should
look different in a more categorical-oriented language? I don't see
it.
>> For example, in the case of 'Product(X,Y)' the operation that is
>> required to exist and be uniquely defined is
>>
>> product: (A:Type, A->X,A->Y) -> (A->%)
>>
>> for any domain A and functions A->X, A->Y.
>
> But I don't see how that helps me with programming. I don't just want
> to model a language but also use it later for concrete programs.
>
Generally speaking, higher-order functions like 'product' and 'sum'
help to make Spad in a more functionally-oriented language. Functional
programming is no longer just a "model language" and certainly used in
concrete programming problems.
Regards,
Bill Page.
Ralf Hemmecke
>> Bill Page wrote:
>>> The original use case that I presented in another thread involved a
>>> different use of "CatOf(R)". If it were possible to refer directly to
>>> the category to which a domain belongs, then implementing
>>> something similar to Aldor 'extend' would be easy in Spad
>>> MyInteger():CatOf(Integer) with
>>> ...
>>> == Integer add
>>> ...
>
> On Wed, Dec 10, 2008 at 7:02 AM, Ralf Hemmecke wrote:
>> OK, that should work if CatOf exists. But now suppose I want
>> MyInteger to have a representation that is given by sticks, i.e. the
>> integer 5 is represented in MyInteger as 11111 (or rather as the
>> string "11111". Now, please implement MyInteger with this
>> representation. (You are not allowed to look up the source code
>> of Integer in order to find out what exports Integer provides.
>> All you have is CatOf.
>
> Since this is supposed to be an *extension* of Integer the underlying
> representation can not change.
Bill, I've already agreed, that as *extension* CatOf might be useful.
(But still I would prefer the Aldor "extend" in order to stay compatible.
I want a use case that is not connected to extension.
> Perhaps I misunderstood your request. :-(
Yep. I really meant "representation" instead of "presentation" and I
certainly did not want "extension".
> Yes, agree. But my point is that 'CatOf' at least makes this much
> possible.
No question about that.
Ralf
Waldek Hebisch
>
> > One remark: if we want just preserve existing functionality,
> > then the simplest way is probably to remove the third argument to
> > Localize and LocalAlgebra. Namely, currentlty there is probably
> > no way to create nontrivial domain of SubsetCategory, so the
> > in working code third argument will be the same as the second
> > one.
>
> Oh, good that you yourself say this. I was exactly thinking in this
> direction and wanted to create a two parameter Localize and LocalAlgebra
> (*in addition*, in order not to break other people's code that relies on
> 3-parameter version).
>
In Spad there is no overloading of constructors, so we can only
have one version of Localize and LocalAlgebra.
> But yes, I am very much in favour of removing the third parameter. Or
> rather to replace it with a boolean function in the following sense
> (It's similar to SubDomain.):
>
> Instead of
>
> Localize(M:Module R,
> R:CommutativeRing,
> S:SubsetCategory(Monoid, R)): Module R with
>
> we would have
>
> Localize(M:Module R,
> R:CommutativeRing,
> denominator?: R -> Boolean): Module R with
>
> where denominator is the characteristic function for the subset S of R
> that can be used for denominators.
>
> Of course, there is a big problem: It cannot be ensured that the set of
> all r for which denominator?(r) returns true is indeed a sub-monoid of
> R.
<snip>
> > So it seems that the only current
> > use of Localize and LocalAlgebra is via Fraction.
>
> In this case, I would even go to the extreme and remove LocalAlgebra and
> Localize completely. If somebody later sees some need for their
> reimplementation then we have someone who is familiar with all the
> issues and who knows probably some use cases that should work.
>
I am tempted to apply the patch below which just removes the
third argument. Why:
1) Adding extra function for membership test _may_ be a good idea.
However, I am reluctant to add untested and unused code, while
proper developement (including creating test domain which actually
uses new functionlity) would take a bit more time that
I want to spent on this.
2) I think that Localize and LocalAlgebra represent important
concept and that current domain may be good start for future
developement. So I am not eager to remove them.
BTW: the patch passes all tests and AFAICS should cause no
performance difference.
diff -ru trunk.bb/src/algebra/fraction.spad.pamphlet trunk/src/algebra/fraction.spad.pamphlet
--- trunk.bb/src/algebra/fraction.spad.pamphlet 2008-12-13 19:28:26.000000000 +0100
+++ trunk/src/algebra/fraction.spad.pamphlet 2008-12-13 19:47:37.000000000 +0100
@@ -24,28 +24,27 @@
++ Description: Localize(M,R,S) produces fractions with numerators
++ from an R module M and denominators from some multiplicative subset
++ D of R.
-Localize(M:Module R,
- R:CommutativeRing,
- S:SubsetCategory(Monoid, R)): Module R with
+Localize(M : Module R,
+ R : CommutativeRing): Module R with
if M has OrderedAbelianGroup then OrderedAbelianGroup
- _/ :(%,S) -> %
+ _/ : (%, R) -> %
++ x / d divides the element x by d.
- _/ :(M,S) -> %
+ _/ : (M, R) -> %
++ m / d divides the element m by d.
numer: % -> M
++ numer x returns the numerator of x.
- denom: % -> S
+ denom: % -> R
++ denom x returns the denominator of x.
==
add
--representation
- Rep:= Record(num:M,den:S)
+ Rep:= Record(num : M, den : R)
--declarations
- x,y: %
+ x, y: %
n: Integer
m: M
r: R
- d: S
+ d: R
--definitions
0 == [0,1]
zero? x == zero? (x.num)
@@ -62,7 +61,7 @@
n*x == [n*x.num,x.den]
r*x == if r=x.den then [x.num,1] else [r*x.num,x.den]
x/d ==
- zero?(u:S:=d*x.den) => error "division by zero"
+ zero?(u:R:=d*x.den) => error "division by zero"
[x.num,u]
m/d == if zero? d then error "division by zero" else [m,d]
coerce(x:%):OutputForm ==
@@ -92,19 +91,18 @@
++ Description: LocalAlgebra produces the localization of an algebra, i.e.
++ fractions whose numerators come from some R algebra.
LocalAlgebra(A: Algebra R,
- R: CommutativeRing,
- S: SubsetCategory(Monoid, R)): Algebra R with
+ R: CommutativeRing): Algebra R with
if A has OrderedRing then OrderedRing
- _/ : (%,S) -> %
+ _/ : (%,R) -> %
++ x / d divides the element x by d.
- _/ : (A,S) -> %
+ _/ : (A,R) -> %
++ a / d divides the element \spad{a} by d.
numer: % -> A
++ numer x returns the numerator of x.
- denom: % -> S
+ denom: % -> R
++ denom x returns the denominator of x.
- == Localize(A, R, S) add
- 1 == 1$A / 1$S
+ == Localize(A, R) add
+ 1 == 1$A / 1$R
x:% * y:% == (numer(x) * numer(y)) / (denom(x) * denom(y))
characteristic() == characteristic()$A
@@ -315,7 +313,7 @@
if S has Canonical and S has GcdDomain and S has canonicalUnitNormal
then Canonical
++ \spad{Canonical} means that equal elements are in fact identical.
- == LocalAlgebra(S, S, S) add
+ == LocalAlgebra(S, S) add
Rep:= Record(num:S, den:S)
coerce(d:S):% == [d,1]
zero?(x:%) == zero? x.num
diff -ru trunk.bb/src/algebra/solverad.spad.pamphlet trunk/src/algebra/solverad.spad.pamphlet
--- trunk.bb/src/algebra/solverad.spad.pamphlet 2008-12-13 19:28:26.000000000 +0100
+++ trunk/src/algebra/solverad.spad.pamphlet 2008-12-13 19:49:19.000000000 +0100
@@ -35,7 +35,6 @@
ST ==> String
PR ==> Polynomial R
UP ==> SparseUnivariatePolynomial PR
- LA ==> LocalAlgebra(PR, Z, Z)
RF ==> Fraction PR
RE ==> Expression R
EQ ==> Equation
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Ralf Hemmecke
> third argument. Why:
>
> 1) Adding extra function for membership test _may_ be a good idea.
> However, I am reluctant to add untested and unused code, while
> proper developement (including creating test domain which actually
> uses new functionlity) would take a bit more time that
> I want to spent on this.
As long as SubsetCategory is removed that is OK.
> 2) I think that Localize and LocalAlgebra represent important
> concept and that current domain may be good start for future
> developement. So I am not eager to remove them.
So be it.
> BTW: the patch passes all tests and AFAICS should cause no
> performance difference.
Still, I don't accept your patch if you are not going to also change the
documentation. Interestingly, there is only need to change for Localize.
Here my replacement:
++ Description: Localize(M,R) produces fractions with numerators
++ from an R module M and denominators being the nonzero elements of R.
Waldek, will you then start hunting down the handling of SubsetCategory
and also remove that code from FriCAS?
Ralf
Waldek Hebisch
>
> > I am tempted to apply the patch below which just removes the
> > third argument.
> As long as SubsetCategory is removed that is OK.
>
> So be it.
>
> > BTW: the patch passes all tests and AFAICS should cause no
> > performance difference.
>
> Still, I don't accept your patch if you are not going to also change the
> documentation. Interestingly, there is only need to change for Localize.
> Here my replacement:
>
> ++ Description: Localize(M,R) produces fractions with numerators
> ++ from an R module M and denominators being the nonzero elements of R.
>
OK, thanks.
> Waldek, will you then start hunting down the handling of SubsetCategory
> and also remove that code from FriCAS?
>
Yes, that is the plan.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Ralf Hemmecke
> would include the 'product' and 'sum' operations as an inherent part
> of their definition. The existence of these operations is dictated by
> describing them as categorical limits. So for example
> See: http://axiom-wiki.newsynthesis.org/LimitsAndColimits
> Then for example the definition of a simple piecewise function might
> look like this:
>
> p:Sum(NegativeInteger,ZeroInteger,PositiveInteger)->Integer :=
> sum(Integer,x +-> -(x^2), x +-> 0,x +-> x^2)
That looks nice. But, of course it involves quite a lot. (You have
demonstrated that by the package Sum2Functions.) Namely, if I define (or
rather just use) for two domains X and Y the type Sum(X, Y), then for
every other domain A the compiler would know about a function
sum: (X->A,Y->A) -> Sum(X,Y)->A
(of course *without* the need of some package like Sum2Functions).
But then Sum and Product are just special cases of (Co-)Limits. So maybe
a Limit and CoLimit constructor should be built-in to the language. My
question would then be, does such a general construction allow to
recover the concret handling of Record/Cross/Union etc.? (Record, Cross,
and Union would then, of course, not be built-in.) By "concrete" I don't
just mean theoretically, but it rather concerns the question how could
this Limit stuff really be implemented into the compiler?
> What makes you think that polynomials of the kind you describe should
> look different in a more categorical-oriented language? I don't see
> it.
Invent some other concrete application for which you could demonstrate
the benefit of the categorical programming language SPAD-CAT. Your
example, I cited above, is already something. Other examples?
Ralf
Bill Page
> Bill Page wrote:
>
>> Then for example the definition of a simple piecewise function
>> might look like this:
>>
>> p:Sum(NegativeInteger,ZeroInteger,PositiveInteger)->Integer :=
>> sum(Integer,x +-> -(x^2), x +-> 0,x +-> x^2)
>
> That looks nice. But, of course it involves quite a lot. (You have
> demonstrated that by the package Sum2Functions.) Namely, if
> I define (or rather just use) for two domains X and Y the type
> Sum(X, Y), then for every other domain A the compiler would
> know about a function
>
> sum: (X->A,Y->A) -> Sum(X,Y)->A
>
> (of course *without* the need of some package like Sum2Functions).
>
I do not think that implementing co-product and product involves
anything really new. The function 'sum' is very "natural". It is
exactly what you would expect it to be if you first evaluated one
function and then another in "series". It is dual to the also very
natural idea of evaluating two functions in "parallel" implemented by
'product'.
>
> But then Sum and Product are just special cases of (Co-)Limits. So
> maybe a Limit and CoLimit constructor should be built-in to the
> language.
There is a theorem called the "existence theorem for limits" which
says that for a category to have all limits, it is sufficient that it
have products and equalizers. So one gains essentially nothing by
generalizing to all limits. On the other hand, an equalizer is a
rather complex thing - it corresponds to the largest subdomain A' over
which two functions evaluate to the same value. I.E.
f:A->B
g:A->B
h:A'->A
f h = g h
Finding h:A'->A is what we would normally call "solving" an equation.
Co-equalizers on the other hand are a generalization of the process of
unification of terms - something that is very important in symbolic
processing.
> My question would then be, does such a general construction allow
> to recover the concrete handling of Record/Cross/Union etc.? (Record,
> Cross, and Union would then, of course, not be built-in.) By "concrete"
> I don't just mean theoretically, but it rather concerns the question how
> could this Limit stuff really be implemented into the compiler?
>
Record and Cross can be easily recovered from Product. And Union from
Sum. The problem is the equalizer (and co-equalizer). To implement
these in the most general case, one needs a large part of what
normally constitutes a complete computer algebra system.
> ...
> Invent some other concrete application for which you could
> demonstrate the benefit of the categorical programming language
> SPAD-CAT. Your example, I cited above, is already something.
> Other examples?
>
I suspect that most of the benefits are conceptual. These might be
rather difficult to capture in concrete examples but I will let you
know when I find anything worth sharing. In the mean time I might try
to take up Waldek's challenge to give a possible treatment of
piecewise polynomial functions.
Regards,
Bill Page.