[Axiom-developer] Re: [Aldor-l] kTuple wish

[Christian Aistleitner]

Hello,

On Thu, 29 Mar 2007 02:03:25 +0200, Ralf Hemmecke <address@hidden> wrote:

> So I would rather need something like
> "Cross", but I cannot even ask about the number of arguments of Cross.

one can easily teach Aldor about the size of a Cross with the help of  
extend. Then you can ask a Cross about the number of elements.
I already discussed the details with Ralf via private mail, so I am just  
stating it here for the record. If anybody else is interested in this, I  
will share some code.


> ---BEGIN aaa.as
> #include "aldor"
> I ==> MachineInteger;
> S(T: PrimitiveType): PrimitiveType == I;
> main(): () == {
>         A ==> S Integer;
>         B ==> S String;
>         a: A := (0$I) pretend A; -- I need some value ...
>         b: B := (1$I) pretend B; -- forgive the "pretend" ...
>         equal?: Boolean := a = b;
> }
> main();
> ---END aaa.as
>
> It currently dose not compile (Aldor 1.0.3):

I am not too sure whether it should compile.

First of all, I think notation is misleading here. The "==" in

> S(T: PrimitiveType): PrimitiveType == I;

does not necessary mean that the function S maps to the same I every time.  
This is somehow the synopsis, now for the details.
From my point of view, the above definition of S is a shorthand notation  
for

  S: PrimitiveType -> PrimitiveType == ( T: PrimitiveType ): PrimitiveType  
+-> I;

. (I quickly wanted to check the AUG on this concern, only to find out  
that I cannot find my rewrite suggestion, but only Ralf's way (page 61) of  
writing it. Nevertheless, I thoroughly believe, that my kind of writing it  
is the way the compiler looks at it, and Ralf's way is just a short-hand  
notation.)
Using this rewritten definition, it is more obvious, what the "==" refers  
to. It definitely denotes that the function is constant, not the result.  
But you did not claim otherwise.

Within the AUG, you'll find that typically only the left-hand side of the  
== is seen at certain stages of compilation. So lets omit the righthand  
part of S's definition:

  S: PrimitiveType -> PrimitiveType ==

Now it is indeed hard to see that

>         A ==> S Integer;
>         B ==> S String;
>         a: A := (0$I) pretend A; -- I need some value ...
>         b: B := (1$I) pretend B; -- forgive the "pretend" ...
>         equal?: Boolean := a = b;

should compile, there is no obvious reason (S Integer) and (S String)  
should evaluate to the same PrimitiveType.

Having seen this from this more abstract point of view, let's investigate  
the right-hand side of S's definition

  ( T: PrimitiveType ): PrimitiveType +-> I;

. Why should this functional evaluate to the same PrimitiveType again and  
again (And this condition would have to be satisfied before allowing the  
compiler to somehow compile above code)?
From a previous discussion, we learned that in Aldor functions typically  
are not functional. The exception are expressions in type context. "S  
Integer" and "S String" are in type context in the above piece of code.  
Nevertheless, type context does not resolve the problem, because it  
basically tells us that the types of
  c: S Integer
and
  d: S Integer
match, not that the type of a and b match. Type context allows to compile  
the line

>         a: A := (0$I) pretend A;

as otherwise, S would be evaluated twice at Integer.
As the exception of non-functionality does not help or apply to the  
problem. S has to be evaluated twice--once for Integer and once for  
String. For each of the evaluations (which happen at run-time from my  
point of view), the function S happens to return the same value. This  
observation can only be made at run time and not at compile time, as the  
"I" may be arbitrary code.

Your code is the rather (seldom case) where the value (I) is hidden just  
to get more structure (S). One could argue that Aldor should treat this  
case properly.
However, only slight variations of your code (e.g.:

  S(T: PrimitiveType): PrimitiveType == Fraction I;

) have a different semantics. For such an S (with the above macros),

>         a: A := (0$I) pretend A;

should work (type context of S String), but

>         a: A := (0$I) pretend A;
>         b: B := (1$I) pretend B;
>         equal?: Boolean := a = b;

_has_ to fail. As Fraction Integer is not in type context, it _should_  
give _different_ instances of fractions over the domain MachineInteger.
This was just to show that your code is really rather the special case.  
Nevertheless, I see that you want and need the compiler to compile

>         equal?: Boolean := a = b;

in your setting. The first line of your message was

> The following text describes a weakness of the Aldor language.

so we both agree that this it not a bug in the compiler (sigh), but rather  
you need something Aldor has not been designed to do.



Kind regards,
Christian