[Axiom-developer] Re: rep, per, Rep in SPAD/Aldor

[Ralf Hemmecke]

On 07/13/2007 12:15 PM, Gabriel Dos Reis wrote:
> On Fri, 13 Jul 2007, Ralf Hemmecke wrote:
>
> | rep, per, Rep are *not* part of the Aldor language. (Gaby, I know that you
> | know.)  Although, all this macro business is a bit hard to understand, I would
> | not really agree to add rep, per, and Rep to the language specification. The
> | "pretend" is enough. I would only say that they should become part of the
> | language if "pretend" disappears. but then we trade one construct for three.
> | And maybe "pretend" cannot be made superfluous.
>
> I don't suggest that "pretend" be removed.  Just like general casts in C, or
> similar constructs in other languages, I don't think it should be
> removed and yet make Spad (or Aldor) expressive enough.  

OK.

> However, I do believe that `rep' and `per' are fundamentally part
> of the language semantics of domain.

Oh. You explicitly say "domain" (you don't include "package"). So I 
somehow have to agree. But not really. You know that by using "pretend", 
I could remove any uses of Rep, per, rep. Of course, nobody should write 
that code but rather follow the convention with Rep. What you want is to 
turn a convention into a rule. All I want to say is that this conflicts 
a bit with the design goals of Aldor: rather remove restrictions than 
introducing new features. I actually thought that you adhere to this 
principle. ;-)

> I don't think Rep should be there.
> Rep is quite of redundant with the pair rep/per.

I don't think, that I understand. There must be some way to actually 
write down the representation domain. If you have only rep and per, how 
would you do this?

> `rep' and `per' are there to fold/unfold views -- they are at the core
> of Spad or Aldor.

As I said, in some way you are right. It always confused me with this 
"Rep :=" or "Rep ==>" or "Rep ==" and no proper description of why Rep 
is so important (the concept, not the literal "Rep"). But now I know 
that if in my include file I define

macro {
        ying x == ((x)@%) pretend Ying;
        yang r == ((r)@Ying) pretend %;
}

I could completely do without Rep and rather say

---BEGIN aaa.as
#include "aldor"
#include "aldorio"

Foo: with {
  inj: Integer -> %;
  get: % -> Integer;
} == add {
  Ying == Integer;
  import from Ying;
  inj(z: Integer): % == yang z;
  get(x: %): Integer == ying x;
}
---END aaa.as

Gaby, I think that code is rather for others than for you. I am sure you 
understand that business quite well.

