[Axiom-developer] RE: Cast = pretend in Spad/Aldor?

[Bill Page]

On November 21, 2005 3:14 PM Gaby wrote:
> ...
> Bill Page wrote: 
> | 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.

I think representation in domains (rep and per) is an essential
part of Axiom's "object model". Would you say that your claim
above also applies to any object-oriented language?

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

We are still waiting <expression of growing frustration> for
Steven Watt to officially announce something. I do not understand
the delay but I am still confident that this is going to happen.
And I am still plotting possible ways to force the issue. :)
Of course it would still help if other people on this list would
simply write to Steven and emphasize the importance of making
Aldor open source as soon as possible.

In the mean time we can certainly apply these same ideas to
Spad and to the Spad-like programming language embedded in
Axiom's interpreter.

> 
> | 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 universal sense, but relatively to
> Aldor's own semantics.

Ok, so my example above from the Axiom interpreter (this is not
what happens in Spad and Aldor) would be such an example of
failure of type safety, right?

> 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

Thank you for this reference. I think it is very useful. I find
the notion of "transitions" between programs to be rather awkward
to apply but perhaps I simply do not understand the approach very
well. Can you suggest a reference that describes the formal approach
used here by Robert Harper?

Generally I have come to prefer a more "category theory" oriented
approach to program semantics e.g. as presented in introductory
form by Benjamin Pierce in "Basic Category Theory of Computer
Scientists" and in his "Advanced Topics ..." collection (which
contains a joint paper by Harper and Pierce on ML modules).

It seems to me that category theory (on the surface at least) is
more suitable to the mathematical aims of Axiom. I would like to
be able to think about type safety in these terms.

Regards,
Bill Page.