Re: aldor pull request #120

6 views
Skip to first unread message

Ralf Hemmecke

unread,
Jan 27, 2017, 4:41:07 PM1/27/17
to aldor-devel
Hi Peter (and others),

I've seen that you have introduced several folding packages.
And you use "with" as type what otherwise was often "Type".


FoldingTransformationCategory2(T: with, R: with): Category == with {..}
^^^^ ^^^^

I like that, but it reminds me at a definition done by Saul Youssef.

http://axiom-wiki.newsynthesis.org/SandBoxAldorCategoryTheory

namely,

define Domain:Category == with;

Shouldn't we introduce this category as the root of all domains?

Any comments?

Ralf

Peter Broadbery

unread,
Jan 27, 2017, 6:06:28 PM1/27/17
to Ralf Hemmecke, aldor-devel
Possibly I could have declared the arguments to be of type Type for
FoldingTransformationCategory;I preferred "with" simply because I
didn't want to worry about types being passed in.

What advantage is there to having an explicit name for the category
with no operations?
> --
> You received this message because you are subscribed to the Google Groups "aldor-devel" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to aldor-devel...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Ralf Hemmecke

unread,
Jan 27, 2017, 7:17:31 PM1/27/17
to aldor...@googlegroups.com
On 01/28/2017 12:05 AM, Peter Broadbery wrote:
> Possibly I could have declared the arguments to be of type Type for
> FoldingTransformationCategory;I preferred "with" simply because I
> didn't want to worry about types being passed in.
>
> What advantage is there to having an explicit name for the category
> with no operations?

https://github.com/pippijn/aldor/blob/master/aldor/lib/axllib/src/al/except.as#L9

define Exception: Category == with {}

I am a bit surprised that *you* are asking this. I would have bet that
you introduced the Exception category. ;-)

