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

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

| Can you teach me what a "mode" is? Is that some common term used in
| some context?

A mode seems to be an Axiom-atic term.  The only places I've seen it
used with that specific meaning is in Axiom literature -- see the
B-natural paper, the Axiom book, scratchpad papers. 

Algol uses the term "mode" for what we call "type."  At least my manual
of Algorl 68-R says (page 1):
    
   Values are classified according to type, known in Algol 68 as their
   /mode/. 

| > |        or   " Complex " construct a domain, but isn't a domain ?
| > I think so.
| 
| Hmmm, according to Section 7.8 in the pdf-version of the
| AldorUserGuide, one must perhaps also call "Complex" a domain. But
| then I would prefer to call it "parametrized domain".

The Axiom book calls it a "domain constructor", just like Polynomial,
etc.  See section 2.1.1, page 61.  For example:

   To create the domain of "polynomials over the integers", AXIOM
   applies the function Polynomial to the domain Integer.  A function
   like Polynomial is called a /domain constructor/ or, more simply, a
   /constructor/. 

That terminology is consistent with anything else I've seen in the
majority of programming language communitites.

| > |        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!  

Do you really want a type system whose language is not functional?
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? 


| (I have no idea whether the
| following could be done in SPAD, though.)
| 
| 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.

| 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.

-- Gaby