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

[Ralf Hemmecke]

Hello Gaby,

I have included aldor-l in this thread, because I think you raised an 
important question with the "functional type (sub-)language". 
Additionally, I've moved it from axiom-math to axiom-developer.

On 05/11/2006 08:49 PM, Gabriel Dos Reis wrote:
> Ralf Hemmecke <address@hidden> writes:

[snip]

> | > |        or   " Integer " is an abbreviation for Integer without parameter ?
> | 
> | > from the functional perspective, Integer is a nullary (type) function;
> | > it is actually a type constant.
> | 
> |  From a functional point of view you are certainly right, the only
> | problem is that Aldor is not functional.
>
> That should not matter; and if it does, it is a bug!  

Well, to me it is not a bug. But I am not the language designer. I am 
sure Stephen Watt could make things clear here.

> Do you really want a type system whose language is not functional?

Actually, I haven't thought about this. I somehow have the feeling that 
the Aldor compiler implements such a functional type language. But I 
don't know whether this is on purpose.

> Notice, that I'm not saying the term language should be functional.
> I'm talking of the type (sub-)language.  How do you work with a type
> system system whose constructors do not evaluate the same arguments to
> the same value?

Surely, it would sound strange if I say:

a: SparseUnivariatePolynomial Integer := ...
b: SparseUnivariatePolynomial Integer := ...

and the compiler would reject

a + b

because it could not figure out that a and b are of the same type 
(because of non-functionality). So in this sense I certainly find a 
functional type language more natural.

> | BTW, I would rather say, Integer is a type constant. If Integer() is
> | defined and works in Axiom then please show me a definition of the
> | language that makes it clear that if one defines
>
> Please, first, show me how you meaningfully work with a type system
> where the type language is not functional.

That is not a field where I'm an expert in.

> | Integer: SomeIntegerCategory
> | 
> | that also
> | 
> | Integer: () -> SomeIntegerCategory
> | 
> | To me, these two things clearly have a different type.

> The syntaxes are different; the question is whether the *semantics*
> should be different.  The answer must be "no", for a workable type
> system.

I don't agree. The program

----------------------------------------------------------
aldor -grun -laldor aaa.as
Dom:   1
Dom(): 0

--begin aaa.as --------------------------------------------
#include "aldor"
#include "aldorio"

Cat: Category == Join(ArithmeticType, OutputType) with;
Dom: Cat == Integer add;
Dom(): Cat == Integer add {
    Rep == Integer;
    import from Rep;
    1: % == per 0;
}
main(): () == {
    import from Dom, Dom();
    stdout << "Dom:   " << 1$Dom << newline;
    stdout << "Dom(): " << 1$Dom() << newline;
}
main();
--end aaa.as

shows that Dom and Dom() need not be identical and one can still have a 
consistent type system.

I would even call it functional (if Dom() always produces the same 
value). It is only that things of type Cat and things of type ()->Cat 
are not identified even if they happen to have the same name.

But of course, I could live with that identification if it is clearly 
documented that ()->Cat can be identified with Cat. Where are our 
category experts? I believe there is a distinction here, n'est pas?

Ralf