On Sat, Dec 6, 2008 at 4:02 AM, Ralf Hemmecke wrote:
>
> 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.
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected]
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en
-~----------~----~----~----~------~----~------~--~---
