[Aldor-l] Using Aldor or SPAD

[Gabriel Dos Reis]

Ralf Hemmecke <ralf at hemmecke.de> writes:

| > The only thing I know of the Aldor compiler
| > is that long time ago my "intern-mate" Yannis was working on it at
| > Sophia Antipolis...
| 
| Ah, Yannis Chicha worked with you... This world is so small...

Yup; Yannis hosted me for weeks before I got a place; it must have been
sometime in 1996. Stephen was the project leader at the time.

[...]

| Currently, in aldor-combinat I am going to define something like...
| 
| define CombinatorialSpecies(L: LabelType): Category == with {
|          <<exports: CombinatorialSpecies>>
| }
| CharacteristicSpecies(n:Integer)(L:LabelType): CombinatorialSpecies L == 
| add {
|          Rep == Set L;
|          import from Rep;
|          <<implementation: CharacteristicSpecies>>
| }
| EmptySetSpecies(L: LabelType): CombinatorialSpecies L == {
|          CharacteristicSpecies(0$Integer)(L) add;
| }
| 
| As you see, EmptySetSpecies is a function and its result type depends on 
| its input type L.


Yes. My question is whether "L" can be any value computed at runtime,
or only values known at compile-time.  E.g., do you want to say

   * read in a Label l
   * call CharacteristicSpecies with l

?

If yes, evaluation at compile-time will be very limited.

Or, would you be happy with Label values that are "known" to the
compiler, from "simple" program text analysis?

| But I think what you mention about categories is not really connected to 
| dependent or not dependent types. I actually don't know how one can 
| construct a category at runtime and later use it.
| 
| For example,
| 
| define Cat: Category == if odd? random() then {with {foo: () -> ()}}
|                                           else {with {bar: () -> ()}}
| 
| I could define a domain
| 
| Dom: Cat == add {
|     foo(): () == {}
|     bar(): () == {}
| }
| 
| But how would I use it? At compile time the compiler cannot decide whether
| 
| foo()$Dom;
| 
| is actually available.

Yes, that pushes checking to runtime and inhibit some static
optimizations.  So, I guess, we sort of agree on where to draw the
boundary. 

| > [ For example, C++ has dependent types at its "template systems" but
| >   values are limited to integers and addresses of toplevel entities ]
| 
| Could you provide some example code? A link?

A simple example involving non-type parameter is the classical

   template<tyename T, int N>
     struct buffer {
       T data[N];
     };

here the template buffer is parameterized by a type name and an
integer.  Internally it holds an array of N Ts.  It can be used as

     buffer<int, 512> cache;

or

     buffer<char, 4 * 512> buf;

Notice that the integer argument is anything that can be evaluated at
compile-time such as 512 or 4 * 512.  

| > | In fact, there are two things missing in Axiom:
| > | 
| > | 1) a replacement for SPAD that allows one to use the Aldor language
| 
| > Can anyone familiar with integrating SPAD with foreign languages
| > educate me about the thorny issues?
| 
| What exactly do you mean here?

Well, suppose I'm going to provide a language (that can be an existing
language such as C or Lisp or Aldor) that people use to write
libraries intended to be used with or from Axiom; are are the whoops I
or people would have to jump through?

-- Gaby