THE GOOD:
1. pickle
2. simplicity and uniformity
3. big library (bigger would be even better)
THE BAD:
1. f(x,y,z) sucks. f x y z would be much easier to type (see Haskell)
90% of the code is function applictions. Why not make it convenient?
2. Statements vs Expressions business is very dumb. Try writing
a = if x :
y
else: z
3. no multimethods (why? Guido did not know Lisp, so he did not know
about them) You now have to suffer from visitor patterns, etc. like
lowly Java monkeys.
4. splintering of the language: you have the inefficient main language,
and you have a different dialect being developed that needs type
declarations. Why not allow type declarations in the main language
instead as an option (Lisp does it)
5. Why do you need "def" ? In Haskell, you'd write
square x = x * x
6. Requiring "return" is also dumb (see #5)
7. Syntax and semantics of "lambda" should be identical to
function definitions (for simplicity and uniformity)
8. Can you undefine a function, value, class or unimport a module?
(If the answer is no to any of these questions, Python is simply
not interactive enough)
9. Syntax for arrays is also bad [a (b c d) e f] would be better
than [a, b(c,d), e, f]
420
P.S. If someone can forward this to python-dev, you can probably save some
people a lot of soul-searching
Jul 18 '05
467  20177 
Here's a link to a relavant system that may be worthwhile to check out: http://www.simulys.com/guideto.htm
--
; Matthew Danish <md*****@andrew.cmu.edu>
; OpenPGP public key: C24B6010 on keyring.debian.org
; Signed or encrypted mail welcome.
; "There is no dark side of the moon really; matter of fact, it's all dark."
Marshall Spight wrote: "Pascal Costanza" <co******@web.de> wrote in message news:bn**********@newsreader2.netcologne.de...
When do programmers know better? An int is an int and a string is a
string, and nary the twain shall be treated the same. I would rather
``1 + "bar"'' signal an error at compile time than at run time.
Such code would easily be caught very soon in your unit tests.
Provided you think to write such a test, and expend the effort
to do so. Contrast to what happens in a statically typed language,
where this is done for you automatically.
There are other things that are done automatically for me in dynamically
typed languages that I care more about than such static checks. I don't
recall ever writing 1 + "bar". (Yes, this is a rhetorical statement. ;)
Unit tests are great; I heartily endorse them. But they *cannot*
do everything that static type checking can do. Likewise,
static type checking *cannot* do everything unit testing
can do.
Right.
So again I ask, why is it either/or? Why not both? I've had
*great* success building systems with comprehensive unit
test suites in statically typed languages. The unit tests catch
some bugs, and the static type checking catches other bugs.
That's great for you, and if it works for you, just keep it up.
But I have given reasons why one would not want to have static type
checking by default. All I am trying to say is that this depends on the
context. Static type systems are definitely not _generally_ better than
dynamic type systems.
Pascal
Pascal Costanza <co******@web.de> wrote in message news:<bn**********@newsreader2.netcologne.de>...
+ Design process: There are clear indications that processes like
extreme programming work better than processes that require some kind of
specification stage. Dynamic typing works better with XP than static
typing because with dynamic typing you can write unit tests without
having the need to immediately write appropriate target code.
This is utterly bogus. If you write unit tests beforehand, you are
already pre-specifying the interface that the code to be tested will
present.
I fail to see how dynamic typing can confer any kind of advantage here.
+ Documentation: Comments are usually better for handling documentation.
;) If you want your "comments" checked, you can add assertions.
Are you seriously claiming that concise, *automatically checked*
documentation (which is one function served by explicit type
declarations) is inferior to unchecked, ad hoc commenting?
For one thing, type declarations *cannot* become out-of-date (as
comments can and often do) because a discrepancy between type
declaration and definition will be immidiately flagged by the compiler.
+ Error checking: I can only guess what you mean by this. If you mean
something like Java's checked exceptions, there are clear signs that
this is a very bad feature.
I think Fergus was referring to static error checking, but (and forgive
me if I'm wrong here) that's a feature you seem to insist has little or
no practical value - indeed, you seem to claim it is even an impediment
to productive programming. I'll leave this point as one of violent
disagreement...
+ Efficiency: As Paul Graham puts it, efficiency comes from profiling.
In order to achieve efficiency, you need to identify the bottle-necks of
your program. No amount of static checks can identify bottle-necks, you
have to actually run the program to determine them.
I don't think you understand much about language implementation.
A strong, expressive, static type system provides for optimisations
that cannot be done any other way. These optimizations alone can be
expected to make a program several times faster. For example:
- no run-time type checks need be performed;
- data representation is automatically optimised by the compiler
(e.g. by pointer tagging);
- polymorphic code can be inlined and/or specialised according to each
application;
- if the language does not support dynamic typing then values need not
carry their own type identifiers around with them, thereby saving
space;
- if the language does support explicit dynamic typing, then only
those places using that facility need plumb in the type identifiers
(something done automatically by the compiler.)
On top of all that, you can still run your code through the profiler,
although the need for hand-tuned optimization (and consequent code
obfuscation) may be completely obviated by the speed advantage
conferred by the compiler exploiting a statically checked type system.
I wouldn't count the use of java.lang.Object as a case of dynamic
typing. You need to explicitly cast objects of this type to some class
in order to make useful method calls. You only do this to satisfy the
static type system. (BTW, this is one of the sources for potential bugs
that you don't have in a decent dynamically typed language.)
No! A thousand times, no!
Let me put it like this. Say I have a statically, expressively, strongly
typed language L. And I have another language L' that is identical to
L except it lacks the type system. Now, any program in L that has the
type declarations removed is also a program in L'. The difference is
that a program P rejected by the compiler for L can be converted to a
program P' in L' which *may even appear to run fine for most cases*.
However, and this is the really important point, P' is *still* a
*broken* program. Simply ignoring the type problems does not make
them go away: P' still contains all the bugs that program P did. Soft typing systems give you dynamic typing unless you explicitly ask
for static typing. That is the wrong default, IMHO. It works much
better to add dynamic typing to a statically typed language than the
other way around.
I don't think so.
Yes, but your arguments are unconvincing. I should point out that
most of the people on comp.lang.functional (a) probably used weakly/
dynamically typed languages for many years, and at an expert level,
before discovering statically typed (declarative) programming and
(b) probably still do use such languages on a regular basis.
Expressive, static typing is not a message shouted from ivory towers
by people lacking real-world experience.
Why not make the argument more concrete? Present a problem
specification for an every-day programming task that you think
seriously benefits from dynamic typing. Then we can discuss the
pros and cons of different approaches.
-- Ralph
Matthias Blume wrote: Pascal Costanza <co******@web.de> writes:
The set of programs that are useful but cannot be checked by a static
type system is by definition bigger than the set of useful programs
that can be statically checked.
By whose definition? What *is* your definition of "useful"? It is
clear to me that static typing improves maintainability, scalability,
and helps with the overall design of software. (At least that's my
personal experience, and as others can attest, I do have reasonably
extensive experience either way.)
A 100,000 line program in an untyped language is useless to me if I am
trying to make modifications -- unless it is written in a highly
stylized way which is extensively documented (and which usually means
that you could have captured this style in static types). So under
this definition of "useful" it may very well be that there are fewer
programs which are useful under dynamic typing than there are under
(modern) static typing.
A statically typed program is useless if one tries to make modifications
_at runtime_. There are software systems out there that make use of
dynamic modifications, and they have a strong advantage in specific
areas because of this.
If you can come up with a static type system for an unrestricted runtime
metaobject protocol, then I am fine with static typing.
So dynamically typed languages allow
me to express more useful programs than statically typed languages.
There are also programs which I cannot express at all in a purely
dynamically typed language. (By "program" I mean not only the executable
code itself but also the things that I know about this code.)
Those are the programs which are protected against certain bad things
from happening without having to do dynamic tests to that effect
themselves.
This is a circular argument. You are already suggesting the solution in
your problem description.
(Some of these "bad things" are, in fact, not dynamically
testable at all.)
For example?
I don't question that. If this works well for you, keep it up. ;)
Don't fear. I will.
....and BTW, please let me keep up using dynamically typed languages,
because this works well for me!
(That's the whole of my answer to the original question, why one would
want to give up static typing.)
(And where are _your_ empirical studies which show that "working around
language restrictions increases the potential for bugs"?)
I don't need a study for that statement because it's a simple
argument: if the language doesn't allow me to express something in a
direct way, but requires me to write considerably more code then I
have considerably more opportunities for making mistakes.
This assumes that there is a monotone function which maps token count
to error-proneness and that the latter depends on nothing else. This
is a highly dubious assumption. In many cases the few extra tokens
you write are exactly the ones that let the compiler verify that your
thinking process was accurate (to the degree that this fact is
captured by types). If you get them wrong *or* if you got the
original code wrong, then the compiler can tell you. Without the
extra tokens, the compiler is helpless in this regard.
See the example of downcasts in Java.
To make a (not so far-fetched, btw :) analogy: Consider logical
statements and formal proofs. Making a logical statement is easy and
can be very short. It is also easy to make mistakes without noticing;
after all saying something that is false while still believing it to
be true is extremely easy. Just by looking at the statement it is
also often hard to tell whether the statement is right. In fact,
computers have a hard time with this task, too. Theorem-proving is
hard.
On the other hand, writing down the statement with a formal proof is
impossible to get wrong without anyone noticing because checking the
proof for validity is trivial compared to coming up with it in the
first place. So even though writing the statement with a proof seems
harder, once you have done it and it passes the proof checker you can
rest assured that you got it right. The longer "program" will have fewer
"bugs" on average.
Yes, but then you have a proof that is tailored to the statement you
have made. The claim of people who favor static type systems is that
static type systems are _generally_ helpful.
Pascal
Andrew Dalke wrote: Pascal Costanza:
The set of programs that are useful but cannot be checked by a static
type system is by definition bigger than the set of useful programs that
can be statically checked. So dynamically typed languages allow me to
express more useful programs than statically typed languages.
Ummm, both are infinite and both are countably infinite, so those sets
are the same size. You're falling for Hilbert's Paradox.
Also, while I don't know a proof, I'm pretty sure that type inferencing
can do addition (and theorem proving) so is equal in power to
programming.
Just give me a static type system CLOS + MOP. I don't need a study for that statement because it's a simple argument:
if the language doesn't allow me to express something in a direct way,
but requires me to write considerably more code then I have considerably
more opportunities for making mistakes.
The size comparisons I've seen (like the great programming language
shootout) suggest that Ocaml and Scheme require about the same amount
of code to solve small problems. Yet last I saw, Ocaml is strongly typed
at compile time. How do you assume then that strongly&statically typed
languages require "considerable more code"?
_small_ problems?
Pascal
Lulu of the Lotus-Eaters <me***@gnosis.cx> writes: Joachim Durchholz <jo***************@web.de> writes:My 100% subjective private study reveals not a single complaint about
over-restrictive type systems in comp.lang.functional in the last 12
months.
I also read c.l.functional (albeit only lightly). In the last 12
months, I have encountered dozens of complaints about over-restrictive
type sytems in Haskell, OCaml, SML, etc.
The trick is that these complaints are not phrased in precisely that
way. Rather, someone is trying to do some specific task, and has
difficulty arriving at a usable type needed in the task. Often posters
provide good answers--Durchholz included. But the underlying complaint
-really was- about the restrictiveness of the type system.
Could you provide a link to an example of such a post?
In my experience, people who have difficulties in getting their programs
to typecheck usually have an inconsistent design, not a design which is
consistent but which the type checker is too restrictive to support.
--
Fergus Henderson <fj*@cs.mu.oz.au> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
Marshall Spight wrote: "Pascal Costanza" <co******@web.de> wrote in message news:bn**********@newsreader2.netcologne.de...
I wouldn't count the use of java.lang.Object as a case of dynamic
typing. You need to explicitly cast objects of this type to some class
in order to make useful method calls. You only do this to satisfy the
static type system. (BTW, this is one of the sources for potential bugs
that you don't have in a decent dynamically typed language.)
Huh? The explicit-downcast construct present in Java is the
programmer saying to the compiler: "trust me; you can accept
this type of parameter." In a dynamically-typed language, *every*
call is like this! So if this is a source of errors (which I believe it
is) then dynamically-typed languages have this potential source
of errors with every function call, vs. statically-typed languages
which have them only in those few cases where the programmer
explicitly puts them in.
What can happen in Java is the following:
- You might accidentally use the wrong class in a class cast.
- For the method you try to call, there happens to be a method with the
same name and signature in that class.
In this situation, the static type system would be happy, but the code
is buggy.
In a decent dynamically typed language, you have proper name space
management, so that a method cannot ever be defined for a class only by
accident.
(Indeed, Java uses types for many different unrelated things - in this
case as a very weak name space mechanism.)
Pascal
Ralph Becket wrote: Pascal Costanza <co******@web.de> wrote in message news:<bn**********@newsreader2.netcologne.de>...
+ Design process: There are clear indications that processes like
extreme programming work better than processes that require some kind of
specification stage. Dynamic typing works better with XP than static
typing because with dynamic typing you can write unit tests without
having the need to immediately write appropriate target code.
This is utterly bogus. If you write unit tests beforehand, you are
already pre-specifying the interface that the code to be tested will
present.
I fail to see how dynamic typing can confer any kind of advantage here.
Read the literature on XP.
+ Documentation: Comments are usually better for handling documentation.
;) If you want your "comments" checked, you can add assertions.
Are you seriously claiming that concise, *automatically checked*
documentation (which is one function served by explicit type
declarations) is inferior to unchecked, ad hoc commenting?
I am sorry, but in my book, assertions are automatically checked.
For one thing, type declarations *cannot* become out-of-date (as
comments can and often do) because a discrepancy between type
declaration and definition will be immidiately flagged by the compiler.
They same holds for assertions as soon as they are run by the test suite.
+ Error checking: I can only guess what you mean by this. If you mean
something like Java's checked exceptions, there are clear signs that
this is a very bad feature.
I think Fergus was referring to static error checking, but (and forgive
me if I'm wrong here) that's a feature you seem to insist has little or
no practical value - indeed, you seem to claim it is even an impediment
to productive programming. I'll leave this point as one of violent
disagreement...
It has value for certain cases, but not in general.
+ Efficiency: As Paul Graham puts it, efficiency comes from profiling.
In order to achieve efficiency, you need to identify the bottle-necks of
your program. No amount of static checks can identify bottle-necks, you
have to actually run the program to determine them.
I don't think you understand much about language implementation.
....and I don't think you understand much about dynamic compilation. Have
you ever checked some not-so-recent-anymore work about, say, the HotSpot
virtual machine?
A strong, expressive, static type system provides for optimisations
that cannot be done any other way. These optimizations alone can be
expected to make a program several times faster. For example:
- no run-time type checks need be performed;
- data representation is automatically optimised by the compiler
(e.g. by pointer tagging);
- polymorphic code can be inlined and/or specialised according to each
application;
- if the language does not support dynamic typing then values need not
carry their own type identifiers around with them, thereby saving
space;
- if the language does support explicit dynamic typing, then only
those places using that facility need plumb in the type identifiers
(something done automatically by the compiler.)
You are only talking about micro-efficiency here. I don't care about
that, my machine is fast enough for a decent dynamically typed language.
On top of all that, you can still run your code through the profiler,
although the need for hand-tuned optimization (and consequent code
obfuscation) may be completely obviated by the speed advantage
conferred by the compiler exploiting a statically checked type system.
Have you checked this?
I wouldn't count the use of java.lang.Object as a case of dynamic
typing. You need to explicitly cast objects of this type to some class
in order to make useful method calls. You only do this to satisfy the
static type system. (BTW, this is one of the sources for potential bugs
that you don't have in a decent dynamically typed language.)
No! A thousand times, no!
Let me put it like this. Say I have a statically, expressively, strongly
typed language L. And I have another language L' that is identical to
L except it lacks the type system. Now, any program in L that has the
type declarations removed is also a program in L'. The difference is
that a program P rejected by the compiler for L can be converted to a
program P' in L' which *may even appear to run fine for most cases*.
However, and this is the really important point, P' is *still* a
*broken* program. Simply ignoring the type problems does not make
them go away: P' still contains all the bugs that program P did.
You are making several mistakes here. I don't argue for languages that
don't have a type system, I argue for languages that are dynamically
typed. We are not debating strong typing.
Furthermore, a program P that is rejected by L is not necessarily broken.
Soft typing systems give you dynamic typing unless you explicitly ask
for static typing. That is the wrong default, IMHO. It works much
better to add dynamic typing to a statically typed language than the
other way around.
I don't think so.
Yes, but your arguments are unconvincing. I should point out that
most of the people on comp.lang.functional (a) probably used weakly/
dynamically typed languages for many years, and at an expert level,
before discovering statically typed (declarative) programming and
Weak and dynamic typing is not the same thing.
(b) probably still do use such languages on a regular basis.
Expressive, static typing is not a message shouted from ivory towers
by people lacking real-world experience.
Why not make the argument more concrete? Present a problem
specification for an every-day programming task that you think
seriously benefits from dynamic typing. Then we can discuss the
pros and cons of different approaches.
No. The original question asked in this thread was along the lines of
why abandon static type systems and why not use them always. I don't
need to convince you that a proposed general solution doesn't always
work, you have to convince me that it always works.
Otherwise I could come up with some other arbitrary restriction and
claim that it is a general solution for writing better programs, and ask
you to give counter-examples as well. This is not a reasonable approach
IMHO.
There are excellent programs out there that have been written with
static type systems, and there are also excellent programs out there
that have been written without static type systems. This is a clear
indication that static type systems are not a necessary condition for
writing excellent programs.
Furthermore, there are crap programs out there that have been written
with static type systems, so a static type system is also not a
sufficient condition for writing good software.
The burden of proof is on the one who proposes a solution.
Pascal
Fergus Henderson wrote: In my experience, people who have difficulties in getting their programs
to typecheck usually have an inconsistent design, not a design which is
consistent but which the type checker is too restrictive to support.
Have you made sure that this is not a circular argument?
Does "consistent design" mean "acceptable by a type checker" in your book?
Pascal
Pascal Costanza <co******@web.de> wrote: You need some testing discipline, which is supported well by unit
testing frameworks.
IMHO it helps to think about static typing as a special kind of unit
tests. Like unit tests, they verify that for some input values, the
function in question will produce the correct output values. Unlike
unit tests, they do this for a class of values, instead of testing
statistically by example. And unlike unit tests, they are pervasive:
Every execution path will be automatically tested; you don't have
to invest brain power to make sure you don't forget one.
Type inference will automatically write unit tests for you (besides
other uses like hinting that a routine may be more general than you
thought). But since the computer is not very smart, they will test
only more or less trivial things. But that's still good, because then
you don't have to write the trivial unit tests, and only have to care
about the non-trivial ones.
Type annotations are an assertion language that you use to write down
that kind of unit tests.
Static type systems are claimed to generally improve your code. I
don't see that.
They do it for the same reason that unit tests do:
* They are executable documention.
* By writing them down first, you focus on what you want to do.
* They help with refactoring.
etc.
Of course you can replace the benefits of static typing by enough unit
tests. But they are different verification tools: For some kind of
problems, one is better, for other kinds, the other. There's no reason
not to use both.
- Dirk
Andrew Dalke wrote: If a few rockets blow up for testing then it's still cheaper than
quintupling the development costs.
Not quite - that was a loss of 500 million dollars. I don't know what
the software development costs were, so I'm just guessing here, but I
think it's relatively safe to assume a doubly redundant system would
already have paid off if it had caught the problem.
The point is that no amount of software technology would have caught the
problem if the specifications are wrong. I think it would have been more
successful if there had been some automated specification checking,
which is safely in the area of theorem proving - which has interesting
connections to static type checking but is otherwise unrelated to
programming.
Regards,
Jo
Pascal Costanza wrote: For example, static type systems are incompatible with dynamic
metaprogramming. This is objectively a reduction of expressive power,
because programs that don't allow for dynamic metaprogramming can't be
extended in certain ways at runtime, by definition.
What is dynamic metaprogramming?
Regards,
Jo
Dirk Thierbach wrote: Pascal Costanza <co******@web.de> wrote: You need some testing discipline, which is supported well by unit
testing frameworks.
IMHO it helps to think about static typing as a special kind of unit
tests. Like unit tests, they verify that for some input values, the
function in question will produce the correct output values. Unlike
unit tests, they do this for a class of values, instead of testing
statistically by example. And unlike unit tests, they are pervasive:
Every execution path will be automatically tested; you don't have
to invest brain power to make sure you don't forget one.
IMHO typical unit-tests in python go a lot further than just testing
types. They test *behaviour* rather than just types. Thus I tend to
think that for languages like python unittests are a *perfect match*
because there is hardly any redundancy and they are very short to write
down usually. Writing unittests in a statically typed language is more
redundant because - like you say - type declarations already are a kind
of (IMO very limited) tests.
cheers,
holger
Dirk Thierbach wrote: Pascal Costanza <co******@web.de> wrote:
You need some testing discipline, which is supported well by unit
testing frameworks.
IMHO it helps to think about static typing as a special kind of unit
tests. Like unit tests, they verify that for some input values, the
function in question will produce the correct output values. Unlike
unit tests, they do this for a class of values, instead of testing
statistically by example. And unlike unit tests, they are pervasive:
Every execution path will be automatically tested; you don't have
to invest brain power to make sure you don't forget one.
This is clear.
Type inference will automatically write unit tests for you (besides
other uses like hinting that a routine may be more general than you
thought). But since the computer is not very smart, they will test
only more or less trivial things. But that's still good, because then
you don't have to write the trivial unit tests, and only have to care
about the non-trivial ones.
Unless the static type system takes away the expressive power that I need.
Type annotations are an assertion language that you use to write down
that kind of unit tests.
Yep.
Of course you can replace the benefits of static typing by enough unit
tests. But they are different verification tools: For some kind of
problems, one is better, for other kinds, the other. There's no reason
not to use both.
I have given reasons when not to use a static type system in this
thread. Please take a look at the Smalltalk MOP or the CLOS MOP and tell
me what a static type system should look like for these languages!
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Joachim Durchholz wrote: Pascal Costanza wrote:
For example, static type systems are incompatible with dynamic
metaprogramming. This is objectively a reduction of expressive power,
because programs that don't allow for dynamic metaprogramming can't be
extended in certain ways at runtime, by definition.
What is dynamic metaprogramming?
Writing programs that inspect and change themselves at runtime.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Andrew Dalke wrote: Pascal Costanza:
The set of programs that are useful but cannot be checked by a static
type system is by definition bigger than the set of useful programs that
can be statically checked. So dynamically typed languages allow me to
express more useful programs than statically typed languages.
Ummm, both are infinite and both are countably infinite, so those sets
are the same size. You're falling for Hilbert's Paradox.
The sets in question are not /all/ dynamically/statically typed
programs, they are all dynamically/statically typed programs that fit
any item in the set of specifications in existence. Which is a very
finite set.
Also, while I don't know a proof, I'm pretty sure that type inferencing
can do addition (and theorem proving) so is equal in power to
programming.
Nope. It depends on the type system used: some are decidable, some are
undecidable, and for some, decidability is unknown.
Actually, for decidable type inference systems, there's also the
distinction between exponential, polynomial, O (N log N), and linear
behaviour; for some systems, the worst-case behaviour is unknown but
benevolent in practice.
The vast majority of practical programming languages use a type
inference system where the behavior is known to be O (N log N) or better :-)
(meaning that the other type systems and associated inference algorithms
are research subjects and/or research tools)
Regards,
Jo
Pascal Costanza wrote: Fergus Henderson wrote:
In my experience, people who have difficulties in getting their programs
to typecheck usually have an inconsistent design, not a design which is
consistent but which the type checker is too restrictive to support.
Have you made sure that this is not a circular argument?
Does "consistent design" mean "acceptable by a type checker" in your book?
Matthias Blume already posted that the type checker caught several
design errors. He's not the only to post such reports, I regularly
statements like that on comp.lang.functional.
Regards,
Jo
Pascal Costanza wrote: Ralph Becket wrote: I fail to see how dynamic typing can confer any kind of advantage here.
Read the literature on XP.
Note that most literature contrasts dynamic typing with the static type
systems of C++ and/or Java. Good type systems are /far/ better.
Are you seriously claiming that concise, *automatically checked*
documentation (which is one function served by explicit type
declarations) is inferior to unchecked, ad hoc commenting?
I am sorry, but in my book, assertions are automatically checked.
But only at runtime, where a logic flaw may or may not trigger the
assertion.
(Assertions are still useful: if they are active, they prove that the
errors checked by them didn't occur in a given program run. This can
still be useful. But then, production code usually runs with assertion
checking off - which is exactly the point where knowing that some bug
occurred would be more important...)
For one thing, type declarations *cannot* become out-of-date (as
comments can and often do) because a discrepancy between type
declaration and definition will be immidiately flagged by the compiler.
They same holds for assertions as soon as they are run by the test suite.
A test suite can never catch all permutations of data that may occur (on
a modern processor, you can't even check the increment-by-one operation
with that, the universe will end before the CPU has counted even half of
the full range).
+ Efficiency: As Paul Graham puts it, efficiency comes from
profiling. In order to achieve efficiency, you need to identify the
bottle-necks of your program. No amount of static checks can identify
bottle-necks, you have to actually run the program to determine them.
I don't think you understand much about language implementation.
....and I don't think you understand much about dynamic compilation.
Have you ever checked some not-so-recent-anymore work about, say, the
HotSpot virtual machine?
Well, I did - and the results were, ahem, unimpressive.
Besides, HotSpot is for Java, which is statically typed, so I don't
really see your point here... unless we're talking about different VMs.
And, yes, VMs got pretty fast these days (and that actually happened
several years ago).
It's only that compiled languages still have a good speed advantage -
making a VM fast requires just that extra amount of effort which, when
invested into a compiler, will make the compiled code still run faster
than the VM code.
Also, I have seen several cases where VM code just plain sucked
performance-wise until it was carefully hand-optimized. (A concrete
example: the all-new, great graphics subsystem for Squeak that could do
wonders like rendering fonts with all sorts of funky effects, do 3D
transformations on the fly, and whatnot... I left Squeak before those
optimizations became mainstream, but I'm pretty sure that Squeak got
even faster. Yet Squeak is still a bit sluggish... only marginally so,
and certainly no more sluggish than the bloatware that's around and that
commercial programmers are forced to write, but efficiency is simply
more of a concern and a manpower hog than with a compiled language.)
There are excellent programs out there that have been written with
static type systems, and there are also excellent programs out there
that have been written without static type systems. This is a clear
indication that static type systems are not a necessary condition for
writing excellent programs.
Hey, there are also excellent programs written in assembly. By your
argument, using a higher language is not a necessary condition for
writing excellent languages.
The question is: what effort goes into an excellent program? Is static
typing a help or a hindrance?
One thing I do accept: that non-inferring static type systems like those
of C++ and Java are a PITA. Changing a type in some interface tends to
cost a day or more, chasing all the consequences in callers, subclasses,
and whatnot, and I don't need that (though it does tell me all the
places where I should take a look to check if the change didn't break
anything, so this isn't entirely wasted time).
I'm still unconvinced that an inferring type system is worse than
run-time type checking. (Except for that "dynamic metaprogramming" thing
I'd like to know more about. In my book, things that are overly powerful
are also overly uncontrollable, but that may be an exception.)
Regards,
Jo
Pascal Costanza wrote: See the example of downcasts in Java.
Please do /not/ draw your examples from Java, C++, or Eiffel. Modern
static type systems are far more flexible and powerful, and far less
obtrusive than the type systems used in these languages.
A modern type system has the following characteristics:
1. It's safe: Code that type checks cannot assign type-incorrect values
(as opposed to Eiffel).
2. It is expressive: There's no need to write type casts (as opposed to
C++ and Java). (The only exceptions where type casts are necessary are
those where it is logically unavoidable: e.g. when importing binary data
from an untyped source.)
3. It is unobtrusive: The compiler can infer most if not all types by
itself. Modifying some code so that it is slightly more general will
thus automatically acquire the appropriate slightly more general type.
4. It is powerful: any type may have other types as parameters. Not only
for container types such as Array <Integer>, but also for other
purposes. Advanced type systems can even express mutually recursive
types - an (admittedly silly) example: trees that have alternating node
types on paths from root to leaves. (And all that without type casts,
Mum! *g*)
Regards,
Jo
Joachim Durchholz wrote:
The vast majority of practical programming languages use a type
inference system where the behavior is known to be O (N log N) or better
Not true, unfortunately. Type inference for almost all FP languages is a
derivative from the original Hindley/Milner algorithm for ML, which is
known to have exponential worst-case behaviour. Interestingly, such
cases never show up in practice, most realistic programs can be checked
in subquadratic time and space. For that reason even the inventors of
the algorithm originally believed it was polynomial, until somebody
found a counterexample.
The good news is that, for similar reasons, undecidable type checking
need not be a hindrance in practice.
- Andreas
--
Andreas Rossberg, ro******@ps.uni-sb.de
"Computer games don't affect kids; I mean if Pac Man affected us
as kids, we would all be running around in darkened rooms, munching
magic pills, and listening to repetitive electronic music."
- Kristian Wilson, Nintendo Inc.
Fergus Henderson <fj*@cs.mu.oz.au> writes: Lulu of the Lotus-Eaters <me***@gnosis.cx> writes:
Joachim Durchholz <jo***************@web.de> writes:My 100% subjective private study reveals not a single complaint about
over-restrictive type systems in comp.lang.functional in the last 12
months.
I also read c.l.functional (albeit only lightly). In the last 12
months, I have encountered dozens of complaints about over-restrictive
type sytems in Haskell, OCaml, SML, etc.
The trick is that these complaints are not phrased in precisely that
way. Rather, someone is trying to do some specific task, and has
difficulty arriving at a usable type needed in the task. Often posters
provide good answers--Durchholz included. But the underlying complaint
-really was- about the restrictiveness of the type system.
Could you provide a link to an example of such a post?
I've no link but I'm sure to have seen (here or on one of the caml
list) people trying to do polymorphic recursion, something that is not
easy to do in ocaml...
--
Rémi Vanicat
In comp.lang.lisp Matthias Blume <fi**@my.address.elsewhere> wrote:
Apologies for the out-of-context snippage: A 100,000 line program in an untyped language is useless to me if I am
^^^^^^^
Your choice of word here makes me suspect that you _may_ understand
something quite different than most of the residents of cll and clp by
dynamic typing:
dynamic typing is *not* the same as untyped!
Of course, maybe it was just an unfortunate choice of words.
Cheers,
-- Nikodemus
Joachim Durchholz wrote: Pascal Costanza wrote:
See the example of downcasts in Java.
Please do /not/ draw your examples from Java, C++, or Eiffel. Modern
static type systems are far more flexible and powerful, and far less
obtrusive than the type systems used in these languages.
This was just one obvious example in which you need a workaround to make
the type system happy. There exist others.
A modern type system has the following characteristics:
I know what modern type systems do.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Matthias Blume wrote: Pascal Costanza <co******@web.de> writes:
The set of programs that are useful but cannot be checked by a static
type system is by definition bigger than the set of useful programs
that can be statically checked.
By whose definition? What *is* your definition of "useful"? It is
clear to me that static typing improves maintainability, scalability,
and helps with the overall design of software.
That sounds right. When I divided a large app into half a dozen sensible
packages, several violations of clean design were revealed. But just a
few, and there was a ton of code.
I did a little C++ and Java once, porting Cells to those languages. This
was existing code, so I did not have to explore as I coded. It was a
total pain, but then it was pretty easy to get working because so many
casual goofs got caught by the compiler.
I just would never want to write original code this way, because then I
am working fast and loose, doing this, doing that, leaving all sorts of
code in limbo which would have to be straightened out to satisfy a compiler.
The other problem with static typing is that it does not address the
real problem with scaling, viz, the exponential explosion of state
interdependencies. A compiler cannot check the code I neglect to write,
leaving state change unpropagated to dependent other state, nor can it
check the sequence of correctly typed statements to make sure state used
in calculation X is updated before I use that state.
kenny
-- http://tilton-technology.com
What?! You are a newbie and you haven't answered my: http://alu.cliki.net/The%20Road%20to%20Lisp%20Survey
Joachim Durchholz wrote: Pascal Costanza wrote:
Ralph Becket wrote:
I fail to see how dynamic typing can confer any kind of advantage here.
Read the literature on XP.
Note that most literature contrasts dynamic typing with the static type
systems of C++ and/or Java. Good type systems are /far/ better.
You are changing topics here.
In a statically typed language, when I write a test case that calls a
specific method, I need to write at least one class that implements at
least that method, otherwise the code won't compile.
In a dynamically typed language I can concentrate on writing the test
cases first and don't need to write dummy code to make some arbitrary
static checker happy.
Are you seriously claiming that concise, *automatically checked*
documentation (which is one function served by explicit type
declarations) is inferior to unchecked, ad hoc commenting?
I am sorry, but in my book, assertions are automatically checked.
But only at runtime, where a logic flaw may or may not trigger the
assertion.
I don't care about that difference. My development environment is
flexible enough to make execution of test suites a breeze. I don't need
a separate compilation and linking stage to make this work.
(Assertions are still useful: if they are active, they prove that the
errors checked by them didn't occur in a given program run. This can
still be useful. But then, production code usually runs with assertion
checking off - which is exactly the point where knowing that some bug
occurred would be more important...)
Don't let your production code run with assertion checking off then.
For one thing, type declarations *cannot* become out-of-date (as
comments can and often do) because a discrepancy between type
declaration and definition will be immidiately flagged by the compiler.
They same holds for assertions as soon as they are run by the test suite.
A test suite can never catch all permutations of data that may occur (on
a modern processor, you can't even check the increment-by-one operation
with that, the universe will end before the CPU has counted even half of
the full range).
I hear that in the worst case scenarios, static type checking in modern
type systems needs exponential time, but for most practical cases this
doesn't matter. Maybe it also doesn't matter for most practical cases
that you can't check all permutations of data in a test suite.
+ Efficiency: As Paul Graham puts it, efficiency comes from
profiling. In order to achieve efficiency, you need to identify the
bottle-necks of your program. No amount of static checks can
identify bottle-necks, you have to actually run the program to
determine them.
I don't think you understand much about language implementation.
....and I don't think you understand much about dynamic compilation.
Have you ever checked some not-so-recent-anymore work about, say, the
HotSpot virtual machine?
Well, I did - and the results were, ahem, unimpressive.
The results that are reported in the papers I have read are very
impressive. Can you give me the references to the papers you have read?
Besides, HotSpot is for Java, which is statically typed, so I don't
really see your point here... unless we're talking about different VMs.
Oh, so you haven't read the literature? And above you said you did.
Well, the research that ultimately lead to the HotSpot Virtual Machine
originated in virtual machines for Smalltalk and for Self. Especially
Self is an "extremely" dynamic language, but they still managed to make
it execute reasonably fast.
When all you wanted to say is that Java is not fast, that's not quite
true. The showstopper for Java is the Swing library. Java itself is very
fast.
In certain cases it's even faster than C++ because the HotSpot VM can
make optimizations that a static compiler cannot make. (For example,
inline virtual methods that are known not to be overridden in currently
loaded classes.)
And, yes, VMs got pretty fast these days (and that actually happened
several years ago).
It's only that compiled languages still have a good speed advantage -
making a VM fast requires just that extra amount of effort which, when
invested into a compiler, will make the compiled code still run faster
than the VM code.
Also, I have seen several cases where VM code just plain sucked
performance-wise until it was carefully hand-optimized. (A concrete
example: the all-new, great graphics subsystem for Squeak that could do
wonders like rendering fonts with all sorts of funky effects, do 3D
transformations on the fly, and whatnot... I left Squeak before those
optimizations became mainstream, but I'm pretty sure that Squeak got
even faster. Yet Squeak is still a bit sluggish... only marginally so,
and certainly no more sluggish than the bloatware that's around and that
commercial programmers are forced to write, but efficiency is simply
more of a concern and a manpower hog than with a compiled language.)
I know sluggish software written in statically typed languages.
There are excellent programs out there that have been written with
static type systems, and there are also excellent programs out there
that have been written without static type systems. This is a clear
indication that static type systems are not a necessary condition for
writing excellent programs.
Hey, there are also excellent programs written in assembly. By your
argument, using a higher language is not a necessary condition for
writing excellent languages.
Right.
The question is: what effort goes into an excellent program? Is static
typing a help or a hindrance?
Right, that's the question.
I'm still unconvinced that an inferring type system is worse than
run-time type checking. (Except for that "dynamic metaprogramming" thing
I'd like to know more about. In my book, things that are overly powerful
are also overly uncontrollable, but that may be an exception.)
Check the literature about metaobject protocols.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Pascal Costanza wrote: Fergus Henderson wrote:
In my experience, people who have difficulties in getting their programs
to typecheck usually have an inconsistent design, not a design which is
consistent but which the type checker is too restrictive to support.
Have you made sure that this is not a circular argument?
It is obviously not a circular argument.
Does "consistent design" mean "acceptable by a type checker" in your book?
Fergus was refering to programs that simply would not work, even if the
compiler ignored the type errors and generated code anyway. Obviously
not all type inconsistent programs fall into this category (only about
99.999..% of them:-). I've been using statically typed FPL's for a
good few years now, and I can only think of one occasion where I had
"good" code rejected by the type checker (and even then the work around
was trivial). All other occasions it was telling me my programs were
broken (and where they were broken), without me having to test it.
This is good thing.
As for dynamics, I don't think anybody would deny the usefulness of a
dynamic type system as a *supplement to* the static type system. (As
you have observed, there are occasions when type checking just can't
be done at compile time). But no way is a dynamic type system an
adequate *substitute for* modern static type systems. Most code
can be (and should be IMO) checked for type errors at compile time.
Regards
--
Adrian Hey
Pascal Costanza <co******@web.de> writes: Joachim Durchholz wrote: Pascal Costanza wrote:
Ralph Becket wrote:
I fail to see how dynamic typing can confer any kind of advantage here.
Read the literature on XP.
Note that most literature contrasts dynamic typing with the static
type systems of C++ and/or Java. Good type systems are /far/ better.
You are changing topics here.
In a statically typed language, when I write a test case that calls a
specific method, I need to write at least one class that implements at
least that method, otherwise the code won't compile.
Not in ocaml.
ocaml is statically typed.
--
Rémi Vanicat
"Andrew Dalke" <ad****@mindspring.com> writes: Pascal Costanza: The set of programs that are useful but cannot be checked by a static
type system is by definition bigger than the set of useful programs that
can be statically checked. So dynamically typed languages allow me to
express more useful programs than statically typed languages.
Ummm, both are infinite and both are countably infinite, so those sets
are the same size. You're falling for Hilbert's Paradox.
They aren't the same size if you limit the length of the program. This
is a reasonable restriction if you are interested in programs that might
be realizable within your lifetime.
Also, while I don't know a proof, I'm pretty sure that type inferencing
can do addition (and theorem proving) so is equal in power to
programming.
Yes, this is true. But it is also the case that a powerful enough
static type checker cannot be proven to halt or produce an answer in a
time less than that required to run the program being checked. It
makes little difference if the type checker produces the answer or the
program produces the answer if they both take about the same time to
run. Of course, it is generally more difficult to program in the type
metalanguage than in the target language.
Remi Vanicat wrote: Pascal Costanza <co******@web.de> writes: In a statically typed language, when I write a test case that calls a
specific method, I need to write at least one class that implements at
least that method, otherwise the code won't compile.
Not in ocaml.
ocaml is statically typed.
How does ocaml make sure that you don't get a message-not-understood
exception at runtime then?
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Nikodemus Siivola <de****@random-state.net> writes: In comp.lang.lisp Matthias Blume <fi**@my.address.elsewhere> wrote:
Apologies for the out-of-context snippage:
A 100,000 line program in an untyped language is useless to me if I am
^^^^^^^
Your choice of word here makes me suspect that you _may_ understand
something quite different than most of the residents of cll and clp by
dynamic typing:
dynamic typing is *not* the same as untyped!
Ah, are we quibbling about *that* again? Words, words, words...
If you want to know how much I know about the difference between typed
and untyped (or "statically typed" vs. "dynamically typed" as you
prefer), look up my track record on implementing languages in either
part of the PL world.
Yes, "dynamically typed" programs are "typed", but the word "type"
here means something quite different from what it means when it is
used with the qualifier "static". I prefer the latter use, and from
that point of view there is only one (static) type in dynamically
typed programs, hence my use of the word "untyped". (If you have only
one (static) type, you might as well not even think about that fact.)
Anyway, unfortunate or not, we are both thinking about the same class
of languages. That shall suffice.
Matthias
PS: When I say "untyped" I mean it as in "the _untyped_ lambda
calculus".
Kenny Tilton <kt*****@nyc.rr.com> writes: The other problem with static typing is that it does not address the
real problem with scaling, viz, the exponential explosion of state
interdependencies. A compiler cannot check the code I neglect to
write, leaving state change unpropagated to dependent other state, nor
can it check the sequence of correctly typed statements to make sure
state used in calculation X is updated before I use that state.
Yes, the usefulness of static types seems to be inversely proportional
to the imperativeness of one's programming style (Haskell, Miranda).
Static types *really* shine in purely functional settings. In mostly
functional settings (SML, OCaml) they lose some of their expressive
"punch" if you start playing with mutable data structures. In
languages that heavily rely on imperative features (mutable state,
object identity, imperative I/O, exceptions) their usefulness goes
increasingly down the drain.
Matthias
Joachim Durchholz <jo***************@web.de> writes: Pascal Costanza wrote: ....because static type systems work by reducing the expressive
power of a language. It can't be any different for a strict static
type system. You can't solve the halting problem in a
general-purpose language.
The final statement is correct, but you don't need to solve the
halting problem: it's enough to allow the specification of some
easy-to-prove properties, without hindering the programmer too much.
In fact, you should never need to "solve the halting problem" in order
to statically check you program. After all, the programmer *already
has a proof* in her mind when she writes the code! All that's needed
(:-) is for her to provide enough hints as to what that proof is so
that the compiler can verify it. (The smiley is there because, as we
are all poinfully aware of, this is much easier said than done.)
Matthias
Pascal Costanza <co******@web.de> writes: Fergus Henderson wrote:
In my experience, people who have difficulties in getting their programs
to typecheck usually have an inconsistent design, not a design which is
consistent but which the type checker is too restrictive to support.
Have you made sure that this is not a circular argument?
Sure. What he says is that the problems with those programs are
usually still there even after you erase types and, thus, arrive at an
untyped program.
Does "consistent design" mean "acceptable by a type checker" in your book?
I cannot speak for Fergus, but I suspect (and hope!) the answer is
"no". By "consistent design" we usually mean design that is free of
certain problems at the time the code executes on a real machine.
Matthias
Adrian Hey wrote: Pascal Costanza wrote:
Fergus Henderson wrote:
I've been using statically typed FPL's for a
good few years now, and I can only think of one occasion where I had
"good" code rejected by the type checker (and even then the work around
was trivial). All other occasions it was telling me my programs were
broken (and where they were broken), without me having to test it.
This is good thing.
Maybe you haven't written the kind of programs yet that a static type
system can't handle.
As for dynamics, I don't think anybody would deny the usefulness of a
dynamic type system as a *supplement to* the static type system.
I don't deny that static type systems can be a useful supplement to a
dynamic type system in certain contexts.
But no way is a dynamic type system an
adequate *substitute for* modern static type systems. Most code
can be (and should be IMO) checked for type errors at compile time.
There is an important class of programs - those that can reason about
themselves and can change themselves at runtime - that cannot be
statically checked.
Your claim implies that such code should not be written, at least not
"most of the time" (whatever that means). Why? Maybe I am missing an
important insight about such programs that you have.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Matthias Blume <fi**@my.address.elsewhere> writes: Yes, the usefulness of static types seems to be inversely proportional
to the imperativeness of one's programming style (Haskell, Miranda).
Static types *really* shine in purely functional settings (****).
[...]
Obviously, the parenthetical remark "(Haskell, Miranda)" should be where
the (****) is.
Matthias
Matthias Blume wrote: PS: When I say "untyped" I mean it as in "the _untyped_ lambda
calculus".
What terms would you use to describe the difference between dynamically
and weakly typed languages, then?
For example, Smalltalk is clearly "more" typed than C is. Describing
both as "untyped" seems a little bit unfair to me.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Pascal Costanza <co******@web.de> writes: Remi Vanicat wrote: Pascal Costanza <co******@web.de> writes:
In a statically typed language, when I write a test case that calls a
specific method, I need to write at least one class that implements at
least that method, otherwise the code won't compile.
Not in ocaml.
ocaml is statically typed.
How does ocaml make sure that you don't get a message-not-understood
exception at runtime then?
It make the verification when you call the test. I explain :
you could define :
let f x = x #foo
which is a function taking an object x and calling its method
foo, even if there is no class having such a method.
When sometime latter you do a :
f bar
then, and only then the compiler verify that the bar object have a foo
method.
By the way, It might give you some headache when you have made a
spelling error to a method name (because the error is not seen by the
compiler where it happen, but latter, where the function using the
wrong method is used).
--
Rémi Vanicat
Pascal Costanza <co******@web.de> writes: Matthias Blume wrote:
PS: When I say "untyped" I mean it as in "the _untyped_ lambda
calculus".
What terms would you use to describe the difference between
dynamically and weakly typed languages, then?
For example, Smalltalk is clearly "more" typed than C is. Describing
both as "untyped" seems a little bit unfair to me.
Safe and unsafe.
BTW, C is typed, Smalltalk is untyped. C's type system just happens
to be unsound (in the sense that, as you observed, well-typed programs
can still be unsafe).
Matthias
Matthias Blume wrote: Pascal Costanza <co******@web.de> writes:
Fergus Henderson wrote:
In my experience, people who have difficulties in getting their programs
to typecheck usually have an inconsistent design, not a design which is
consistent but which the type checker is too restrictive to support.
Have you made sure that this is not a circular argument?
Sure. What he says is that the problems with those programs are
usually still there even after you erase types and, thus, arrive at an
untyped program.
Well, to say this once more, there are programs out there that have a
consistent design, that don't have "problems", and that cannot be
statically checked.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Pascal Costanza <co******@web.de> writes: There are also programs which I cannot express at all in a purely dynamically typed language. (By "program" I mean not only the executable
code itself but also the things that I know about this code.)
Those are the programs which are protected against certain bad things
from happening without having to do dynamic tests to that effect
themselves.
This is a circular argument. You are already suggesting the solution
in your problem description.
Is it? Am I? Is it too much to ask to know that the invariants that
my code relies on will, in fact, hold when it gets to execute?
Actually, if you think that this problem description already contains
the solution which is static typing, then we are basically on the same
page here.
...and BTW, please let me keep up using dynamically typed languages,
because this works well for me!
Since I have no power over what you do, I am forced to grant you this
wish. (Lucky you!)
See the example of downcasts in Java.
You had to dig out the poorest example you could think of, didn't you?
Make a note of it: When I talk about the power of static typing, I am
*not* thinking of Java! To make a (not so far-fetched, btw :) analogy: Consider logical
statements and formal proofs. Making a logical statement is easy and
can be very short. It is also easy to make mistakes without noticing;
after all saying something that is false while still believing it to
be true is extremely easy. Just by looking at the statement it is
also often hard to tell whether the statement is right. In fact,
computers have a hard time with this task, too. Theorem-proving is
hard.
On the other hand, writing down the statement with a formal proof is
impossible to get wrong without anyone noticing because checking the
proof for validity is trivial compared to coming up with it in the
first place. So even though writing the statement with a proof seems
harder, once you have done it and it passes the proof checker you can
rest assured that you got it right. The longer "program" will have fewer
"bugs" on average.
Yes, but then you have a proof that is tailored to the statement you
have made. The claim of people who favor static type systems is that
static type systems are _generally_ helpful.
I am not sure you "got" it: Yes, the proof is tailored to the
statement (how else could it be?!), but the axioms and rules of its
underlying proof system are not. Just like not every program has the
same type even though the type system is fixed.
Matthias
Pascal Costanza <co******@web.de> writes: Well, to say this once more, there are programs out there that have a
consistent design, that don't have "problems", and that cannot be
statically checked.
Care to give an example? How you you know that the design is
consistent? Do you have a proof for that claim? Can you write that
proof down for me, please?
:-)
Matthias
Matthias Blume wrote: Pascal Costanza <co******@web.de> writes:
Matthias Blume wrote:
PS: When I say "untyped" I mean it as in "the _untyped_ lambda
calculus".
What terms would you use to describe the difference between
dynamically and weakly typed languages, then?
For example, Smalltalk is clearly "more" typed than C is. Describing
both as "untyped" seems a little bit unfair to me.
Safe and unsafe.
BTW, C is typed, Smalltalk is untyped. C's type system just happens
to be unsound (in the sense that, as you observed, well-typed programs
can still be unsafe).
Can you give me a reference to a paper, or some other literature, that
defines the terminology that you use?
I have tried to find a consistent set of terms for this topic, and have
only found the paper "Type Systems" by Luca Cardelli
( http://www.luca.demon.co.uk/Bibliography.htm#Type systems )
He uses the terms of static vs. dynamic typing and strong vs. weak
typing, and these are described as orthogonal classifications. I find
this terminology very clear, consistent and useful. But I am open to a
different terminology.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Remi Vanicat wrote: Pascal Costanza <co******@web.de> writes:
Remi Vanicat wrote:
Pascal Costanza <co******@web.de> writes:
In a statically typed language, when I write a test case that calls a
specific method, I need to write at least one class that implements at
least that method, otherwise the code won't compile.
Not in ocaml.
ocaml is statically typed.
How does ocaml make sure that you don't get a message-not-understood
exception at runtime then?
It make the verification when you call the test. I explain :
you could define :
let f x = x #foo
which is a function taking an object x and calling its method
foo, even if there is no class having such a method.
When sometime latter you do a :
f bar
then, and only then the compiler verify that the bar object have a foo
method.
Doesn't this mean that the occurence of such compile-time errors is only
delayed, in the sense that when the test suite grows the compiler starts
to issue type errors?
Anyway, that's an interesting case that I haven't known about before.
Thanks.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Pascal Costanza wrote: Joachim Durchholz wrote:
Pascal Costanza wrote:
For example, static type systems are incompatible with dynamic
metaprogramming. This is objectively a reduction of expressive power,
because programs that don't allow for dynamic metaprogramming can't
be extended in certain ways at runtime, by definition.
What is dynamic metaprogramming?
Writing programs that inspect and change themselves at runtime.
Ah. I used to do that in assembler. I always felt like I was aiming a
shotgun between my toes.
When did self-modifying code get rehabilitated?
- ken
On Thu, 23 Oct 2003, Remi Vanicat wrote: How does ocaml make sure that you don't get a message-not-understood
exception at runtime then?
It make the verification when you call the test. I explain :
you could define :
let f x = x #foo
which is a function taking an object x and calling its method
foo, even if there is no class having such a method.
When sometime latter you do a :
f bar
then, and only then the compiler verify that the bar object have a foo
method.
you might want to mention that this is possible because of 'extensible
record types'. Well, there is a good chance the pyhton/lisp community will
not understand this, but it illustrates that a lot of the arguments
(probably on both sides in fact) are based on ignorance.
One more thing I remembered from a heavy cross-group fight between
comp.lang.smalltalk and c.l.f. quite a while ago, is that so-called
'dynamically typed' languages are useful because they allow you to
incrementally develop ill-typed programs into better-typed programs (the
XP-way), where the ill-typed programs already (partially) work. OTOH, with
a static type system, you have to think more in advance to get the types
right. XP-people consider this a hindrance and that is what people mean
with 'the type system getting the way'. With a Haskell-style or even
Ocaml-style type system, you cannot seriously argue that you can write a
program which cannot be easily(!) converted into one that fits such type
systems. By program, I mean 'a finished production-reade piece of
software', not a 'snapshot' in the development cycle.
The arguments from the smalltalk people are arguably defendable and this
is why this kind of discussion will pop up again and again. Using either
static or dynamic (Blume: untyped) type systems is not the point at all.
What actually matters is your development style/phylosophy and this is
more an issue of software engineering really.
Ok, I am phasing out again.
Regards,
Simon
Matthias Blume wrote: Pascal Costanza <co******@web.de> writes:
There are also programs which I cannot express at all in a purelydynamically typed language. (By "program" I mean not only the executable
code itself but also the things that I know about this code.)
Those are the programs which are protected against certain bad things
from happening without having to do dynamic tests to that effect
themselves.
This is a circular argument. You are already suggesting the solution
in your problem description.
Is it? Am I? Is it too much to ask to know that the invariants that
my code relies on will, in fact, hold when it gets to execute?
Yes, because the need might arise to change the invariants at runtime,
and you might not want to stop the program and restart it in order just
to change it.
Actually, if you think that this problem description already contains
the solution which is static typing, then we are basically on the same
page here.
...and BTW, please let me keep up using dynamically typed languages,
because this works well for me!
Since I have no power over what you do, I am forced to grant you this
wish. (Lucky you!)
:-) See the example of downcasts in Java.
You had to dig out the poorest example you could think of, didn't you?
Make a note of it: When I talk about the power of static typing, I am
*not* thinking of Java!
OK, sorry, this was my mistake. I have picked this example because it
has been mentioned in another branch of this thread. To make a (not so far-fetched, btw :) analogy: Consider logical
statements and formal proofs. Making a logical statement is easy and
can be very short. It is also easy to make mistakes without noticing;
after all saying something that is false while still believing it to
be true is extremely easy. Just by looking at the statement it is
also often hard to tell whether the statement is right. In fact,
computers have a hard time with this task, too. Theorem-proving is
hard.
On the other hand, writing down the statement with a formal proof is
impossible to get wrong without anyone noticing because checking the
proof for validity is trivial compared to coming up with it in the
first place. So even though writing the statement with a proof seems
harder, once you have done it and it passes the proof checker you can
rest assured that you got it right. The longer "program" will have fewer
"bugs" on average.
Yes, but then you have a proof that is tailored to the statement you
have made. The claim of people who favor static type systems is that
static type systems are _generally_ helpful.
I am not sure you "got" it: Yes, the proof is tailored to the
statement (how else could it be?!), but the axioms and rules of its
underlying proof system are not. Just like not every program has the
same type even though the type system is fixed.
Yes, but you have much more freedom when you write an arbitrary proof
than when you need to make a type system happy.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Matthias Blume wrote: Pascal Costanza <co******@web.de> writes:
Well, to say this once more, there are programs out there that have a
consistent design, that don't have "problems", and that cannot be
statically checked.
Care to give an example? How you you know that the design is
consistent?
Squeak, probably. Lisp development environments. Probably almost any
development environment with a good debugger that allows for changing
code on the fly.
Do you have a proof for that claim? Can you write that
proof down for me, please?
No. Design consistency is an aesthetical category.
:-)
Matthias
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Ken Rose wrote: Pascal Costanza wrote:
Joachim Durchholz wrote:
Pascal Costanza wrote:
For example, static type systems are incompatible with dynamic
metaprogramming. This is objectively a reduction of expressive
power, because programs that don't allow for dynamic metaprogramming
can't be extended in certain ways at runtime, by definition.
What is dynamic metaprogramming?
Writing programs that inspect and change themselves at runtime.
Ah. I used to do that in assembler. I always felt like I was aiming a
shotgun between my toes.
When did self-modifying code get rehabilitated?
I think this was in the late 70's.
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Simon Helsen wrote: On Thu, 23 Oct 2003, Remi Vanicat wrote:
How does ocaml make sure that you don't get a message-not-understood
exception at runtime then?
It make the verification when you call the test. I explain :
you could define :
let f x = x #foo
which is a function taking an object x and calling its method
foo, even if there is no class having such a method.
When sometime latter you do a :
f bar
then, and only then the compiler verify that the bar object have a foo
method.
you might want to mention that this is possible because of 'extensible
record types'. Well, there is a good chance the pyhton/lisp community will
not understand this, but it illustrates that a lot of the arguments
(probably on both sides in fact) are based on ignorance.
Do you have a reference for extensible record types. Google comes up,
among other things, with Modula-3, and I am pretty sure that's not what
you mean.
One more thing I remembered from a heavy cross-group fight between
comp.lang.smalltalk and c.l.f. quite a while ago, is that so-called
'dynamically typed' languages are useful because they allow you to
incrementally develop ill-typed programs into better-typed programs (the
XP-way), where the ill-typed programs already (partially) work.
Sometimes the ill-typed program is all I need because it helps me to
solve a problem that is covered by that program nonetheless.
OTOH, with
a static type system, you have to think more in advance to get the types
right. XP-people consider this a hindrance and that is what people mean
with 'the type system getting the way'. With a Haskell-style or even
Ocaml-style type system, you cannot seriously argue that you can write a
program which cannot be easily(!) converted into one that fits such type
systems. By program, I mean 'a finished production-reade piece of
software', not a 'snapshot' in the development cycle.
The arguments from the smalltalk people are arguably defendable and this
is why this kind of discussion will pop up again and again. Using either
static or dynamic (Blume: untyped) type systems is not the point at all.
What actually matters is your development style/phylosophy and this is
more an issue of software engineering really.
Exactly. Very well put!
Thanks,
Pascal
--
Pascal Costanza University of Bonn
mailto:co******@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Pascal Costanza wrote:
But only at runtime, where a logic flaw may or may not trigger the
assertion.
I don't care about that difference. My development environment is
flexible enough to make execution of test suites a breeze. I don't need
a separate compilation and linking stage to make this work.
(Assertions are still useful: if they are active, they prove that the
errors checked by them didn't occur in a given program run. This can
still be useful. But then, production code usually runs with assertion
checking off - which is exactly the point where knowing that some bug
occurred would be more important...)
Don't let your production code run with assertion checking off then.
You don't seem to see the fundamental difference, which has been stated
as "Static typing shows the absence of [certain classes of] errors,
while testing [with assertions] can only show the presence of errors."
When you actively use a type system as a tool and turn it to your
advantage that "certain class" can be pretty large, btw.
I hear that in the worst case scenarios, static type checking in modern
type systems needs exponential time, but for most practical cases this
doesn't matter. Maybe it also doesn't matter for most practical cases
that you can't check all permutations of data in a test suite.
Come on, you're comparing apples and wieners. The implications are
completely different.
--
Andreas Rossberg, ro******@ps.uni-sb.de
"Computer games don't affect kids; I mean if Pac Man affected us
as kids, we would all be running around in darkened rooms, munching
magic pills, and listening to repetitive electronic music."
- Kristian Wilson, Nintendo Inc. This thread has been closed and replies have been disabled. Please start a new discussion. Similar topics
by: Xah Lee |
last post by:
http://python.org/doc/2.4.1/lib/module-re.html
http://python.org/doc/2.4.1/lib/node114.html
---------
QUOTE
The module defines several...
|
by: Juha S. |
last post by:
Hi,
I'm writing a small text editor type application with Python 2.5 and
Tkinter. I'm using the Tk text widget for input and output, and the...
|
by: Berco Beute |
last post by:
I wonder what it would take to implement Python in JavaScript so it
can run on those fancy new JavaScript VM's such as Chrome's V8 or
Firefox'...
|
by: Luke Kenneth Casson Leighton |
last post by:
On Sep 3, 10:02 pm, bearophileH...@lycos.com wrote:
1200 lines of code for the compiler, and about... 800 for a basic
suite of builtin types...
|
by: Kemmylinns12 |
last post by:
Blockchain technology has emerged as a transformative force in the business world, offering unprecedented opportunities for innovation and...
|
by: Naresh1 |
last post by:
What is WebLogic Admin Training?
WebLogic Admin Training is a specialized program designed to equip individuals with the skills and knowledge...
|
by: jalbright99669 |
last post by:
Am having a bit of a time with URL Rewrite. I need to incorporate http to https redirect with a reverse proxy. I have the URL Rewrite rules made...
|
by: Matthew3360 |
last post by:
Hi there. I have been struggling to find out how to use a variable as my location in my header redirect function.
Here is my code.
...
|
by: Arjunsri |
last post by:
I have a Redshift database that I need to use as an import data source. I have configured the DSN connection using the server, port, database, and...
|
by: WisdomUfot |
last post by:
It's an interesting question you've got about how Gmail hides the HTTP referrer when a link in an email is clicked. While I don't have the specific...
|
by: Oralloy |
last post by:
Hello Folks,
I am trying to hook up a CPU which I designed using SystemC to I/O pins on an FPGA.
My problem (spelled failure) is with the...
|
by: Carina712 |
last post by:
Setting background colors for Excel documents can help to improve the visual appeal of the document and make it easier to read and understand....
|
by: BLUEPANDA |
last post by:
At BluePanda Dev, we're passionate about building high-quality software and sharing our knowledge with the community. That's why we've created a SaaS...
| |
