[Axiom-developer] kTuple wish

[Ralf Hemmecke]

The following text describes a weakness of the Aldor language.

Suppose I want to write a domain that takes a finite number of domains
satisfying a certain category "LabelType".

I write kTuple instead of Tuple, because the Aldor-Tuple constructor
is not suitable for what I want. In particular, if

  T: Tuple PrimitiveType

then I T = (Integer, String, Boolean, String) would be one possible
value for T. However, an element of T is not a Tuple, since T (not its
type) is non-homogeneous. So I would rather need something like
"Cross", but I cannot even ask about the number of arguments of Cross.


Let us give a rough outline of the domain Multiset which should be
seen as a constructor to construct k-tuples of sets over different domains.
Note that "SetSpecies" is just a special instance. I need something
for arbitrary S: LabelType -> LabelType.


Multiset(M: kTuple LabelType): with {
        <<exports: Multiset>>
} == add {
        macro S == SetSpecies;
        <<representation: Multiset>>
        <<implementation: Multiset>>
}
@




Section: <<representation: Multiset>>
--------------------------------------

The representation will be a kTuple.

By M.i I mean something like "element(M, i)" exported by the Tuple
constructor, but rather supported by the language (not the library).
If

  T: Tuple PrimitiveType == (Integer, String);

then element(T, 1) cannot be identified with Integer
at compile time, since the function "element" could be
non-terminating.

So the representation should informally be something like

  Rep == (S M.1, S M.2, ..., S M.k);

Since elipses are not a rigorous concept it should perhaps rather look
like

  Rep == MapOver(S)(M);


The "MapOver" constructor should be understood by applying the
constructor

  S = SetSpecies: LabelType -> LabelType

to each element of the tuple.

The above Rep could still be done via Aldor-Tuple, but I don't know
how to map a constructor S over a tuple whose size is not given at
compile time.



Section: <<exports: Multiset>> + <<implementation: Multiset>>
-------------------------------------------------------------

I somehow want that the Multiset constructor can be seen as a function
from kTuple to kTuple, i.e. the input and output tuple should have the
same arity.

 #: I == # $ M; -- arity doesn't change

It would simply be overcool if I'd have a function definition that
informally looks like

  multiset: (S M.1, ..., S M.k) -> %;

or rather

  multiset: MapOver(S)(M) -> %;

so that I could write

  multiset(sm1: S M.1, ..., smk: S M.k): % == per (sm1, ..., smk);

or rather

  multiset(sm: MapOver(S)(M)): % == per sm;

and later use it as

  T == Multiset(Integer, String);
  a: SetSpecies Integer := set [1,3,5];
  b: SetSpecies String := set ["a", "x", "free", "open"];
  t: T := multiset(a, b);

  U == Multiset(String, Boolean, Integer);
  c: SetSpecies Boolean := set [true];
  w: W := multiset(b, c, a);

The compiler should reject a statement like

  u: T := multiset(a, a);

at compile time.

If the constructor "MapOver" where built into the Aldor language that
should be doable at compile time. If I construct it as an ordinary
domain constructor (I still don't know how to do this with all the
"nice" properties I describe above), then the compiler has no good
chance to check at compile time since I might have made my constructor
non-terminating.

Is such a "MapOver" a bad idea? Or are there perhaps similar concepts
in other programming languages that would allow to reject a statement
like

  u: T := multiset(a, a);

at compile time.

Hmmm, maybe it is a bit tricky. Take, for example, the program aaa.as.

---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):

aldor -fx -laldor aaa.as
"aaa.as", line 10:         equal?: Boolean := a = b;
                   ...........................^
[L10 C28] #1 (Error) Argument 1 of `=' did not match any possible 
parameter type.
    The rejected type is S(AldorInteger).
    Expected one of:
      -- Boolean
      -- S(String)

The reason is clear, even though A = S Integer = S String = B = I, the
compiler will not evaluate S and thus consider A as unequal to B.

Being in that light, the compiler could reject

  u: T := multiset(a, a);

but if S maps everything to the same domain, should it reject it?
I'd rather live with "rejection", but since I am not a compiler
developer, I would like to hear people with more inside.

Thank you in advance

Ralf