Anyway, yes, somehow for this reason: not writing Type where a Domain is
required. Simply writing "with" is not telling enough for my taste.
So the category Domain would be the type of all domains. (Somehow like
the keyword Category is the type of all categories.
Well, of course, one can now argue that exceptions are also domains. But
having Exception and Domain as categories, makes it more clear what the
purpose of the type is. It's just one bit of information more.

Ralf

Ralf Hemmecke

unread,
Jan 28, 2017, 12:26:42 PM1/28/17
to aldor-devel, Peter Broadbery
On 01/28/2017 12:05 AM, Peter Broadbery wrote:
> What advantage is there to having an explicit name for the category
> with no operations?

Look at

https://github.com/pippijn/aldor/blob/master/aldor/lib/aldor/src/datastruc/sal_table.as#L77

define TableType(K:PrimitiveType, V:Type): Category ==
BoundedFiniteDataStructureType Cross(K, V) with {
if K has InputType and V has InputType then InputType;
...

As far as I understand Type is the type of categories and domains. So I
am allowed to use

TableType(Integer, PrimitiveType)

right?

But as far as I read the Aldor User Guide, there is no specification for
the meaning of

V has InputType

if V is a category.

Page 96 of http://www.aldor.org/docs/aldorug.pdf

So either this specification is extended to "category valued
expressions" in the first argument (yielding false for "has") or
it makes sense to restrict to "V: Domain".

Opinions?

Ralf

Peter Broadbery

unread,
Jan 28, 2017, 1:56:45 PM1/28/17
to Ralf Hemmecke, aldor-devel, Peter Broadbery
The implementation of exceptions in the type system is not something
I'm too happy with - it allows inheritance, but that is it's only
advantage. I don't think they are a strong argument for adding
additional special types into the core language -- and definitely not
as part of this pull request.

In the case of table - : Type is a bit special (obviously), and
perhaps the user guide should be tweaked such that it's clear that T
is "domain-valued" if T is declared to be Type.

In any case, I might change the Fold operations to use X: Type, as I
can see some potential use cases.

Waldek Hebisch

unread,
Jan 28, 2017, 2:20:40 PM1/28/17
to aldor...@googlegroups.com
Ralf Hemmecke wrote:
>
> Look at
>
> https://github.com/pippijn/aldor/blob/master/aldor/lib/aldor/src/datastruc/sal_table.as#L77
>
> define TableType(K:PrimitiveType, V:Type): Category ==
> BoundedFiniteDataStructureType Cross(K, V) with {
> if K has InputType and V has InputType then InputType;
> ...
>
> As far as I understand Type is the type of categories and domains. So I
> am allowed to use
>
> TableType(Integer, PrimitiveType)
>
> right?
>
> But as far as I read the Aldor User Guide, there is no specification for
> the meaning of
>
> V has InputType
>
> if V is a category.
>
> Page 96 of http://www.aldor.org/docs/aldorug.pdf
>
> So either this specification is extended to "category valued
> expressions" in the first argument (yielding false for "has") or
> it makes sense to restrict to "V: Domain".
>

I usualy consider categories to _not_ be of "first class". In
particular, that would exclude categories as arguments of
constructors. Can you give resonable example when one would
like to pass category as an argument to a constructor?

--
Waldek Hebisch

Peter Broadbery

unread,
Jan 28, 2017, 5:40:59 PM1/28/17
to Waldek Hebisch, aldor...@googlegroups.com
It does depend on your definition of reasonable, but a simple example would be:

import from List PrimitiveType
-- random things from random types
for T in [Integer, String, IntegerMod 10] repeat
stdout << random()$T << newline

Replace PrimitiveType with a more complex category, and random() with
a generic calculation in that category and you get a way of testing an
algorithm over a number of domains. If the list was obtained by
reflection on the library (which might be feasible in fricas), then
it's a way of getting test coverage across less used domains.

Ralf Hemmecke

unread,
Jan 28, 2017, 6:11:55 PM1/28/17
to aldor...@googlegroups.com
On 01/28/2017 11:40 PM, Peter Broadbery wrote:
> import from List PrimitiveType -- random things from random types for
> T in [Integer, String, IntegerMod 10] repeat stdout << random()$T <<
> newline

Thank you, Peter.

I also had List PrimitiveType in mind. I faintly remember that there
once was a discussion where I criticized List(T: Type) because of "has"
expressions in the respective category. I don't remember whether I ran
into a bug, but I definitely find the specification of "has"
not understandible (correct?) if the aldor compiler accepts
(as in ListType(PrimitiveType), i.e., T is the category PrimitiveType)

if T has PrimitiveType then {
find: (T, %) -> (%, Z);

> In the case of table - : Type is a bit special (obviously), and
> perhaps the user guide should be tweaked such that it's clear that T
> is "domain-valued" if T is declared to be Type.

Well, then the term "domain-valued" means "is a category or a domain".
If this was the original idea for the first argument of "has", then I'm
fine with it, but the Aldor User Guide should definitely not use
"domain-valued", since that had (at least me) confused up to today.

> I don't think they are a strong argument for adding additional
> special types into the core language -- and definitely not as part of
> this pull request.

Oh no... I was not saying to add a keyword "Domain". I am just in favour
of adding

define Domain: Category == with;

to the standard library.

For my taste "Domain" is just a bit more telling then "with", in
particular in situations where one just wants to say that the thing can
be a domain, but not a category.

Ralf

Peter Broadbery

unread,
Jan 30, 2017, 4:05:23 PM1/30/17
to Ralf Hemmecke, aldor...@googlegroups.com
On 28 January 2017 at 23:11, Ralf Hemmecke <ra...@hemmecke.org> wrote:
> On 01/28/2017 11:40 PM, Peter Broadbery wrote:
>> import from List PrimitiveType -- random things from random types for
>> T in [Integer, String, IntegerMod 10] repeat stdout << random()$T <<
>> newline
>
> Thank you, Peter.
>
> I also had List PrimitiveType in mind. I faintly remember that there
> once was a discussion where I criticized List(T: Type) because of "has"
> expressions in the respective category. I don't remember whether I ran
> into a bug, but I definitely find the specification of "has"
>
> Page 96 of http://www.aldor.org/docs/aldorug.pdf
>
> not understandible (correct?) if the aldor compiler accepts
> (as in ListType(PrimitiveType), i.e., T is the category PrimitiveType)
>
> if T has PrimitiveType then {
> find: (T, %) -> (%, Z);
>
>> In the case of table - : Type is a bit special (obviously), and
>> perhaps the user guide should be tweaked such that it's clear that T
>> is "domain-valued" if T is declared to be Type.
>
> Well, then the term "domain-valued" means "is a category or a domain".
> If this was the original idea for the first argument of "has", then I'm
> fine with it, but the Aldor User Guide should definitely not use
> "domain-valued", since that had (at least me) confused up to today.
>

I'll think of a suitable form of words for the user guide in a
subsequent pull request - there's the simple fix (ie. it's a type),
plus a second option which will allow more operations on domain-valued
objects, but needs a bit more thought and discussion.

>> I don't think they are a strong argument for adding additional
>> special types into the core language -- and definitely not as part of
>> this pull request.
>
> Oh no... I was not saying to add a keyword "Domain". I am just in favour
> of adding
>
> define Domain: Category == with;
>
> to the standard library.
>

Even this is a relatively large change - every domain would need it,
even the smaller ones used for testing. It is possible to add "define
Domain == with" (note the lack of :Category), and this will give you a
name to use in place of "with". It should mean exactly the same
thing, as opposed to introducing a new category.

> For my taste "Domain" is just a bit more telling then "with", in
> particular in situations where one just wants to say that the thing can
> be a domain, but not a category.
>

I think we have to disagree here - I do see your point, but then
consider the use of
"with" in constructors - eg F(X: with { 1: %}).. would you insist on
putting "Domain" in front of the with?

> Ralf

Ralf Hemmecke

unread,
Jan 30, 2017, 5:00:42 PM1/30/17
to aldor...@googlegroups.com
On 01/30/2017 10:04 PM, Peter Broadbery wrote:
>> Well, then the term "domain-valued" means "is a category or a domain".
>> If this was the original idea for the first argument of "has", then I'm
>> fine with it, but the Aldor User Guide should definitely not use
>> "domain-valued", since that had (at least me) confused up to today.
>>
>
> I'll think of a suitable form of words for the user guide in a
> subsequent pull request - there's the simple fix (ie. it's a type),
> plus a second option which will allow more operations on domain-valued
> objects, but needs a bit more thought and discussion.

Thanks.

>>> I don't think they are a strong argument for adding additional
>>> special types into the core language -- and definitely not as part of
>>> this pull request.
>>
>> Oh no... I was not saying to add a keyword "Domain". I am just in favour
>> of adding
>>
>> define Domain: Category == with;
>>
>> to the standard library.
>>
>
> Even this is a relatively large change - every domain would need it,
> even the smaller ones used for testing. It is possible to add "define
> Domain == with" (note the lack of :Category), and this will give you a
> name to use in place of "with". It should mean exactly the same
> thing, as opposed to introducing a new category.

Oh. Good. Now perhaps I will learn the difference between

define Domain: Category == with; (A)

and

define Domain == with; (B)

To be honest, I didn't get the difference. And there would be something
else:

macro Domain == with; (C)

I probably understand (A) and (C), but how exactly do they differ from (B)?

I guess, I would be happy with (B) if it gives me a way to restrict an
argument to domains (in contrast to categories) and is more telling than
with in a situation like "Foo(D: with)".

>> For my taste "Domain" is just a bit more telling then "with", in
>> particular in situations where one just wants to say that the thing can
>> be a domain, but not a category.

> I think we have to disagree here - I do see your point, but then
> consider the use of
> "with" in constructors - eg F(X: with { 1: %}).. would you insist on
> putting "Domain" in front of the with?

Well, in fact, yes. Or rather yes and no. Surely, "Domain" wouldn't add
much information, but on the other hand I'd argue that "1: %" is also
meaningless in the sense that the axioms are missing. Unfortunately,
Aldor doesn't allow me to require some axioms that must be fulfilled.
For example, if I want

F(X: with {+: (%, %) -> %})

then most people will think that + should be an assosiative and
commutative operation. BUT, the compiler cannot check this requirement.
Now if we had

AssociativePlust: Category == with {+: (%, %) -> %}
CommutativePlust: Category == with {+: (%, %) -> %}

then I could write

F(X: Join(AssociativePlus, CommutativePlus)

Yes, that is only a trick to add a bit of meaning to the code that can
be checked by the compiler. Yes that would be cumbersome to write, and I
would be much more happy if I could express commutativity in the Aldor
language by a logical formula, but just writing

F(X: with {+: (%, %) -> %})

is nothing that is algebraically much helpful.

I would want "Domain" to have something similar to "Category" and (as a
bigger wish) I want an option to express axioms of operations in Aldor.

Ralf

Waldek Hebisch

unread,
Feb 1, 2017, 12:46:52 PM2/1/17
to aldor...@googlegroups.com
Peter Broadbery wrote:
>
> It does depend on your definition of reasonable, but a simple example would be:
>
> import from List PrimitiveType
> -- random things from random types
> for T in [Integer, String, IntegerMod 10] repeat
> stdout << random()$T << newline

Thanks. I find it quite reasonable -- actually I was thinking
about storing types in aggregates but somewhat forgot about
that.

So it seems that has should be defined for categories and
return appropiate values (corresponding to operations that
one can do on types), like

Group has Group ---> false
Group has Category ---> true
Group has Type ---> true

I am not sure is current runtimes (Aldor and FriCAS) support
this...

--
Waldek Hebisch

Waldek Hebisch

unread,
Feb 1, 2017, 12:55:30 PM2/1/17
to aldor...@googlegroups.com
Ralf Hemmecke wrote:
>
> Oh no... I was not saying to add a keyword "Domain". I am just in favour
> of adding
>
> define Domain: Category == with;
>
> to the standard library.
>
> For my taste "Domain" is just a bit more telling then "with", in
> particular in situations where one just wants to say that the thing can
> be a domain, but not a category.

IIUC something is of such category only if explicietly declared.
So domains not declared as Domain would fails the test.
Concerning "with", it declares anonymous category with no
operations -- I would say that categories match that:
anoymous category is matched structually and since it
has no exports it imposes no conditions.

--
Waldek Hebisch

Peter Broadbery

unread,
Feb 1, 2017, 4:50:27 PM2/1/17
to Waldek Hebisch, aldor...@googlegroups.com
Not sure about the last two; the second argument of "has" should
really be a category, as having any type on the right would allow
things like "X has Float", which ought to be an error.
Effectively in aldor, "has" is of type "(Type, Category) -> Boolean".

This still allows things like "Ring has SetCategory", at least in theory.

Ralf Hemmecke

unread,
Feb 1, 2017, 5:13:15 PM2/1/17
to aldor-devel
> This still allows things like "Ring has SetCategory", at least in theory.

And what should be returned by this?

Now that I learned has: (Type, Category) -> Boolean, my wish would be
that it returns "true".

Ralf

Peter Broadbery

unread,
Feb 1, 2017, 5:30:45 PM2/1/17
to Ralf Hemmecke, aldor-devel
Currently, in aldor, false. It would be a fair amount of work to implement.
Reply all
Reply to author
Forward
0 new messages