[Aldor-l] exports and constants

[Gabriel Dos Reis]

"Bill Page" <bill.page1 at synthesis.anikast.ca> writes:

| On July 24, 2006 5:10 PM Gaby wrote:
| 
| > | > ...
| > | > Bill Page wrote:
| > | ... 
| > | Could you define for me what you mean by "dynamic type"?
| > | I think the usual definition involves type checking during
| > | run time.
| > 
| > Not really.  If you take the C language for example, there is the
| > notion of "static type" and "dynamic type" (sometimes called
| > "effective type"), yet C does not require type checking during
| > runtime.  
| > 
| > When you have the notion of variable declaration and the possibility
| > of "cast", i.e. in the sense of change of *type of expression* used
| > to access data, you naturally get into distinguishing "static type"
| > from "dynamic type".  You don't necessarily need to have runtime
| > type checking involved.
| 
| Oh, the water is so muddy! Let's reserve talking about Aldor's
| 'pretend' for another time, but recall that 'rep' and 'pre' are
| intended as a "type-safe" implementation of this idea.

But, casts in C are also intended to be "type-safe" too -- no kidding,
really. :-)

| > "static type" concerns with the properties of the program that
| > can be derived only from "static" analysis without taking into
| > account any runtime semantics.
| > 
| > "dynamic type" concernes the properties of the program that can
| > be derived by taking into account runtime semantics.
| 
| Yes, this definition seems fine to me.
| 
| Do you agree that Aldor uses only "static type"?

not from my understaing of "static type" and the way Aldor handles
"multiple inheritance" and "has".

| > | Since Aldor is statically typed how can we define this in a
| > | useful way in Aldor?
| > | 
| > | Should we say something like this?
| > | 
| > |  The "dynamic type" of Y is
| > | 
| > |    Join( x for x in Category where Y has x)
| > 
| > that is close -- and certainly matches practice in object oriented
| > languages and non-object orinted ones like C.
| > 
| > | But then dynamic type would be just type satisfaction as I
| > | said earlier, no?
| > 
| > no, "type satisfaction" is a generic term that applies to both
| > the static semantics and the dynamic semantics.
| 
| I meant "type satisfaction" as it is used in the Aldor Users Guide
| in the definition of the "has expression".

It says in section "7.7 Type Satisfaction":

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

That does not tell me that "type satisfaction" is only in the sense of
"dynamic type" -- nor does the rules that are listed there...

| > ... 
| > I suspect the trouble here is that in some context "has" is
| > evaluated statically, and in other context it is evalued
| > dynamically.  So you fail to appreciate the distinction.
| 
| The Aldor Users Guide says that "has" expressions are evaluated
| at run time.

Yet, you have to confront that with earlier claims that Aldor uses
only "static type" when one is confronted with codes like

   with {
           BoundedFiniteLinearStructureType S;
           if (T has TotallyOrderedType) then {
                   TotallyOrderedType
                   sort!: % -> %
           }
   }

-- Gaby