Re: [Axiom-developer] B#

[Gabriel Dos Reis]

"Bill Page" <address@hidden> writes:

| On November 21, 2005 2:56 PM Gaby wrote:
| > ... 
| > | > | I still think the referenced article is well balanced
| > | > | and accurate.
| > | > 
| > | > I don't think so  If is full of confusion and misunderstanding.
| > | 
| > | You have given only one example of something you disagree with
| > 
| > You're very kind in crediting me as author of the example you put
| > forward :-)
| >
| 
| Well, I suppose I should have been a little more careful with
| my example. How about this:
| 
| $ gcc --version;cat cast1.c; gcc -o cast1 cast1.c; cast1
| gcc.exe (GCC) 3.4.2 (mingw-special)
| Copyright (C) 2004 Free Software Foundation, Inc.
| This is free software; see the source for copying conditions.  There is NO
| warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
| 
| /*
|   'caste' example of weak typing in C
|    Author: Bill Page
|    Date: 21 Nov 2005
| */
| #include <stdio.h>
| int main(int argn, char *argv[]) {
| int i;
| float j;
| 
|   i = 1;
|   j = (float)i;
|   printf("float: %d\n",j);
|   return 0;
| }
| float: 0
| 
| ----------
| 
| Does this program conform to ISO C99?

No, it does not.
Because of the obvious reasons -- passing in double (yes, floats get
promoted to doubles when passed in ellipsis) and telling printf() to
access if as int.  That is undefined behaviour according to ISO C
rules.  
Good compilers would catch such cases; and good runtimes would also catch
it. 

| Does it compile with
| your newer version of gcc? Does it produce a result that you
| expect?

GCC has format checkin -- which gets improved every release -- and
mine says

   merlin[16:37]% cat bad-format.c && gcc -Wformat bad-format.c
   /*
       'caste' example of weak typing in C
          Author: Bill Page
             Date: 21 Nov 2005
   */
   #include <stdio.h>
   int main(int argn, char *argv[]) {
      int i;
      float j;

      i = 1;
      j = (float)i;
      printf("float: %d\n",j);
      return 0;
   }
   bad-format.c: In function 'main':
   bad-format.c:13: warning: format '%d' expects type 'int', but argument 2 has 
type 'double'

| > ... 
| > | > Unfortunately, many people take it as a Bible sentence
| > | > don't go and do a minimum scrutinity as would be required
| > | > in a scientific setting :-(
| > | > 
| > | 
| > | Maybe some people do, but I do not intend to accept such an
| > | attitude. I think I have applied much more than "minimum
| > | scrutiny" to this article. Of course it is difficult to be
| > | entirely accurate in an article that is intended to be at
| > | most one or two pages.
| > 
| > Well, don't take it as a personal thing.  My comment was very
| > broad and was not targetting you specifically.  It upset me you
| > took it personally.
| 
| No problem, I do not mind being "targetted" even if you did
| not intend it. Please don't worry that I took it "personally",

OK, thanks.

| but I did take it seriously and I think you meant it seriously,
| right?

yes.

| > ... 
| > Notice I'm not disputing that the term "strong typing" is
| > ambiguous. I'm disagreeing with the claims that the C
| > programming language was supposed to illustrate.
| 
| Do you think my improved example illustrates this point?

Not really -- not in the sense that the compiler would be _required_
to accept it. A compiler is not required to accept an ill-formed
program.  I believe that is main point of confusion when people
talk about the C type system. 

I would concede it exhibits the C type system as a "weak system" --
not in the sense that the C semantics requires the compiler (or the
runtime) to accept the program.  It illustrates the weakness in the
sense that such an error (from the language semantics point of view)
can be made very easily -- see my previous message. 

| > (I know of lot of deficiencies in C -- it is hard not to,
| > when you're involved in its specification and implementation)
| > but none of the examples I've so far are illustrative of the
| > claim of "weak typing".
| 
| I am very glad that you have been active in the standardization
| of C and that you are here discussing Axiom. Perhaps some day
| we will be talking about standardization of computer algebra
| languages?

probably, but I would first need to make a good contribution,
implementation wise :-)
I'm glad Tim followed up on the Lyon meeting by having the Axiom
happening free.

| > | Could you provide a reference to a short article that you
| > | think is less "full of confusion and misunderstanding"?
| > 
| > About C?  The shortest is the ISO C specification :-)
| > 
| 
| That is a pity.

Indeed.

| Suppose we agree to strike all references of C from the
| Wikipedia article:
| 
| http://en.wikipedia.org/wiki/Datatype
| 
| then would you consider it a reasonable brief discussion of
| type systems in programming languages?

well, it depends at what level.  For a simple introductory material
for freshmen, that would probably do.
But I'm not sure I would take it as a basis for more serious
discussions on type systems in programming languages.

The point is, it starts with equating "datatype" with "types", then
builds on a set-theoretic centric notion of type.  However,
polymorphism, for example, is not set-theoretic (see Reynolds).  I
don't think I agree that is reasonable.  
Type system is not a simple matter -- it took Pierce about 6 hundreds
pages to introduce the basic notions (and another volume to talk about
"advanced" type systems.) 

I'm not claiming I have better answers; I'm just dubitative that the
material you point to is a reasonable summary.  However, it is a
material to be read by all parties :-)

-- Gaby