[Aldor-l] exports and constants

[Bill Page]

On July 24, 2006 4:06 AM Christian Aistleitner wrote:
> 
> On Mon, 24 Jul 2006 04:33:34 +0200, Bill Page wrote:
> 
> > In Aldor when we write:
> >
> >   X: CatX
> >
> > it means explicitly that the type of X is CatX. And we are
> > saying that it is the compiler's job to check (at compile time)
> > that this is necessarily always the case.
> >
> > But 'X has CatA' is something different. I think Christian
> > referred to it earlier as something like the "dynamic type"?
> > But in the Aldor User's Guide this is just called
> > "type satisfaction".
> 
> But I suppose, the reason for the whole discussion is that 
> Aldor does simply refer to types. Aldor follows the "types on
> variables approach". And "values are not normally self-identifying"
> (which hopefully means something like "values are normally not
> self-identifying").

I don't think I understand your previous sentence. Do you mean
to emphasis the phrase "not normally", implying that the cases
when this does not implying are very important?

I think section "7.1 Why types?" in

http://www.aldor.org/docs/HTML/chap7.html

describes this very clearly.

Section 7.2 describes types as values. As values, the type of these
type-values would not be "self-identifying".
 
> So data has no type on its own--normally. Assume Domains are not
> self-identifying. The whole "has" thing would  collapse. Because
> "has" does test on the data, not the type of the variable referring
> to the data. So domains have to be self-identifying.

Section 7.9 says:

  Has expressions

  A ``has'' expression has the following form:

      dom has cat

  where dom is a domain-valued expression, and cat is a category-valued
  expression. A ``has'' expression may be used in any part of a program,
  but is most often used to conditionalize domains and categories. The
  result of the expression is a Boolean value which will be true if dom
  can be shown to **satisfy** the category, and false otherwise.
  ...
  The evaluation of this expression is made at run-time, ...

** my emphasis. Type satisfaction is defined in section 7.7: 

  "We say that a type S satisfies the type T if any value of type S can
  be used in any context which requires a value of type T."

Why do you claim that this means that domains must be "self-identifying"?

> Therefore, in a statement
> 
> A: B == C;
> 
> we have to separate between the type that A is defined to have (which
> is B -- due to the "A: B") and the type of the value of A (which is
> the type of  C -- due to A == C).
> During my education, I've been given the terms "static type 
> of X" to refer to the first concept and "dynamic type of X" to the
> later concept.
> 
> Yes, these two terms are important for type satisfaction. But 
> I do not think, "dynamic type" is just called "type satisfaction"
> in the Aldor user guide.

I agree.

The only time the Users Guide refers to dynamic type is in the
context of the discussion of "7.4 Dependent Types":

"Solution 3: Use an Object-Oriented approach.

One can associate the dynamic type of the value with the value itself.

If the different possible types are to be handled in essentially the
same way, then this solution can be a reasonable choice. The type
information associated with the value can carry the functions which
may be used to operate on it.

One difficulty with this solution is that it is not possible to
indicate when many values belong to the same dynamic type, leading
either to unsafe code, or to testing tags during program execution."

As I understand it, the point is that Aldor implements dependent
times instead of object-oriented dynamic types.

> Type satisfaction typically acts on the static type of both,  
> participing entities. (In the example above A's static type 
> (which is B) has to met by C's static type. Not "dynamic type
> at all.)
> 
> "static type" and "dynamic type" may coincide, but do not have
> to.
> 

Ok. Do you still think that it is appropriate to try to use the
term "dynamic type" in the discussion of Aldor semantics?

Regards,
Bill Page.