Python from Wise Guy's Viewpoint

[Ed Avis]

prunesquallor at comcast.net writes:

>As I mentioned earlier in this thread, the two things I object to in a
>static type system are these:
>
>    1)  The rejection of code I know to be useful, yet the system is
>        unable to prove correct.

This has never happened to me with Haskell, and I don't think it has
ever happened with C.  With C++ I have often felt as though the type
system was being picky and getting in the way, but this was usually a
case of me finding it difficult to make my intentions clear to the
compiler - which is also a disadvantage of static typing, of course.
Languages like Haskell and ML don't tend to suffer that problem,
because the type system is a bit more understandable than C++ and will
infer things it's not told explicitly.

>    2)  The requirement that I decorate my program with type
>        information to give the type checker hints to enable it 
>        to check things that are, to me, obviously correct.

This is why type inference as used in the above-mentioned languages
and many others is so useful.  You can still add explicit type
declarations where you want to, either to help find out where you have
made a mistake (analogously to putting in extra assertions to narrow
down the point where something goes wrong at run time) and to act as
documentation (which, unlike comments, is automatically checked by the
compiler to make sure it's up to date).

>To my knowledge, not one of my fellow lisp hackers would mind a
>static type checker that noticed code fragments that could be proven
>to never produce anything but an error provided that said type
>checker never need hints and is never wrong.

I believe this is what you get with standard Haskell (though some
language extensions may require explicit type annotations in some
places).  Certainly the type checker is never wrong: it never flags a
type error in a correct program, and never gives the all-clear for a
program containing a type error.

But of course, the checker is checking Haskell programs, not Lisp
programs.  Nobody is suggesting to use some form of full compile-time
type checking on Common Lisp, nor could such a thing exist.

[later]

>This appears to be getting very close to arguing that static type
>checkers never reject useful programs because, by definition, a
>program rejected by a static type checker is useless.

Absolutely true - in a statically typed language!  In Lisp or a
dynamically typed language, obviously not true - except that the
statement doesn't really make any sense for Lisp, because one cannot
write a full static type checker for that language.

-- 
Ed Avis <ed at membled.com>