[Axiom-developer] Re: Cast = pretend in Spad/Aldor? (was: B#)

[Gabriel Dos Reis]

"Bill Page" <address@hidden> writes:

| On November 21, 2005 12:59 PM Gaby wrote:
| 
| > 
| > "Bill Page" writes:
| > 
| > | On November 20, 2005 11:50 PM Gaby wrote:
| > | > | 
| > | > | We have mentioned before on this list the very good article
| > | > | 
| > | > | http://en.wikipedia.org/wiki/Datatype
| > | > | 
| > | > 
| > | > That is interesting but the link above is confused to start
| > | > with. I quote: 
| > | > 
| > | >    An example of the absence of strong typing is a C cast 
| > | >    gone wrong; if you cast a value in C, not only is the
| > | >    compiler required to allow the code, but the runtime is
| > | >    expected to allow it as well.
| > | > 
| > ...
| 
| Actually, perhaps I should simply concede that the above
| article is not particularly good, and I will be glad to do
| so if you can recommend a better alternative that defines
| these terms more accurately.

I don't know of a good definition of "strong typing" that does not
promote particular languages one is interested in, and at the same
time downplay languages one does not particular like/prefer/use.

The term is ambiguous, and usually used to convey personal preferences
undr the cover of seemingly "universal terms."

| But really I don't want to be spending a lot of time arguing
| about the merits of the C programming language on this list.
| What I would really like to think about is strong static typing
| in the context of Axiom, specifically in Spad and in Aldor.

Great!  We're on the same page then.

| There is one very important type-related construction in
| Spad and in Aldor that looks as if it might make them "weak"
| in the sense in which the author of the above quote implies
| the use of cast in the C language makes it weak. That is the
| use of 'pretend'.

I claim that any serious programming language for large scale
software, that supports system programming to some extent, and that
allows "multiple representation" would contain something similar to
casts, and that operation would probably be spelled differently.

| It is pretty clear in the following example that the Axiom
| interpreter does something odd:
| 
| (1) -> I:Integer
|                                                 Type: Void
| (2) -> F:Float:=1.0
| 
|    (2)  1.0
|                                                 Type: Float
| (3) -> I := F pretend Integer
| 
|    (3)  1()
|                                                 Type: Integer

I'm not (yet) fluent in Aldor as I would like, and I wish I had more
time to devote to the language specification and implementation.  I
however hope the Aldor compiler source will be "open sourced" soon as
I understood it.

| Yet the ability to use 'pretend' is critical to the concept
| of representation in the construction of Axiom domains.

Indeed.

| For a perhaps overly abstract discussion of this see:
| 
| http://wiki.axiom-developer.org/RepAndPer
| 
| So my question is: Does this feature of the Spad and Aldor
| languages actually make them "weakly typed"?

In my mind "pretend" by itself does not make the language "weak
typed".  It would make it so only if it "actively support" type
unsafe operations to be carried on with minimal effort -- in that
sense I would claim C is weakly typed.  Notice here that my used of 
"type safety" is not in a a universal sense, but relatively to Aldor's
own semantics.
For more elaboration of what I meant, and in better and clearer terms,
have a look at the following (of Bob Harper):

  http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00298.html

-- Gaby