[Aldor-l] Name constancy in type context and lazy evaluation

[Christian Aistleitner]

Hello Martin,

I think, we are loosing focus because of terminology problems. So I  
decided, to write these things up for a start, and rephrase the problems  
and claims of the previous mails.

_arbitrary_, _recursive_, parametric types:
----------------------------------------------

By arbitrary, recursive, parametric types I mean types of the form

   ( r1, r2, ... rn ) == f( p1, p2, ..., pm, r1, r2, ..., rn );

. This is plainly what you want from Aldor, when being able do define  
Types for your grammars:

( A, B ) == typeBuildingFunction( [
   "Union(Atom, Cross(Self1, Self2))",
   "Union(Atom, Cross(Self2, Self1))"
  ] );

Because, your function should yield A, B such that

   ( A, B ) == ( Union(Atom, Cross( A, B )), Union(Atom, Cross( B, A )) );

. This is connected to the above formulation via
n=2,
m=1,
A <-> r1,
B <-> r2,
Atom <-> p1,
f: ( X, Y, Z ) |-> ( Union( X, Cross( Y, Z ) ), Union( X, Cross( Z, Y ) ) )

We know that your code works with the current Aldor compiler. Whether or  
not your code covers the whole "arbitrary, recursive, parametric types"  
problem is not yet important.



iteration scheme:
-------------------

The term “iteration scheme” was probably not the best translation from the  
German term for it. However, Wikipedia shows, what I meant
http://en.wikipedia.org/wiki/Iteration_scheme
which is also called “iterative method”.

So basically things like for example Newton's method. You apply a method  
again and again until you get a solution (or a value being sufficiently  
close to the exact solution).




So after these clarifications, let me recall the original discussion and  
add further remarks:

>>>> However, I'd say that the more important questionis, whether it  
>>>> [ Annotation by Christian: changingsomething constant for patching up  
>>>> parameters todomain building functions before the domain building
>>>> functions get evaluated ] *should* be allowed ornot. It doesn't  
>>>> really make sense to have such abeautiful language imposing  
>>>> conditions that actually
>>>> restrict it's applicability.

Then I said

>>> Are there languages, where you can create _arbitrary_,
>>> _recursive_, parametric types (...) smoothly at runtime?

because I do not know of any language where you can do the things you want  
clearly, nicely and smoothly.
You can do what you want in Aldor, but it's far from smooth and nice, as  
hopefully we all agree on.

>> As far as I know, ANSI Common Lisp allows that...

However, I doubted that and wanted to see an example. You could not give  
one, because of terminology problems in the discussion. Hopefully you can  
give an example now.

As there is not yet an example, this leaves us with your claim of

>>>> It doesn't really make sense to have such abeautiful language  
>>>> imposing conditions that actually
>>>> restrict it's applicability.

. However, _every_ language has this restriction (until an example shows  
the contrary).

I tried to show you, where the problems are when allowing, what you want  
to have. Let me recall my remarks (with additional explanations):

What you want relates to the fixed point problem in mathematics:

     x = f( x )

. The correspondance is given above when explaining arbitrary, recursive,  
parametric types.

What are the constraints for the compiler when computing x?

The compiler needs to find the exact solution:
Fix point problems are often solved numerically, by approximating the  
exact solution using iterative methods. In our settings, approximations of  
x are worthless. We cannot compute with domains meeting their  
specification only approximately.
As iterative methods typically give the exact solutions for specially  
taylored examples or after infinitely many iterations, we cannot use them.
Hence, the compiler cannot use iterative methods to solve the fix point  
equation.

The compiler has no information about f:
It would not make much sense to allow the above x = f(x) only if f is some  
special function (say List) and give it special treatment. The reason is  
simple: The compiler must not make assumptions on the nature of the  
implementation of f (or List). f (or List) is just a name. Everything can  
be hidden inside.
f can be essentially an _arbitrary_ domain building function.

The compiler must not evaluate f more than once:
f may cause side effects. If you use code like, x = f( x ), you'll expect  
f to be evaluated once (at most). Assume the compiler would evaluate f  
twice. The first evaluation to gain knowledge about f, and the second  
evaluation to solve x = f( x ). Then the side effecting part of f would be  
executed twice. How should you know in advance, how often the compiler  
evaluates f? Therefore, the restriction to evaluate f only once is natural.

The compiler must not evaluate f at a value different to the solution x of  
x = f( x ):
This more or less is required for consistency reasons and is partly  
implied be the previous argument.

Has to work for all f:
The compiler has to generate working code for all possible fs. f may be  
generated at runtime. Therefore, it's hazardous if the code works for some  
f and does not for others. The programmer would have to decide at runtime,  
whether the compiler generated code works with the function generated at  
runtime. This looks like a nightmare to me.

x = f( x ) has to hold:
Effectively you want the compiler to solve the above problem without any  
knowledge about, f or x. f may be evaluated only once. This evaluation has  
to be already at x.
Rather impossible I guess.


In the whole discussion, we assumed that there is a fixed point. What if  
there is no finite fixed point?
E.g.:
    X == List( X );

You said

> recurse to infinity, as soon as I try to use X.

But that's not an option.

What if there are more than one fixed point? Would you take any and  
introduce compiler generated vagueness?


--
Kind regards,
Christian