[Axiom-developer] Re: [Aldor-l] [Axiom-math] Are Fraction and Complex domains.

[Christian Aistleitner]

Hello Gaby,

On Sun, 14 May 2006 20:56:09 +0200, Gabriel Dos Reis  
<address@hidden> wrote:

> If you're after a non-functional type system,

I think, we all agree that for any programming language, it is good to  
have _non_ functional functions.
Just think about a system call time() behaving functional.

Besides, I am looking for a language, where same formalisms are treated in  
the same way.
For example all functions should be treated equal.
If one function is allowed to behave non-functional, all functions should  
be allowed to do so.

I'd like to model parametric categories and parametric domains by  
functions, as I described before -- it just seems natural.
Since there are non-functional functions, I'd allow all functions to be  
non-functional.

So finally, I am maybe after a non-functional type system.

> please explain
> clearly what they are useful for, with clear examples.

My previous examples in this directlions were probably not explicit enough:

System(): with {
  timestamp: Integer;
  cpuTemperature: Integer;
} == add {
  timestamp: Integer == { obtain the timestamp somehow }
  cpuTemperature: Integer == { obtain the timestamp somehow }
}

Of course, you can rewrite it to

System: with {
  grabData: () -> %
  timestamp: % -> Integer;
  cpuTemperature: % -> Integer;
} == add {
  macro Rep == Record( ts: Integer, temp: Integer );

  grabData(): % == {
     per record( obtain the timestamp somehow, obtain the temperature  
somehow );
  }

  timestamp( a: % ): Integer == { (rep a) . ts; };
  cpuTemperature( a: % ): Integer == { (rep a) . temp; };
}

, but would that be better? The latter version is the one we are more used  
to, but is it really better?
To determine the given temperature and timestamp for the system involves 1  
Function call for non functional Domains and 3 for functional Domains.

Of course, you can do a lot of rewriting tricks to say "non functionality"  
is not needed.
Of course, you can introduce a lot of "this is bad design" axioms to say  
"non functionality" is not needed.

But I think, non functionality would not be the baddest thing in the world.
As I said before, to me it looks like the compiler behaves non-functional,  
but uses fancy techniques to get functionality, wherever "this might me  
nice". I am sorry that I cannot give a more precise definition, since I do  
not have access to the compiler sources.

But consider, we had a completely non functional Aldor compiler (which we  
do not have). Would this compiler really lead to problems. I suppose not.  
Because in most cases, we have the types of interest in a constant form  
(e.g.: as parameter to a domain) and do not have to instantiate at all.

For example re-consider the SparseUnivariatePolynomial Integer example  
from Ralf
http://www.aldor.org/pipermail/aldor-l/2006-May/000198.html

Ralf> Surely, it would sound strange if I say:
Ralf>
Ralf> a: SparseUnivariatePolynomial Integer := ...
Ralf> b: SparseUnivariatePolynomial Integer := ...
Ralf>
Ralf> and the compiler would reject
Ralf>
Ralf> a + b
Ralf>
Ralf> because it could not figure out that a and b are of the same type

What Ralf wanted to have is that the two invokations of  
SparseUnivariatePolynomial refer to the same value.
For several reasons, it is important to tell the compiler everything you  
know about your code. But Ralf did not. If he would, the code would look  
like:

Poly == SparseUnivariatePolynomial Integer
a: Poly := ...
b: Poly := ...
and of course, the compiler would correctly recognize the + in
a+b

Furthermore, I the two approaches (functionality and non-functionality)  
are not completely different.
A functional type system can be used to "simulate" a non-functional one by  
adding the current time as parameter.
E.g.:
List( T: Type, timestamp: Integer == getCurrentTimestamp() ): with {
  ...
} == add {
}

So, calling List( Integer ) twice gives two different Instances, as the  
timestamp changed.

A non-functional type system can be used as a functional one by using  
constants.

ListInteger == List( Integer );
local a: ListInteger := empty$ListInteger;
local b: ListInteger := (insert!$ListInteger)( ... );

So you can get more or less the same behaviour ... If you want to.

> Explain also
> how one reasons with such type system, how one writes relaible program
> with such a type system.

Could you give an example in the functional world of what you mean by  
"reason"?

--
Kind regards,
Christian