[Aldor-l] exports and constants

[Bill Page]

On July 25, 2006 2:00 AM Christian Aistleitner wrote:
> ...
> Assume, Aldor has no knowledge about a values type other than 
> the static type (I guess that's what you want have.) -- purely
> "Types on variables".
>

Please keep in mind here that I, like you, are primarily just
trying to understand Aldor, how it works and how best to use
it for programming. So if it sounds like I am being "dogmatic"
below, take that with a "grain of salt". I mean: I am quite
willing to change my point of view if forced by argument. :)
 
> Then in a statement like
> 
> func( R: Ring ): () ==
> {
> 	
> }
> 
> Aldor knows that R is of static type Ring within the 
> function's body.  
> Nothing more. Nothing less.
> Especially, the test "R has Field" in
> 
> func( R: Ring ): () ==
> {
> 	if ( R has Field ) then
>        {
>           ...
>        }	
> }
> 
> could never be true, since (as stated before) Aldor only 
> knows that R is of static type Ring. Nothing more. Nothing
> less.

Actually, I think what I want is to have that the expression
"R has Field" does not necessarily involve the concept of "type"
as such. In Axiom (from which Aldor was derived), it is common
to consider this use of Field as testing an attribute. In the
design of Axiom, attributes are asserted and tested by the
programmer.

For example you might see:

  if R has commutative("*") then
    determinant: $ -> R

but 'commutative' is not defined as a category anywhere.

See section 12.9 of the Axiom book. I hope you don't mind if
I quote it almost in it's entirety:

---------------
12.9 Attributes

Most axioms are not computationally useful. Those that are can
be explicitly expressed by what Axiom calls an attribute. The
attribute commutative("*"), for example, is used to assert that
a domain has commutative multiplication. Its definition is given
by its documentation:

  A domain R has commutative("*") if it has an operation
  "*": (R,R) For all R such that x * y = y * x.

Just as you can test whether a domain has the category Ring, you
can test that a domain has a given attribute. Do polynomials over
the integers have commutative multiplication?

  Polynomial Integer has commutative("*")

Do matrices over the integers have commutative multiplication?

  Matrix Integer has commutative("*")

Attributes are used to conditionally export and define operations
for a domain (see 13.3 on page 909). Attributes can also be asserted
in a category definition. After mentioning category Ring many times
in this book, it is high time that we show you its definition:

  Ring(): Category ==
  Join(Rng,Monoid,LeftModule($: Rng)) with
    characteristic: -> NonNegativeInteger
    coerce: Integer -> $
    unitsKnown
  add
    n:Integer
    coerce(n) == n * 1$$

There are only two new things here. First, look at the $$ on the
last line. This is not a typographic error! The first $ says that
the 1 is to come from some domain. The second $ says that the
domain is "this domain." If $ is Fraction(Integer), this line
reads

  coerce(n) == n * 1$Fraction(Integer).

The second new thing is the presence of attribute "unitsKnown".
Axiom can always distinguish an attribute from an operation. An
operation has a name and a type. **An attribute has no type.**
The attribute unitsKnown asserts a rather subtle mathematical
fact that is normally taken for granted when working with rings.
Because programs can test for this attribute, Axiom can correctly
handle rather more complicated mathematical structures (ones that
are similar to rings but do not have this attribute).

-------------

Apparently in the design of Aldor it was realized that because
of the possibility of multiple inheritance, the concept of an
"attribute" could be modelled in Aldor as a category with an
empty signature. But multiple inheritance also means that the
concept of "type" is more complicated than in some other
programming languages.

> 
> However, that's not the way things work. And that's actually 
> a good thing. (We drop the assumption).

I agree with that.

> 
> Aldor has to have more knowledge about R than only its static 
> type. Aldor knows about the dynamic type. And the "types on
> variables" paradigm does not deal with this. If I am not wrong,
> "Types on variables" refers solely to the static type.

I think that because of multiple inheritance, you are in fact
wrong. And I am reluctant to introduce a new concept "dynamic type"
that is not defined in the current Aldor or Axiom documentation.

> 
> So for domains, we have more than the static type -- more 
> than the type on a variable. We have dynamic types --
> "Types on data" (Be it that the type is really stored in memory
> locations close to the data, be it that there is some lookup
> table for dynamic types, or be it something completely  
> different. Aldor gets to know the dynamic type of a domain 
> and thereby associates a type to data, not to the variable).
> 

I agree that there is more than "static type" but I do not
agree that this is "types on data". "types on data" (i.e.
dynamic type checking at run time) contradicts one of the
design goals of Aldor. I do not see anywhere in Aldor where
the notion that all data (values) have type. But as I said in
an earlier email, Aldor does of course have "type inference"
which means that in a given context, Aldor must be able to
determine the types of various expressions.

Regards,
Bill Page.