[Aldor-l] exports and constants

[Gabriel Dos Reis]

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

| On July 24, 2006 1:09 PM Gaby wrote:
| > ...
| > Bill Page wrote:
| > | 
| > | Ok. Do you still think that it is appropriate to try to use
| > | the term "dynamic type" in the discussion of Aldor semantics?
| > 
| > Even in the context of dependent types, the phrase "dynamic type"
| > makes sense, just as static type does.
| > 
| 
| 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.

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

| 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.  If you have

   mumble : (Monoid) -> Monoid

and call it with Integer, you have a type satisfaction (implemented by
coercien) yet, the decision is made statically.

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.

-- Gaby