Re: [fricas-devel] Re: leftover from allowing functions to return types

View: New views
3 Messages — Rating Filter:   Alert me  

Parent Message unknown Re: [fricas-devel] Re: leftover from allowing functions to return types

by Ralf Hemmecke :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message

On 11/13/2008 06:45 PM, Bill Page wrote:

> Martin,
>
> On Wed, Nov 12, 2008 at 4:33 AM, you wrote:
>> ...
>> I noticed that my spad file was flawed, it seems that I can't get Rep and
>> % right in Spad.  In aldor it's so easy... At least, now FriCAS doesn't
>> complain anymore about the Rep.
>>
>> Could we add these two macro definitions to FriCAS?  (I'd rather have
>> them as macros, not builtin as in Open-Axiom, I must admit)
>>
>> macro {
>>        rep x == ((x)@%) pretend Rep;
>>        per r == ((r)@Rep) pretend %;
>> }
>>
>
>>From my point of view these operations are an essential part of the
> SPAD language even though most of the legacy code in the Axiom library
> does not use them in a type-sage manner.
>
> Could you explain why you prefer these to be pre-defined macros rather
> than being builtin as Gaby has done in OpenAxiom and Aldor?

You should (currently) delete "and Aldor" from the last sentence.

https://svn.origo.ethz.ch/algebraist/trunk/aldor/lib/aldor/include/aldor.as

Of course, one can make these things into a language defined concept.
However, one can also consider them to be just a convention.

This % thing is rather driven by the concept of universal algebra where
Rep refers to the carrier set. It's in some sense nice, since universal
algebra comprises a lot of cases, but take, for example, zero?: % ->
Boolean. Strictly speaking, this function cannot live in a universal
algebra, since Boolean is not the carrier set.

Let's look at this

Dom: with {
   +: (%, %) -> %
   zero?: % -> Boolean
} == add { ... }

Here % refers to Dom and Boolean refers to the globally defined domain
Boolean. So why not writing

Dom2(C: T1, Boolean: T2): with {
   +: (C, C) -> C
   zero?: C -> Boolean
} == add { ... }

where for T2 one has to specify the type that Boolean must fulfil inside
Dom2 and T1 is ??? Well, T1 is a problem. But not really.
((NB. Don't be confused that in Dom2 "Boolean" is the name of a
parameter and has nothing to do with a globally defined domain of the
same name.))

I guess, one can program in Aldor without ever using %. But then Aldor
will look much more object oriented (... don't take this too serious).

In fact Dom2 looks more like a multi-sorted algebra.

Dom2 = ((C, Boolean), (+, zero?))

Speaking in Aldor-terminology, Dom2 is, however, just a package (i.e. a
domain in whose definition no % appears).

Maybe it could be fun to think a bit along these lines...

Ralf

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

Re: [fricas-devel] Re: leftover from allowing functions to return types

by Bill Page-7 :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message

On Thu, Nov 13, 2008 at 2:11 PM, Ralf Hemmecke wrote:
>Bill Page wrote:
>> Could you explain why you prefer these to be pre-defined macros
>> rather than being builtin as Gaby has done in OpenAxiom and Aldor?
>
> You should (currently) delete "and Aldor" from the last sentence.
>
> https://svn.origo.ethz.ch/algebraist/trunk/aldor/lib/aldor/include/aldor.as
>

Thanks. Point accepted. Of course, almost everything is added-on to
Aldor because really the core language itself is quite small. Still,
rep and per could be local functions instead of macros. I simply
wonder why one is preferable to the other.

> Of course, one can make these things into a language defined concept.
> However, one can also consider them to be just a convention.
>

If one wants to argue that Axiom (and Aldor) are fully typed
languages, then it seems to me that one is obliged to claim that it is
"part of the language".

> This % thing is rather driven by the concept of universal algebra where
> Rep refers to the carrier set. It's in some sense nice, since universal
> algebra comprises a lot of cases, but take, for example, zero?: % ->
> Boolean. Strictly speaking, this function cannot live in a universal
> algebra, since Boolean is not the carrier set.
>

Honestly, I do not see the need for any of this discussion of
universal algebra in the context of Axiom/Aldor. To me % is just a
convenient name for "this domain". Many other languages including Java
and Python have names like "this" or "self", or whatever. In
Axiom/Aldor it is just %.

Could you summarize again why you think it is important?

> ...

Regards,
Bill Page.

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

Parent Message unknown Re: [fricas-devel] Re: leftover from allowing functions to return types

by Bill Page-7 :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message

On Thu, Nov 13, 2008 at 3:15 PM, Ralf Hemmecke wrote:
>... it would make me happier if you could at least say whether you
> think my view is mathematically valid or not.
>

Yes, I do think that your view is mathematically valid.

> I don't say that one *needs* universal algebra, but I find that
> mathematical concept rather illuminating to understand the relation
> between domains and mathematics. UA (or rather multi-sorted algebras
> with a distinguished carrier set) is the closest mathematical concept
> (for me) that matches the "domain" concept in Aldor.
>

It think that it is "ok" as far as it goes, but I believe that it does
not go far enough. It is clear that many of the ideas in Axiom were
motivated by the concept of Abstract Data Type (ADT) that was popular
at the time of the development of Axiom's first incarnation as
ScratchPad II. I think the following paper by Jean Baillie presents
that "state of the art" as it existed at that time very well:

http://homepages.feis.herts.ac.uk/~comqejb/algspec/pr.html

Although he is publishing as a computer scientist, Baillie presents in
some detail a method for describing ADTs as many-sorted universal
algebras.

BTW, I think you can see one of the legacies of this "algebraic"
orientation in Axiom (and even in Aldor): the signatures of operations
are defined with an "arity", i.e. as functions that take multiple
arguments and return a single value. Since Axiom and Aldor contain
several "product" types (e.g. Cross, Tuple, Record, etc.) strictly
speaking this is not necessary and leads to a some awkwardness (for
example, so called courtesy coercions in Aldor).

But my point is that the implementation of these algebraic concepts in
Axiom did not get much past chapter 2 (
http://homepages.feis.herts.ac.uk/~comqejb/algspec/node3.html ).

> A mathematical category does not fit. Don't you agree?
>

No I do not agree. The (mathematical) concept of cartesian closed
categories and topoi provide tools for describing both the programming
language and data structures of Axiom/Aldor.

> Since you don't agree with my UA view, what is your closest mathematical
> thing to an Aldor domain?
>

An Aldor domain is an object in the category (a topos) consisting of
all Aldor domains and operations (functions). A similar view has also
been advocated by Haskell programmers.

http://www.haskell.org/haskellwiki/Category_theory

I believe that by taking such a view it is possible to explain how
domains are used now in Axiom/Aldor and also to suggest improvements
to the language that will make it more flexible and expressive.

Regards,
Bill Page.

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org