> | Why am I saying this? Maybe Martin now starts to listen more carefully... ;-)
> | 
> | In Aldor-Combinat, our species export two functions (simplified)
> | 
> |   structures: Set L -> Generator %;
> |   isoTypes:   Set L -> Generator %;
> | 
> | where L is the domain of labels of the structure.
> | 
> | I have not really a full picture yet (so don't take that overly serious), but
> | sometimes it comes to Martin's and my mind that isotypes should actually
> | return something else. For example, take Partition. structures, would return
> | set partitions while isoTypes (currently) return representatives of an
> | equivalence classes (a.k.a. isomorphism type). Clearly these equivalence
> | classes are in one-to-one correspondence with integer partitions. Integer
> | partitions could be handled much more efficiently. So it would be useful to
> | have 2 different representations for one domain.

> Yes.  How would that conflict with making rep and per part of the language?

No conflict. It just introduces new and unnecessary keywords. The 
conflict is with the principle I stated above.

> Many (most?) domains have only on representation, so it makes sense
> to `optimize' the notation for the common cases.

I completely agree. I just say it is not necessary to add new keywords. 
What do you think is the problem with rep and per as macros?

> For those that do
> need more refinement, users can provide their own views and the language
> will recognize that.  There is a precedence for that.  In C++ for example,
> user-defined types come equipped with a compiler generated copy constructor
> if user the user does not declare one.  For many value types, that is
> exactly what is needed and the semantics is optimal.

I somehow begin to understand your view.

> So, think about this:
>
>   (1) if a domain defines Rep, then automatically rep/per are
>      generated.

But that is also the way it is now in Aldor. If you don't define Rep and 
use rep/per, that gives a compile time error.

>   (2) if a domain defines one of per or rep, then the automatic
>       definition of the other is suppressed.

This is something I don't understand. Without defining Rep, I cannot 
define per. Why should I define rep/per anyway. They should just allow a 
different view on a object.

> | Let me for a moment even use an additional symbol %2. I'd like to say
> | 
> |   isoTypes: Set L -> Generator %2;
> | 
> | Of course that doesn't work in Aldor, but to my current knowledge it seems
> | that having several of these % symbols would better fit to the
> | multisort-algebra view on domains. It is not always the case that just one
> | carrier set is the most important and called %.

> I sort of agree.  When you have seveval representations (algebra in universal
> algebra sense) that abstract to the a given domain, then you actually
> have a category (in CT sense).  Would it not be convenient to express
> that in the code and actually use Spad categories?

OK, let me give my view on domains.

You have probably read
http://portal.axiom-developer.org/refs/articles/doye-aldor-phd.pdf
where Doye says that domains are somehow like order sorted algebras.

This is something like A = ((C1,...,Cn), (f1,...,fm)) with cardinal 
numbers n and m. (Of course, in Aldor we cannote express the infinite 
case since that would mean to write an infinite program.)

The order-sorted view is somehow correct, but if we look at an Aldor 
domain, there is always some distinguished thing (I don't know how to 
actually call this thing) which is denoted by %. It actually corresponds 
to the A from above. However, Aldor let's you think that it corresponds 
to C1 (the distinguished domain) which is usually denoted by Rep.

In Aldor we write

Foo: with {
  coerce: Integer -> %;
  test?: % -> Boolean;
} == add {
  Rep == String;
  ...
}

and mean something like

  Foo = ((%, Integer, Boolean), (coerce, test?))

in the multisorted algebra sense. We don't actually make Integer and 
Boolean (not String) an argument to Foo or "with", they are implicit.

Now, I have written % in the Foo = ... above and not

  Foo = ((Rep, Integer, Boolean), (coerce, test?))

since then the signatures of coerce and test? would not be OK.

That is the confusing point. Actually, there should be Rep and Foo 
should correspond to %. This is what we do in mathematics all the time. 
We speak of the (additive) monoid of integers and denote it by Z 
although that is at most the carrier set and some people would find that 
confusing if Z is used without reference to the additive structure.


I think there is a difference if we consider the "with" or the "add" 
part of a domain.

For the "with" part (and that is what a user of the domain actually 
sees), the above definition clearly corresponds to

  Foo = ((%, Integer, Boolean), (coerce, test?))

And for the user of this algebra, Foo and % are identified. That is what 
Aldor does here. (Although, it is mathematically not strictly correct.)
But most mathematicians do so in (almost) all cases.

Now let us look to the "add" part. There we have yet another domain, 
namely Rep. Inside "add" we actually consider an algebra like

  Foo' = ((%, Rep, Integer, Boolean), (coerce, test?, per, rep))

Hmmm, I have just cooked that all up right now, but it seems a pretty
coherent view on domains.

Since "add {...}" is an anonymous domain, it should actually export what 
is in the signature part of Foo', so let's see.

aldor -gloop
%1 >> #include "aldor"
%2 >> #include "aldorinterp"
%3 >> add {Rep==String;coerce(z:Integer):%==per 
"int";test?(x:%):Boolean==true}
  () @  with
        Rep: ? == String
        coerce: (z: AldorInteger) -> %
        test?: (x: %) -> Boolean

That is pretty close, but lacks per and rep. Gaby, I think that is one 
point for you. Here I would like to see rep,per, Rep. Don't you agree?
But note if we export Rep, we somehow are in conflict with "hiding the 
representation".

Any other opinions.

Actually, I started that mail with something else in mind, but now I am 
not so sure anymore whether I would really like to have %, %2, %3, etc. 
anymore. This correspondence of Foo with % is in some way rather 
ingenious. I have to think more about my original reference to wanting 
two representations for species in Aldor-Combinat.

Sorry, Gaby, I have not really responded to that categorial view in your 
statement above. I think I don't understand it properly. Could you 
elaborate and add a bit of your wisdom.

Thank you
Ralf