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

[Page, Bill]

I think Francois Maltey's question is an excellent one!

On Thursday, May 11, 2006 12:47 PM Gabriel Dos Reis answered:
> ... 
> "Complex" is the name of a (type) function.
>  "Complex ?" is a mode.
> ...

> Ralf Hemmecke asked:
> 
> | Can you teach me what a "mode" is? Is that some common
> | term used in some context?
>
 
On Thursday, May 11, 2006 2:49 PM Gabriel Dos Reis wrote:

> 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 Algol 68-R says (page 1):
>
>    Values are classified according to type, known in
>    Algol 68 as their /mode/. 

I like Gaby's first answer better than the 2nd. Specifically,
in the Axiom interpreter "Complex ?" (literally including
the ? ) is a called a "mode". This has nothing much to do
with the use of the term "mode" in Algol.

In Axiom a mode is a kind of "type pattern" or partially
specified type. The interpreter uses this pattern in the
way that it does type inherence. See especially Chapter 2
of the Axiom Book:

"2.2.4 Modes

A mode is a type that possibly is a question mark (?) or
contains one in an argument position. For example, the
following are all modes.

?
Polynomial ?
Matrix Polynomial ?
SquareMatrix(3,?)
Integer
OneDimensionalArray(Float)

As is evident from these examples, a mode is a type with
a part that is not specified (indicated by a question
mark). Only one "?" is allowed per mode and it must appear
in the most deeply nested argument that is a type. Thus
?(Integer), Matrix(? (Polynomial)), SquareMatrix(?, Integer)
(it requires a numeric argument) and SquareMatrix(?, ?)
are all invalid. The question mark must take the place
of a domain, not data. This rules out, for example, the
two SquareMatrix expressions."

The type system of the Axiom interpreter is actually subtly
more general than the type system in SPAD and Aldor. In the
interpreter symbols are actually assigned modes (which may
also be completely specified be types).

For example the symbol 'm' is assigned the type 'Complex
Integer'

(1) -> m:Complex Integer
      Type: Void

and so the following is an invalid assignment:

(2) -> m:=2.3

   Cannot convert right-hand side of assignment
   2.3
      to an object of the type Complex Integer of the left-hand side.

But the symbol 'm' is the mode "Complex ?"

(2) -> n:Complex ?
       Type: Void

Now the assignment of a Float value makes sense because
the interpreter can inference the actual type:

(3) -> n:=2.3

   (3)  2.3
   Type: Complex Float

The same mode "Complex ?" can also match other types:

(4) -> n:=2

   (4)  2
   Type: Complex Integer

(5) ->

> 
> | > |  " 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 "parameterized domain".
> 
> The Axiom book calls it a "domain constructor", just like Polynomial,
> etc.  See section 2.1.1, page 61.

The Aldor users' guide also uses the term "type constructor"
e.g. in reference to 'List'. Since in Aldor domains are types
the Axiom terminology makes sense. See section 5.6, page 42
and section 7.2, page 75, and even in one place, page 230,
the term "domain constructor".

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

I what sense is Aldor's type system "not functional"?
Do you mean in the sense that evaluating a type
expression in Aldor might have some side-effect? E.g.

   a:Funny(Integer)

where 'Funny' is some type constructor. As far as I know,
in both Aldor and SPAD this is not possible. Types in
Aldor and SPAD are static - evaluated a compile time -
not during run time.
 
> 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 whose
> constructors do not evaluate the same arguments to the
> same value? 
>

I think Ralf is wrong. Both SPAD and Aldor's type systems
are functional (and static!) in this sense.
 
Regards,
Bill Page.