Lambda the Ultimate

My experience with other dynamic languages coincides with these claims for Python. Are there numbers available that suggest debunking is in order, or is the request for debunking just a subjective feeling at this point?

Good, disciplined programmers can produce good disciplined code and perhaps don't need strict type checks, const guarantees, enforced encapsulation, etc. However, I've rarely seen a project run that way; every large chunk of Python code I've seen, including Zope, contains quite a few fragilities and inconsistencies that I found quite disturbing.

In general, having used Python since 1996, I've noticed that many Python programmers tend to:

a) Overuse dictionaries in general & use dictionaries where dispatch on an object is preferable.

b) Be sloppy with variable scoping and abuse of object encapsulation -- use of many module-level globals, direct access and mutation of data members on objects, etc.

Python has solutions that a disciplined team can use to remedy both of these, but I don't always see many people using them. I'd like to see something like Python with much stricter default module and class level encapsulation rules, compile-time const variable and function checks, and perhaps even optional run-time type constraints / checks. Perhaps as a dialect of Python ("strict Python?")?

Sometimes this is really useful, but often I wish I could specify what introspective features a module will actually /use/, so the compiler can make some more assumptions about what might be correct code and what might not, to save me from finding all these errors at run time (or not).

b. All the empirical research I am aware of regarding programmer productivity tends to show that typing time (I mean keyboard typing, not type checking ) is not an important factor, when talking about large software products. If anyone can point to a reserach showing otherwise, let me know.

Notice that I am not saying that Python doesn't enhance productivity. I think it is a very useful languages (as I have said here repeatedly). But aside from quick and dirty scripting, the reason isn't merely that you need to type less.

By the way, my guess is that Guido was trolling himself

With over 20 years of programming spent, roughly, equally between dynamic and static languages, I have never seen any language feature of any language supplant discipline. I'm not buying this argument.

The only real key to success I have ever seen or practiced is discipline.

Guido van Rossum: Weak typing probably helps you feel productive, because it lets you bend the rules a bit when deciding what goes into your array. You can have an array of numbers that occasionally has something else inside, if that doesn't bother you.

I'm having trouble imagining why I would occasionally want to throw a string into my array of integers.

If I really do want to do this, I'm quite happy to declare a type of:

type Message of String | Number of int

And have the compiler check to make sure I'm always adding integers and concatinating strings and not vice versa.

Thoughts?

Mixing types in collections occurs more often with complex types. Languages like CLOS and Smalltalk support this dynamically, e.g. this is Smalltalk:

  aCollection collect: 
      [ :account | account movingAverage: 14 ]

This results in a collection of moving averages over the last 14 days for all the accounts in the original collection. Any object can be in the collection as long as it knows how to respond to the #movingAverage: selector.

type Message of String | Number of int

Dynamic languages have been easier to change in the past because the amount of effort required to (1) prototype the proposed change, and then (2) implement the change throughout the system, once it is accepted.

What could change this equation is the use of implicitly typed languages like Haskell, etc. I have used Haskell in small learning situations, so I personally do not have enough evidence.

I would really like to see some empirical evidence on agile approaches to building large systems with implicitly typed languages. But doing useful empirical studies like this are challenging to say the least.

On the other hand, as far as I know, in ocaml you can have a collection of diverse objects that share some method signatures, and get the static typing too, implicitly. This is what you were getting at in your second post.

This seems to be the best of both worlds. I can quickly update my variable types, and the compiler helps me by flagging the spots where I really do need to make changes.

I think J closes the lid on the fewer lines of code angle. I love the language, but it makes my head hurt to write anything non-trivial in it.

The only real key to success I have ever seen or practiced is discipline.

I absolutely agree, and I didn't say that strong typing was any kind of guarantee of success. In fact, in languages where type and class are unified, I really think that the typing just obstructs object oriented polymorphism in a way that can lead to even more errors.

I just think Python's default lack of any kind of real encapsulation rules on objects and modules leads to code which works fine when seen in a "scripting" light, but doesn't scale that well. People end up creating objects which are really nothing more than records or tables and often write code which mutates the innards of other objects at will. IMHO in a heavily threaded (or any application with complex flow of control) this is just a recipe for disaster.

Programming is about automation. I try to find ways to let my computer do my work for me. If I can factor my design work so that my computer can check some of its consistency for me, then I will do it.

I agree. The question I have is this: does the present state-of-the-art in type systems make a programmer with my skills more productive than the present state-of-the-art in dynamic languages?

The answer is not clear to me, and I am looking for empirical evidence one way or the other.

...maybe you should look for a more structured discipline, which lets you focus on the work which your computer cannot do for you.

Exactly. Type systems do not seem to help my productivity nearly as much as does a personal discipline that helps me write more dynamic systems.

Maybe this is true in the simplest of implementations, but then the cost would hardly be noticed compared to the cost of a simple implementation of everything else.

Certainly the cost of call/cc is not paid by every program in implementations like Chez Scheme, PLT Scheme, Gambit Scheme, MIT Scheme, etc. I doubt even a good Java implementation of Scheme like SISC pays such a price.

Is there evidence to the contrary? Scheme implementors have been handling call/cc just fine for well over a decade in the implementations I've been using. Read the literature, try the implementations, benchmark real scenarios, but please don't spread these claims without real evidence.

Lack of keyboard typing: 1) Python also supplies sufficient syntatic sugar like true, [], for ... in, zip, which make working in Python far less verbose than in a language Java. 2) Minor factor - Most function names are in lower case, and there is very little line noise like characters. which require the "shift" keystroke.

Chui: See the Nice Programming Language for an example of how all that suffering can be eliminated without giving up type safety. Actually, like most strongly type modern functional or object/functional languages (Haskell, ML, Neel's language Needle, etc.), you get more type safety than with Java - no casting required. Personally I favor languages with clutter-free syntax like Python and Haskell, but Nice is a very good blend of mainstream Java and modern type systems. It would be better with type inference, I understand that's coming...

Just like structured programming means you can't use goto where you might like to, type checked programs limit you, but in a way that's generally seen to help more than hurt.

That's a straw man argument. Dynamic languages like Python, Smalltalk, and Scheme are hardly assembly languages. The discipline these languages require is not significantly different from the discipline of more static languages, i.e. you still need to write the same tests and you still need to refactor code as it grows.

Higher levels of abstraction are ways of enforcing the discipline of doing things certain ways...

I agree. Languages like Smalltalk and Scheme, and to a lesser degree Python, are higher order than languages like Java. They are just as expressive, and arguably more so, than languages like Haskell.

...type checked programs limit you, but in a way that's generally seen to help more than hurt.

That's the crux of this thread of discussion. Some people say yes, others say no. I'm not sure where the majority is. I know there isn't much empirical evidence one way or the other.

I agree it would be no use if this were true. But since sane programmers do use it, Scheme has it. It may not be well known. It is certainly not used every day in end-user applications, but that is as undesirable as using macros every day in end-user applications. (Many people don't get the point of extending syntax either.)

But it is used by sane programmers who do things like implement language constructs and "little languages". And so in this way, call/cc does become widely used (to the extent that Scheme and Ruby are widely used).

With a proper implementation strategy, the expense can be pushed down as low as a 5% overhead (which is why I think that it's a worthwhile feature), but it will affects all programs.

I don't know if it is 1% or 5%. I have a feeling it is not 10%. In any case, it is not controversial because of the performance hit. It certainly does not affect all programs to the extent that there is a good argument for throwing it out of the language.

Certainly it is not widely understood. In general that is because most teachers could not provide a good presentation of it. In general that is because their teachers could not...

Face it, to the extent call/cc is controversial, it is because computer science educators don't know Landin's J operator from a hole in the ground.

I love python, but I must say that as a program gets larger and larger I find dynamic typing starts to lose. Type inference takes away a lot of the pain of static typing (which isn't that painful to begin with), but most statically typed languages (even ocaml) have too restricted type systems for my taste. I'm quite curious about Nice and Needle, and hope to see more languages exploring multimethods in the context of statically typed languages.

Another point that Neel brings up is the stack-copying associated with multiply-invoked continuations. Apparently, this was such a nuisance that at least one of the parallel Schemes implemented different constructs for making singly and multiply invoked continuations.

There are some really good papers on this type of stuff in the proceedings from the 1989 US/Japan Workshop on Parallel Lisp (published as volume 441 of Lecture Notes in Computer Science by Springer-Verlag).

In my experience as all applications get larger they start to lose, whatever the language. This is where diligence and experience kick in. Diligence in the form of complete tests and ruthless refactoring is the only way to win in the end.

I don't know Python well, but I've implemented large Smalltalk and Lisp applications with good and not-as-good teams. In each case it was the team that made the difference. This includes distributed systems with hundreds of concurrent users, thousands of classes, and millions of objects.

Large Python programs should probably driven by a good test framework and a devotion to test-driven development. I know of no other way.

More recent work suggests otherwise. See Threads Yield Continuations.

If discipline was all it took, we'd all program in assembly.

That's a straw man argument. Dynamic languages like Python, Smalltalk, and Scheme are hardly assembly languages.

I think Adrian has a point.

The two important differences between a conventional dynamically typed language and assembly languages are that a) the former have a more reasonable syntax, and b) they come equipped with a large standard library of routines (including not only file I/O and standard datatypes, but also heap management and stuff which assembly hasn't got). For a second I thought error-trapping was also a difference, but you can have that in an assembly language implementation which interprets (emulates) rather than compiles to machine code.

Assembly language is indeed the first dynamically typed language.

The discipline these languages require is not significantly different from the discipline of more static languages, i.e. you still need to write the same tests and you still need to refactor code as it grows.

Granted, no static type system is ever going to be "perfect" (because of Goedel). But that doesn't mean we should throw the baby out with the bathwater: having some static guarantees is better than none. Programs written in DT languages also satisfy static guarantees (that's what a specification is, after all), but they are not generally effectively inferrible from the source code.

I do think statically typed languages require a different sort of discipline from dynamically typed ones. With an ST language, every user has to agree on a certain set of rules which every program has to satisfy, namely the typing rules, and that certainly affects the way in which you have to design your programs. Static typing thus rules out some designs, but in my experience a good type system only rules out designs which are unmaintainable in the long run. If you have a very short program or a one-shot program, then sometimes it can get in the way. But even then, the problem disappears if you have a combinator-style library available.

DT language programmers feel that they cannot abide by a set of ground rules for program design, hence they reject static typing. Personally, I think that DT programmers tend to vastly overestimate their own originality and insight.

Almost every time I've cursed Haskell's static typing (except for type classes, which have lots of problems) because it got in my way, I found that the redesigned program which obeys static typing has advantages over the old one; if I do enough work, they can even be as flexible. My "clever" solutions always have lurking problems. When I want default arguments, overloading, multiple arities for the same function, whatever, I try to figure out why, and I almost always find some additional structure in the problem which I can axiomatize and factor out. This happens so often that for the cases where I haven't figured it out, I now believe that I have just missed some key insight and that there is a more elegant solution waiting somewhere, though perhaps with a better type system I would find an even more elegant solution.

After studying category and proof theory, I sort of discovered why this was true. It's because typing (in the presence of general recursion) does not limit what you can model; instead, it limits how shallowly you can model it, and what set of primitives (by analogy, "coordinate basis" or "axioms") you can use to express the problem. In other words, typing forces you to look more carefully at the problem you're trying to solve, and it forces you to use a particular language to express it in.

The difference in disciplines is thus that you have to be a) willing to explore the problem to a certain depth, and b) willing to accept the style of design which is implied by your choice of primitives.

There is an escape route for a): if you don't want to explore the problem too deeply, you can emulate a DT language by injecting everything into a universal datatype and doing dynamic checks explicitly. This is a chore, but always possible. If you aren't willing to explore the problem, it's the price you pay; people that aren't willing to model the problem deeply enough, are the ones who end up saying ST languages are a long-winded pain in the ass and find DT languages more convenient. Indeed, for their style of programming they probably are more convenient.

I think b), OTOH, is not as big a deal. Every programmer subscribes to some design methodology: get/set() methods, hiding representations, naming conventions, etc. People call this "good programming practice" and many are universally accepted. Others aren't universally accepted, indeed are mutually exclusive. But the important thing is to follow a coherent set of rules which reinforce each other. So, even when you see a shortcut solution which breaks a rule, you try to follow it anyway because you know that the rule serves a larger purpose. This holds for programming in both DT and ST languages.

Typing rules are also a set of rules which encourage "good programming practice". Type systems differ on what is good programming practice, and sometimes there is a shortcut solution in one that is disallowed by the other, and vice versa. But the important thing is that the rules in the system are coherent and reinforce each other. If you can agree on good programming practice, then you can agree on a set of typing rules.

Mind you, I don't think these arguments hold for every static type system, only good ones. For example, Java's (and most OO languages') type system is "lossy" somehow; without casts in most interesting programs, if you run them long enough, every object reverts to the most general Object type. This lossiness is, I think, an indication that Java's type system is "incomplete" somehow. Also, Java's type system seems full of redundancies and inconsistencies, with multiple ways of expressing things that don't reduce to each other, and that makes it difficult to think about the problem in terms of types.

I understand this is your belief. I understand some people agree with you. Please understand this is not my belief and that some people agree with me.

Moreover, please understand that I have yet to see a convincing formal, even semi-formal, argument that would suggest universal agreement is anywhere in the near future.

Programs written in DT languages also satisfy static guarantees (that's what a specification is, after all), but they are not generally effectively inferrible from the source code.

For most languages and applications, dynamic specifications (i.e. unit and functional tests) guarantee far more about desired behavior than static specifications.

Increasingly this is not true. Newer type systems express far more dynamic guarantees than ever before. Also other kinds of checks like concurrent state machine analyzers are very practical in many cases.

DT language programmers feel that they cannot abide by a set of ground rules for program design, hence they reject static typing.

Thank you for speaking so eloquently on behalf of all us dynamic language programmers! Just one problem: your claim is false.

Personally, I think that DT programmers tend to vastly overestimate their own originality and insight.

Let's stick to the facts, please.

Almost every time I've cursed Haskell's static typing (except for type classes, which have lots of problems) because it got in my way, I found that the redesigned program which obeys static typing has advantages over the old one; if I do enough work, they can even be as flexible. My "clever" solutions always have lurking problems.

Fortunately dynamic languages do not require cleverness. I am not so clever myself.

When I want default arguments, overloading, multiple arities for the same function, whatever, I try to figure out why, and I almost always find some additional structure in the problem which I can axiomatize and factor out.

Me too. I am not a fan of these either. I try to keep things as simple as possible.

In other words, typing forces you to look more carefully at the problem you're trying to solve, and it forces you to use a particular language to express it in.

Same for a good dynamic test-driven approach. I think there are similarities that will come out of current and future research.

...people that aren't willing to model the problem deeply enough, are the ones who end up saying ST languages are a long-winded pain in the ass and find DT languages more convenient. Indeed, for their style of programming they probably are more convenient.

Could you please include just one more ad hominem attack in your argument? I'm almost convinced of your point. 8^)

Sheesh.

Mind you, I don't think these arguments hold for every static type system, only good ones.

I agree these newer type systems are very good. Almost as good as a simple dynamic language like Smalltalk or Scheme and a rigorous test-driven development approach.

Almost. Not quite yet, for my money.

I try to avoid religious wars here on LtU, as I am sure both Frank and Patrick know. I am sure you guys know exactly why I try to avoid these at all costs.

Reading both your posts, I see you have quite a lot to say on the subject, even without getting into these ad hominem fights...

Java's type system seems full of redundancies and inconsistencies, with multiple ways of expressing things that don't reduce to each other, and that makes it difficult to think about the problem in terms of types.

I've had to learn java in more detail recently, and I'm appalled by how ad-hoc and inconsistent the language is, with dozens of special cases covering almost every conceivable facet of the language. I really like the language libraries and environment, but I can't believe that the designers couldn't come up with a more consistent design. Complex language designs always lose for me because I don't want to have to keep a huge rulebook in my head. Even python is getting too complex for my tastes.

I tend to agree with this sentiment. However, there are cases (Scheme?) where the language is smaller and consistent, but anything substantial requires libraries, which must have their own documentation, and rulebook.

So you have to consider the tradeoffs.

(Note that Java also has huge libraries, so this isn't a defense of Java, or something like that, God forbid)

I've been thinking a lot about this lately. I tend to regard scheme as a canonical example of a language with very few bogosities, although it's an unfair comparison because pure R5RS scheme has so much missing functionality (threads, objects, exceptions, modules...) that you can't directly compare it with (say) java. PLT scheme is a better comparison, because it has all those features. Interestingly, the PLT object system is implemented as a library (about 2K LOC!). It uses macros extensively, so as you say you have to learn the new rulebook (represented by the syntactic extensions instantiated by the macros) when you learn the libraries. Libraries that don't include macros are much more straightforward to learn (just learn a bunch of new procedures, not a new way of doing things). It's only when the library can extend the language in a more fundamental way (= macros) that the rulebook gets significantly more complex.

I don't know if the scheme approach is better, but having to write out macros explicitly at least makes the rulebook explicit, as well as allowing evolution. If my object system is excessively complex and bogus, you can write your own. The counterargument is that the rulebook isn't fixed, so that reading someone else's code becomes that much harder. This is why some scheme/lisp advocates argue for macros being used sparingly.

Even with the Python development team's committment to simplicity and "there should be one obvious way to do it" we're still seeing an increase in redundancy. For example we now have iterators, generators, list comprehensions, map, for loops and in 2.3 the enumerate built-in function providing different ways to go through a sequence. They're not all equivalent but there's enough overlap that one ends up maintaining a mental rulebook if one wants consistent code.

Or consider a language like Perl6 where which seems to have even more complexity than Perl5 before it's finished. Looking at the roadmaps for langauges like C# and Java I see promises of even more redundant ways to do the same thing (iterators on top of enumerators and the foreach loop respectively) and nothing about simplifying/refactoring what's already there.

Are there any languages that have been able to stave off entropy and still remain useful?

I am tempted to hazard a conjecture that languages must become complex in order to be made robust to their environment (both programming and execution). At the moment, I cannot think of an engineered system or evolved organism which is both simple and robust (but I would be happy for someone to bring one to my attention), and at the moment, I am not sure why computer languages would be different.

• Law of continuing change: a system needs to change in order to be useful
• Law of increasing complexity: the structure of a system detoriates as it evolves.

A unified theory of software evolution

Professor Lehman's homepage

DT language programmers feel that they cannot abide by a set of ground rules for program design, hence they reject static typing.

Thank you for speaking so eloquently on behalf of all us dynamic language programmers! Just one problem: your claim is false.

Oh? What is your position then?

I should have written:

DT language programmers feel that they cannot abide by a set of decidable ground rules for program design, hence they reject static typing.

but aside from that I don't see where my claim is anything but a restatement of the DT philosophy.

Personally, I think that DT programmers tend to vastly overestimate their own originality and insight.

Let's stick to the facts, please.

I'm sorry about the tone of that remark.

But what I'm trying to say is that the extra freedom which a DT language gives over an ST language is frequently either a) not exploited, b) exploited in a way which leads to programs with worse designs.

Fortunately dynamic languages do not require cleverness. I am not so clever myself.

I think you're wrong there. DT languages have more degrees of freedom, hence the solution space is larger and more difficult to search. There is inherently more wheel-reinventing going on in a DT language because if the programmers of a DT language could get together and agree on a set of (decidable) ground rules for design, then it would be an ST language.

The place where a DT language can theoretically beat an ST language is in reuse, because static typing inherently limits it. But in practice I don't see this exploited in DT programs. Instead, DT programs often seem to end up being less reusable because the specifications of programs a) are more complex than those of ST programs because there is no bound on their complexity, and b) are never stated explicitly, so there is confusion on the client side.

In other words, typing forces you to look more carefully at the problem you're trying to solve, and it forces you to use a particular language to express it in.

Same for a good dynamic test-driven approach. I think there are similarities that will come out of current and future research.

Tests are necessary for ST programs as well. The difference is that DT programs require a lot more tests to achieve the same level of confidence because because they don't catch trivial errors which could be caught by static checks.

...people that aren't willing to model the problem deeply enough, are the ones who end up saying ST languages are a long-winded pain in the ass and find DT languages more convenient. Indeed, for their style of programming they probably are more convenient.

Could you please include just one more ad hominem attack in your argument? I'm almost convinced of your point. 8^)

What I wrote was by no means an ad hominem argument but I apologize if you read it that way.

Indeed, I was trying to empathize with DT programmers. What I see often in students and programmers who struggle with ST languages is frustration because "the goddamn type checker won't let my perfectly good program through" or "I'm sick of all this pointless extra information I have to give to appease the type checker". But 95% of the time they are complaining because of some problem which a DT language would allow them to commit and force them to either a) spend much longer hunting down afterward during debugging, or b) spend even longer redesigning their program afterward. The problem is that, though some people see a) happening, very few ever trace b) back to the presence of static type checking, and I think that is part of the reason ST is undervalued.

As for my remark that DT languages are more convenient for certain people's style of programming, I was basically saying that they are fighting the type checker rather than living in harmony with it.

To make an analogy, they are like guitar players who never learned to use all the fingers on their left hand, so end up finding it impossible to play difficult pieces because they can't move their fingers quickly enough along the fretboard: they think that speed is the problem, but in reality the problem is their finger placement. (A good guitar player's left hand moves very little.)

I agree these newer type systems are very good. Almost as good as a simple dynamic language like Smalltalk or Scheme and a rigorous test-driven development approach. [Emphasis mine.]

I believe very strongly that what you take for simplicity is an illusion because you see only half of the equation. Those languages are simpler only because they model less of the problem. The programmer is the one who ends up having to compensate but, as I said above, I think few people recognize it. They end up diagnosing the symptoms rather than the disease.

BTW, sorry again for my tone. It was not my intent to belittle DT programmers, but I do believe that the ST vs. DT question is not just a question of taste or subject to relativism; ST languages really are superior software development tools. I'm well aware "that this is not [your] belief and that some people agree with [you]" and indeed I have a lot of respect for some DT advocates like, for example, Felleisen and Krishnamurthi. I also think that a well-designed DT language like Scheme is arguably appropriate for teaching beginning programmers precisely because it addresses a smaller part of the problem (writing correct, efficient programs), and we shouldn't drop the entire problem into students' laps at once. But for advanced and intermediate programming tasks, ST is simply a better tool.

Frank, I'm (somewhat) familiar with category theory, but I don't know what you mean by proof theory. Any good links or books you can recommend?

Proof theory is to logic like set theory is to number theory, or like category theory is to set theory. It studies the formal structure of proofs of propositions rather than the propositions themselves. The most important concept is that of cut elimination or proof reduction, which is an algorithm which recursively transforms an arbitrary proof with its normal form. If you view a logic as a type system and a proof as a program, then proof theory studies the structure of programs. If the logic is intuitionistic logic, then the proofs are typed lambda-terms and cut elimination is evaluation. (This is called the Curry-Howard(-Tait-Feys-de Bruijn...) correspondence.)

The best introductory book is:

Jean-Yves Girard, Yves Lafont and Paul Taylor. Proofs and Types. Cambridge University Press, 1989.

Also see:

Jean H. Gallier. Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi.

———. Constructive Logics. Part II: Linear Logic and Proof Nets.

Helmut Schwichtenberg. Proof Theory.

on my PLT page.

This is the difference between theory and practice. In theory you want to model as much as possible statically. In practice you might not.

Tests are necessary for ST programs as well. The difference is that DT programs require a lot more tests to achieve the same level of confidence...

I am awaiting for publication of the evidence behind this claim. I know this is not true for the older type systems of Java-like languages. If this claim is true for newer type systems like those of modern functional languages, can you point me to substantive descriptions of the studies which back this up?

I have written academic programs in Haskell, but nothing I would classify as significant industrial-strength applications. I think these languages have a lot of potential, but I am unaware of significant studies like this. I am looking forward to such evidence.

I definitely see your point wrt static type systems, and in general I prefer them to dynamic typing as well. HOWEVER, I fear situations where the static type system is too rigid to express some perfectly reasonable designs. This has happened to me in ocaml, for instance, because ocaml's object system doesn't allow downcasting (a deliberate design decision, BTW). This sort of problem doesn't happen in DT languages, and rarely happens in ST languages with "loopholes" (C++ and java come to mind), regardless of what one may think of these loopholes. Designing a good static type system is extremely hard!

Re the arguments about language complexity: I think one thing that is implied is that languages, like programs, need to be refactored periodically. However, this rarely happens because for a popular language there is so much legacy code that depends on the old language constructs that changing them would break everything. So languages just go on adding feature after feature, and never subtract features which are no longer necessary. It's hard enough even to deprecate library functions! So what happens instead? New languages are written. I think this is one area where languages with macros win: they allow the user to do some of the design and thus allow the user to do his own refactoring. If you wrote your own object system, you'd be more willing to refactor it than if you were using an off-the-shelf object system.

Parenthetically (no pun intended) I wouldn't mind seeing languages with static typing AND macro systems (ideally with S-expression syntax as well).

Tests are necessary for ST programs as well. The difference is that DT programs require a lot more tests to achieve the same level of confidence...

I am awaiting for publication of the evidence behind this claim. I know this is not true for the older type systems of Java-like languages. If this claim is true for newer type systems like those of modern functional languages, can you point me to substantive descriptions of the studies which back this up?

"Studies" of this aren't necessary, because formal proofs exist. In fact, Frank's claim (italicized above) is understated - perhaps Frank was trying to go easy on DT :)

Other than in trivial cases, tests can never provide the "same level of confidence", w.r.t. the type behavior of a system, as a static type analysis. The reason is simply that static type analysis is deductive, and forms a proof, whereas a suite of tests of a program in a DT language merely provide inductive evidence for the hypothesis that the program is correct. Without resorting to other kinds of proofs, this hypothesis can only be proved by testing with every possible input value.

The "win" that a statically typed language offers is that a potentially infinite set set of tests which would otherwise have to be written to test the type soundness of a program, does not have to be devised or written. The compiler uses the types you specify to prove (or disprove) your program's correctness in this respect. This is impossible with non-trivial programs in dynamically typed languages.

So, when considering the comparison between test-driven DT and ST, any extra work involved in static specification of types should be balanced against the number of tests that do not have to be written for the ST program. Since that number of tests is essentially infinite, ST always wins. :)

Of course, practical experience tells us that we can produce working programs in DT languages without writing an infinite number of tests. This is partly due to programming discipline - essentially, the programmer reasons about the types in his program, and is conservative about the use of types, etc., and the result is a program which can be well-tested without requiring an infinite number of tests. However, this is still essentially seat-of-the-pants stuff. In truly mission critical systems, this can leave a lot to be desired.

Shifting gears, Frank provided an excellent insight into a core issue - here's an edited version:

Typing does not limit what you can model; instead, it limits how shallowly you can model it.

A conclusion from this, which Frank didn't dwell on, is that sometimes shallow modeling of a problem is perfectly reasonable. More thorough modeling may simply not be justified, cost-effective, etc. - this an obvious variation on worse-is- better. And of course, this may be true of a majority of "ordinary" business systems. I'd say that the strong showing of DT languages in e.g. the web application world, to a large extent reflects this fact, i.e. that DT languages are capable of being used to shallowly model problems, which may often require less upfront work.

Frank's observation also explains why DT languages can be so attractive for prototyping. During prototyping, models often start off shallow and get deeper as you go along.

Finally, it provides a reason for the resistance to ST among DT enthusiasts: if ST makes it more difficult to play at the shallow end of the modelling pool, this is not necessarily a good thing, considering that a large and important class of applications usefully occupies that space.

Choice of shallow vs. deep modeling is often, if not usually, outside of our control. It's pretty common for systems to hit the limitations of their models and require redesigning as a result. Of course, nothing prevents deep models from being expressed in a DT language. DT advocates will claim this means that DT languages are more flexible: they're able to play at both ends of the pool.

The question then becomes how important static checkability is for deep models. I agree with Frank, it can be pretty important. However, that discussion would be a rehash of all the usual arguments, some of which have been covered above, and I won't go there right now.

I agree with Michael:

Parenthetically (no pun intended) I wouldn't mind seeing languages with static typing AND macro systems (ideally with S-expression syntax as well).

We had a few references in the past to the Ocaml macro system, which may be of interest.

In the real world, the customer desires much more from her software than "type soundness". Even the most advanced type systems do not prove enough about the actual behavior of a program. You still have to write tests.

My experience is these tests more than make up for the lack of static type checking.

In theory there is no difference between theory and practice.

In practice there is.

The question then becomes how important static checkability is for deep models.

The kinds of statically checked models I have found most useful are concurrent state machines. These can be written, checked, and used to generate code in a dynamic language.

The ocaml macro system (camlp4) is very cool, but it's extremely heavyweight and difficult to use when compared to lisp's defmacro or scheme's define-syntax. As I understand it (others can correct me if I'm wrong) it operates directly on parse trees. This shows one example of s-expression syntax: an s-expression pretty much is a parse tree already.

Yes, but type soundness is a non-trivial minimum requirement, which ST helps to achieve. The argument that tests can substitute for this is an argument from a position of weakness, for a variety of reasons which I'll enumerate if you like. It's a tradeoff which is made for things like the flexibility of shallow modeling that Frank identified.

Even the most advanced type systems do not prove enough about the actual behavior of a program. You still have to write tests.

You do still have to write tests, for any non-trivial system. However, advanced type systems prove a lot that's important about a program, and they prove it without writing tests, and they prove it better than tests can. The advantages of this are demonstrated intuitively every time a statically-typed program works first time after it passes typechecking.

This becomes especially valuable in systems that take a long time to run: the earlier you catch errors, the faster you can develop. There are many kinds of system for which TDD is easier said than done. In fact, such systems are mostly what I work on professionally, which is why I have a healthy respect for ST, even though in my own personal development, I almost always start out with a DT language. Which is why I agreed with Michael about the kind of languages I'd like to see.

In over 20 years of professionally developing software, I have never encountered a customer asking for type soundness. That is not intended as a facetious answer. The customer wants correctly executing and easily maintainable code. Maybe that is best achieved with an advanced type system, but maybe not.

I personally have not found type soundness to be an important milestone on the path toward satisfying the customer's needs. I have not seen enough results from the FP community to indicate otherwise. It seems to me your argument makes sense on paper, but not necessarily in production.

Real data is welcome.

There are many kinds of system for which TDD is easier said than done. In fact, such systems are mostly what I work on professionally...

We work in very different domains, which thankfully is getting to the heart of the disagreement. Neither one of us can apparently generalize to the other's domain of experience.

I think you're misinterpreting my point. Correctly executing code can only be achieved by a program which uses types correctly, whether or not they're statically checked. All you're saying is that you're perfectly happy to achieve type-correctness by reasoning about types, writing tests which explicitly or implicitly test type correctness, and running those tests until you've worked out any type bugs, along with other kinds of bugs.

So you're lumping type debugging along with other kinds of debugging. In software development, lumping together different kinds of things is something that's always worth scrutiny. I'm saying that this process works well in some cases, less well in others.

(Actually, I was originally saying that Frank's observation about shallow modeling resonated with me as an explanation for why DT languages have an advantage for certain kinds of application, but I drew the other side of the picture too.)

I personally have not found type soundness to be an important milestone on the path toward satisfying the customer's needs.

It's not an important milestone because you're lumping it in as part of another milestone, i.e. passing your more general tests. How would you know if it's an important milestone, if you don't identify it separately?

Real data is welcome.

What sort of data would satisfy you?

We work in very different domains, which thankfully is getting to the heart of the disagreement. Neither one of us can apparently generalize to the other's domain of experience.

Well, I don't know what specific domains you're thinking of. For my part, I was in fact attempting to generalize across a wide range of domains using Frank's observation. I believe I have the experience to at least try that, having worked commercially on development of fairly simple apps, very complex apps, web apps, languages, and system tools, in both ST and DT languages, both imperative and FP.

I find attempting to characterize and discuss the nature of development in these often very different kinds of systems to be helpful for better understanding, so I'm not just arguing for the sake of it (despite occasional appearances to the contrary). You can program in two completely different systems without really grokking the relationship between the two - in fact, that's more common than not.

Back on topic, my experience is that there's a size and abstraction complexity level at which ST begins to have significant benefits, both technical and commercial. Do you dispute this, or would big/complex systems qualify as the kind of "very different domains" you're thinking of?

I agree with earlier observations that sufficient discipline can compensate for DT shortcomings, and I agree with you that tests can also compensate. There are other things that can compensate also. But compensating isn't always good enough.

Personally, I tend to view the ST vs. DT debate as largely a matter of taste. My preference for ST is that I know I'm sloppy enough that I make a lot of trivial type errors, and when they're eliminated my debugging time is dramatically reduced. Some programmers are undoubtedly more careful than I am in this respect, and for them the tradeoffs may not be worth it. However, I do like the feeling of knowing that my program can't have a type error. Of course, in the Real World (TM), very few languages (ocaml is one) actually give you this kind of guarantee (C and C++ don't come close, and java has loopholes as well).

BTW I recently read a powerpoint presentation by Robert Harper (linked to from LtU, I believe) that described static type systems as the best-known and most useful example of a theorem prover. I thought this was a very profound statement.

By the way, my guess is that Guido was trolling himself

Actually, I think what Guido was doing was marketing. For the average language user, "less (finger) typing" is likely to be a valid selling point.

Perhaps the FP & ST languages should take a lesson from this, and advertise themselves as requiring "less testing"! ;oP

I recommend trying test-first design, aka test-driven development, with or without a static type checker. This approach eliminates debugging my own code. What remains of debugging is really figuring out how some other software works that someone else wrote, without complete tests, using some really poor language, usually C or C++.

Test-first programming combined with refactoring is really a form of "deep reasoning" about a system. A "test" in this case is a poor man's theorem about how the system should behave. In theory, this approach is more ad hoc than a modern type system. In practice, it works very well, and I see people adopting it with measurable results.

More generally, if you model a complex problem with a simple ("shallow") model, you run into limitations in cases where distinct entities have been conflated, for example. Problems like this often manifest as an inconsistency in the program's types, and so static type systems help to debug this kind of problem. Think of a static type system and compiler as a rapid design/development/debugging environment for type schema - you can develop and test your type system without ever running your program, or even needing the program to have any functionality.

Of course, in languages like Python, classes provide some of the same kind of design-level debugging, but not the compile-time proof kind, nor the whole-program mathematical-consistency kind.

import sys


file = sys.argv[1]     # 'file' is a string.
file = open(file, "r") # 'file' is now a file object.

I can't do this in a statically-typed language, and it's a good thing ;-) I try not to do it in python either anymore.

Yes, adding that I find very little time working out "type bugs" per se, mainly due to a test-first programming cycle, i.e. many small tests, no application code written that is not preceded by a broken test that needs it, frequent refactoring.

• Write a small test.
• Write the minimum amount of code to satisfy the test.
• Refactor if needed.
• Repeat.

What sort of data would satisfy you?

I would hope claims of universal fact be accompanied by enough data for people to decide for themselves based on the quality of the data.

If you look back through my messages, I hope you will find that I always try to speak from personal experience and carefully state what I don't know to be proven one way or the other. I am amazed at the claims that are made in other messages that are generalized assumptions stated as absolutes.

I would hope people would:

• Keep an open mind, they don't know everything.
• Separate what they believe from what has been proven.
• Speak from experience rather categorizing how all people of category X think or act.

Back on topic, my experience is that there's a size and abstraction complexity level at which ST begins to have significant benefits, both technical and commercial. Do you dispute this, or would big/complex systems qualify as the kind of "very different domains" you're thinking of?

I have found that dynamic languages scale better, and in fact systems written in static languages take on more dynamic features in order to scale. Since I have not participated in large software systems development using modern type systems, I cannot speak to that. I would like to see an expert Smalltalk team and an expert Haskell team, say, tackle a large, distributed, multi-month, changing requirements, real-world project with some rational approach for making observations and conclusions.

But compensating isn't always good enough.

See, I have no data points that tell me it isn't good enough. My data points tell me its better than. I don't even see it as "compensating". I just don't see lack of static types even show up on the radar as something to cry about.

Some would argue that the language is too small to be useufl in real life, but according to your defintion this is not a robustness issue.

By the way, regarding C (and other languages) being "fragile to reuse or redesign" see my Component Libraries and Language Features paper:

The results should also influence the design of new language features for this purpose, and help create a taxonomy of kinds of abstraction breaking, and of abstraction breaking mechanisms. Using more expressive languages in general, and more expressive types systems in particular, may reduce the need for abstraction breaking, by allowing the creation of more flexible components.

let file = Sys.argv.(1) in
let file = open_in file in
let file _ = print_endline (input_line file) in
let file = file file in
file

The only guarantee you get is that all these "file"s are well-typed, not that their names are in any way helpful.

In the mean time, here is something to chew on: Robert Harper's posts to comp.lang.scheme.

In particular, the Scheme or ML? (was Re: multiple values) thread is very interesting, with comments from luminaries such as Harper, Matthias Blume, R. Kent Dybvig and Olin Shivers. Perhaps Ehud would like to put it on the front page? It would also make a good place to carry this now-lengthening discussion.

Here is a quote from Harper about ST vs. DT discussions, BTW, which perfectly expresses my own stubborn insistence on this topic:

Why don't people like me "just say no"? Because the issues aren't just a matter of opinion. If they were, it'd make sense to agree to disagree. But they're not, at least not in every case. To take a topical example, it's a Schemer's mantra that statically typed languages are more restrictive than dynamically typed languages. Yet the latter are merely tiny subsets of the former: the claim is just plain false. This is not a matter of opinion, it's a matter of fact. To me it is worth correcting --- perhaps repeatedly --- a persistent (I would almost say willful) misunderstanding of this fundamental point.

let file = ref Sys.argv.(1) in
file := open_in !file

Sounds fine to me. Unfortunately that Usenet discussion is almost seven years old. According to typical industry adoption rates, the modern type systems should begin to see widespread use around 2010, or die out before then. 8^)

let file = Sys.argv.(1) in
let file = open_in file in
let file _ = print_endline (input_line file) in
let file = file file in
file

Of course this same format couold be used in Scheme. In Erlang, the single assignment restriction would prevent it altogether.

Let's face it: Python is an ugly hack.

The Harper thread is interesting. I guess it depends on which static type system you mean. Pure untyped lambda calculus is more powerful than simply typed lambda calculus, but more advanced type systems (system F? I'm *not* an expert) are more expressive. I've never before heard anyone argue that there is anything *more* expressive than untyped lambda calculus, though. I guess it depends on what you mean by "expressive" i.e. does having the ability to enforce invariants at compile-time make a language more expressive?

My impression is that statically typed languages have real problems with some things that dynamically typed languages have an easy time with; two examples are reflection and supporting functional programming and object-oriented programming in the same language (I know ocaml does the latter, but the object system is to restricted for my tastes). That said, I'm all for more research on advanced static type systems.

Incidentally, let's make sure we keep the tone civil. I know people get worked up over these issues, but there's no need to get upset. I think the rest of the world would be highly amused at how passionately programming language people defend their favorite type systems ;-)

This is a cool thread.

Fair enough, let me try to restate more constructively.

Considering:

• The influences on Python
• The resulting limitations and special cases (e.g. "lambdas" aren't)
• Comparable languages, in particular, Ruby is a very nice DT language

I am not sure why Python would be a preferred language. Except that:

• It does have a useful library, e.g. Zope.
• A relatively large number of developers.

But I don't see much that speaks for the language, per se.

I'm all for more research on advanced static type systems.

I definitely am for this as well. There may be a tipping point out there, I just haven't seen it yet.

http://groups.google.com/groups?q=g:thl3243730853d&dq=&hl=en&lr=&ie=UTF-8&safe=off&selm=4tbes4%24gjf%40roar.cs.utexas.edu&rnum=4

I've never heard the ST vs. DT debate framed any better.

1. Should ST be preferred over DT?

2. Are current ST languages more or less suitable for large scale projects than are DT languages?

(2) is more difficult to answer, since it usually relies on empirical research which is sparse and personal opinions, which are not always objective.

(1) however is much easir to answer. In general, we would like to specify and prove as much as possible about our code before run time.

So the question becomes "are current type systems powerful enough" and if the answer to that is No, than you must answer the more fundamental question "are static type systems powerful enough possible?"

Personally (part of my researhc interesets) the answers are "No" and "Hopefully yes".

The main problem I see is that useful concepts like predicate types, dependent types etc. often result in unwanted complexity, and can (if not handled properly) make the type system undecidable (which means it is of no use to us looking for static guarantees).

I admit I haven't studies some of the languages discussed here (like Nice) that try to solve some of these issues, so maybe the solution already exists. But I wouldn't bet the farm on it just yet...

But we will get there.

P.S

Frank will say that the Haskell tpe system is powerful and useful right now. I am not disputing that - but I understand why Patrick wants empirical proof.

let file = ref Sys.argv.(1) in
file := Obj.magic (open_in !file);
print_endline (input_line (Obj.magic !file))

You could write some functions or macros to hide the Obj.magic from plain view if you do things like this on a regular basis... Though you probably shouldn't.

Nicely summarized.

Of course, Obj.magic is a totally awful hack/kludge, as even the authors of ocaml freely acknowledge ;-) Core dumps can easily happen when using it.

BTW, the UseNet post by Paul Wilson perfectly sums up my views on the dynamic typing/static typing debate. Soft typing anyone?