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. _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer
