Lambda the Ultimate

This debate was mentioned here in the past, in connection with extreme programming. Robert Martin as far as I recall put forward a strong case for dynamic languages + unit tests. [I should really search the archives for my previous comments...]

Personally, I am undecided. Typing is obviously not enough, since types don't capture all useful information. The same can be said about Eiffel like contracts. But both can help with catching errors as soon as they happen. Either during compile time, or as soon as invalid values are generated.

This is a Good Thing since garbage has a tendency to slowly enter your database and corrupt useful data. Another important aspect is that explicit contracts (and types) help identify the faulty components. Now I know XP fans will just say re-run all your unit tests and the exact location of the error will surface (and this is a good idea, of course) but this is rarely done, requires time etc. Types allow this localization to be done automatically.

[Ehud] Typing is obviously not enough, since types don't capture all useful information.

First, many type systems are not statically decidable; among these are ones which do capture all the (extensional) behavior of a function.

But let's suppose that you don't want to put up with such type systems since, after all, they are not very well-suited for programming (no type inference, principal typing, etc.). So, instead you do testing.

To test something, you need to know what you are testing for. So you need a specification. If you are scrupulous, it will be a formal specification. Then you devise a set of inputs for the tests, and maybe a testing program. Now you need to know that your tests will actually ensure that your program matches your specification. If you are scrupulous, you will write a proof of the fact. If your proof is constructive, then your specification and proof together constitute a typed program, by the Curry-Howard isomorphism.

Well, that's a lot of "if"'s perhaps (but it's also a lot of work, and if your programming language isn't typed, then your test set will get a lot larger, since you have to test so many trivial things explicitly), but my point is that even if you use the testing approach, you're doing something which is fairly close to what a type checker and typed language-using programmer do.

Here's another thing to consider: haphazard testing can make your programs less efficient. This is because, whereas types make assertions about the extension of a program (the relation of inputs to outputs), tests are frequently over-specified, so they tend to assert things about the intension of a program (how it computes its outputs from its inputs). Thus, if you optimize your program, since the intension changes, your tests may break.

[Patrick] OK, you got the argument count correct, and yes, you sent an Integer when it was expected. You still have to write all the same unit tests to demonstrate the behavior is what you expected.

Yeah, but you don't have to write a test to check those properties, do you? And it's not so easy to check them. To prove that your function accepts any integer, you have to test it on every possible integer input (plainly impossible), or prove that its implementation is somehow invariant with respect to the property of being an integer and then test it on one integer, or something like that.

I see this argument about arity checking, etc. quite often. Usually the people who make it are people who have only ever used dynamically typed languages and a language or two with very weak type systems, like C. Often they have switched to Perl or something because C's type system is so unexpressive. This is not the case for advanced languages, like ML.

Another thing is that people who use expressive static type systems tend to exploit it much more than others. Have you ever tried to a program which makes really extensive use of higher-order functions, or genericity, or monads, or algebras, in a dynamically typed language like Scheme? I have. It's very frustrating. You make lots of silly errors which are hard to track down. Errors which would be caught instantly in a statically typed language. In this respect, static typing is an enabling technology, not a constrictive one.

I think these are all good arguments for static typing. But they're not why I use it. The real reason I like static typing is as follows.

Suppose you are given a massive box full of millions of oddly shaped Lego block-type things and told to build a house with them. (This is not a skyscraper argument, BTW.) One way to do it is to use a greedy strategy and start at the bottom, and every time you need a piece, to look for something with the right shape. This might work, but probably your house will look very odd, with lots of bits sticking out, occluding window and doorways.

Another way is to look at the pieces and arrange them into categories, and then develop rules which tell you what kinds of shapes you get when you stick together pieces from certain categories, rules which you can rely on in specific situations. This will not solve all your problems, but if you pick a good set of rules, it will let you concentrate on the larger task. If your set of rules is "complete" in a sense, then you furthermore know that you will also be able always to build your house following those rules exclusively.

It's true that another set of rules may work as well even though they conflict with yours, and following your own rules to the letter will cause you to miss some opportunities for "optimization". But that's a small price to pay for the gains you make.

Now, here's the important bit. Nobody uses the greedy strategy, or at least nobody who has successfully built a medium-sized program. Everybody has some more complex strategy for programming. OO, or waterfall, or patterns, or whatever. They attack problems using that strategy. Usually exclusively with that strategy. In my case, my strategy is to attack problems using algebraic methods.

A type system also induces such a strategy if it has a denotational semantics. In my case, the type systems I use have an algebraic semantics. Therefore, they exactly match my own strategy. Therefore, I hardly ever complain about typing being too strict or something, because when I get a type error, it reflects an error in my mental model of the task, not somebody else's. Once you get in this frame of mind, typing is 99% boon, and only 1% hindrance (mostly when you hit the limits of the type system, but I use languages with very expressive ones, so it doesn't happen much).

If you reverse this line of thought, then, users can learn to work in harmony with their type system if they pick one which uses the same semantics as they do. If you think in terms of OO, you need a language which has an "OO semantics", etc.

The thing is, semantics are always expressed in the language of mathematics, and mathematics is simply not OO, it's algebraic. OO is more coalgebraic, which can be expressed mathematically, but is at odds, stylistically, with a hundred or so years of mathematical literature. Other, team project methodologies and so on, have no conceivable mathematical basis at all.

This is why I strongly believe that the only programming paradigms which will survive to the end of this century are the functional and logic ones. Eventually, programmers will be writing mostly programs which deal with real world problems, problems which come up in physics and statistics and biology (someone will say "what about business?", but every business has to produce a product, and products typically involve the sciences), and these problems are always expressed mathematically, which is to say mostly algebraically, because that is the easiest way to express a complex problem unambiguously. Then the most obvious choice of paradigm is declarative.

What programmers debate is the use of partial specification using the type system, as opposed to manual testing.

I am all for typing, but I think the case against static typing has some merit.

To give an example, I often hear the claim that Ada programs run correctly if they pass the compiler - because of the type system. Same is said about ML etc.

Well, I write code - and have bugs - in these languages, so I am not convinced.

An analogy: If I would have written "here" instead of "hear" two paragraphs ago, a spelling checker wouldn't help me, since "here" is an English word.

In fact most bugs can go undetected by the type system (instead of i+1 retrun 1+2). Other bugs come from ill defined types...[I know type inferencing can help with this problem.]

To my mind type checking is important, even if it only helps catch some errors. I gladly spend the time writing the type annotations. Helps me think about the code.

I think type annotations make code more readable.

I also think that module specifications should include explicit type information.

But I have heard reasonable people argue the other side of the issue, and even give some interesting arguments...

It is interesting to note that type systems can indeed be used to write rather powerful specifications. When we design an API, we can encode in types patterns of correct usage. For example, we can specify that a file opened for reading can only be read from and closed. Therefore, any attempt to write into such file will trigger a compile-time error.

An article "Phantom types (very long)" http://pauillac.inria.fr/bin/wilma_hiliter/caml-list/200109/msg00097.html and its follow-ups show several interesting examples.

A POPL02 talk "Type systems for certified binaries" showed how to construct extensible type systems to express assertions about the code that are usually stated using Horn clauses. In other words, how to use the typechecker to do logic programming. Amazingly, typechecking in these remarkably expressive type systems is still decidable. Another talk showed how to use logic programming to help typechecker (to choose the correct instantiation of an overloaded function). The summaries will be posted.

However, the opponents of this view have a point. What they are saying essentially is that since you still must do testing, for properties that are not covered by the formal specification in the code. And, if these tests are any good, they'll uncover such errors as trying to read from a closed file.

Now obviously I wouldn't trust this approach in mission critical or simply very complex software systems. But when you think about more mundane programs this argument has some appeal.

However, the opponents of this view have a point. What they are saying essentially is that since you still must do testing, for properties that are not covered by the formal specification in the code.

So what? If type-checking is decidable, then there will be fewer things to check, and I already indicated that some of the properties which are checked are not easy to test.

Let's not throw the baby out with the bathwater.

Static type checking is one component of a philosophy which every programmer can conscionably subscribe to, namely that we should automate the tasks which can be automated, and spend our time doing (more rewarding) work which computers can't do for us.

Sure, writing your programs in such a way that they are statically checkable requires thinking more carefully about them, but that is something every programmer agrees to do when they decide to become a programmer.

The payoff of static type checking is that it solves a specific problem once and for all: if you change your program, you don't have to re-examine your test suite to come up with a new test for the class of properties which type checking checks; the compiler does that work for you.

The thinking is that (automated) regression testing is going to be needed anyway, so the advantages of static typing are diminished (and the effort is considered to be too much for so little a gain. I don't see it that way, BTW).

But seriously, I understand the "degree of effort" factor. In fact, I think the static typing versus dynamic typing issue reflects a difference of culture.

But, I'm curious: you claim to understand both sides and yet ultimately agree with my perspective; what is it that makes you come down on the side of static typing?

I also tend to like provability, and types are help capture specifications.

Another thing is that I find types make languages more expressive. If you know that a Length() function is going to return a natural result, why not tell the reader?

My main problem with most (imperative) typed languages is that their type systems are weak, and thus make programming more difficult than it should be. In fact I propose the conjecture that the stronger (and more static) the type system, the less public library code you can find. This is sad, but I am sure will change over time.

My main problem with Don's statements was not the fact that he advocates typed (compiled) languages over untyped (usually script) languages. I too prefer typed languages, provided they support generics et al. My fondness for JavaScript (a dynamic untyped language) notwithstanding, such systems often do save me from having to track down lots of stupid bugs (indeed the Beyond library introduces a smidgeon of typing into JavaScript, for example a reliance on a function's argument signature.)

My main problem was that Don takes an either-or stand on compiled vs. scripting languages. This to me is like stating that a saw makes a very poor hammer. This is obvious (usually :) I believe that both types of languages have their place. Indeed, by its very definition a script language is intended to script something. And that something is usually an application written in a compiled language. Examples of this approach include most OSs, browsers and many applications such as Office.

I find that systems with I have designed that I am the most proud/fond of made significant use of scripts for tasks such as:

• (Advanced) user customization.
• Capturing logic as data.
• System integration (glue).

Though he does not explicitly state it, I believe Don's objection is to building web services using script (untyped, dynamic, interpreted) languages. At least that is the impression I get from the context of his statements. That is a valid argument, and one that at the present I'm undecided on. If you intend to utilize web services as the infrastructure for some critical application than Don's assertions do make sense. OTOH, samples I've seen demonstrate that building web services using dynamic environments, at least at the present, are a lot simpler. And if you consider the use of scripts as glue between applications, it also makes a lot of sense.

You can find this result in many textbooks, but perhaps it's a little bit surprising, since typed LC is strongly normalizing while untyped LC isn't. The reason it works, of course, is that there is a very non-trivial degeneracy, namely you take the set of base types to be a singleton set {o} and demand that o = o->o (read "=" as, "is isomorphic to").

The search for a model of this domain equation, as it's called, was the impetus for Dana Scott's hugely influential work on denotational semantics, and he has argued that viewing untyped LC as a model of typed LC is the "right" way to look at untyped LC.

He has a good point too, because what makes this isomorphism work is precisely the fact that you have to interpret the function space operator (->) in a domain of computable functions, rather than the more conventional domain of merely sets and "mathematical" functions, where the cardinality of the sets o and o->o makes the isomorphism impossible, since sets are isomorphic iff they have the same cardinality.

BTW, here is a fragment of part of Matthias' post which is relevant to our discussion:

[Proponents of dynamic typing often cite scripting as an example where their favorite technique shines. However, I beg to differ: Scripts -- especially the run-once-and- throw-away variety -- would benefit tremendously from static typing. Dynamic typists say that the bugs that static typing finds are easily found by testing. But thorough testing is against the very spirit of run-once scripts. And of course, if I have the time to do thorough testing, then I also have the time to type a few more brackets...]

While I definitely agree with the gist of Matthias' post, I don't find it surprising at all the most script languages are dynamically typed. Static type checking requires parsing the code at development time, and to many people such a step is associated with compilation. This is of course patently wrong, some script languages have a parsing step, while us old-timers remember lint which checked C code independently of compilation. However, I do believe that many script users would resist any interruption between editing and execution.

Also, static typing often requires some extra typing and attention to details. This "wasted" time is obviously returned in spades during debugging, but everybody likes to believe their code is bug-free anyway :)

There are also some technical difficulties with static typing as applied to programming languages in general and scripting in particular. First, without generics much of the benefit of static typing is lost. Without generics, you need to do much of the type checking at runtime (see Java's collection objects for example) so its back to square one, almost. Yet adding generics to a language is no trivial undertaking, and can certainly sacrifice its simplicity (I can just imagine Dave adding templates to UserTask).

A second issue to contend with is implicit type conversion. Most scripting languages are very lax in their conversion rules. If a conversion is at all possible it will often be done automatically. Obviously implicit type conversions can negate all of the benefits of static typing (which is why C++ allows only one such conversion, and introduced the explicit keyword). Yet many scripters have grown so used to such conversion that they view them as a key requirement of their development environment (BTW, such conversions can make a script program more robust by overcoming some programmer errors; the old "do what I want not what I say").

Third, script languages are often dynamic to the degree that some of the code is generated at runtime (even VBScript has an Eval() function.) This means that some of the code cannot be checked until runtime in any event (Beyond for example does quit a bit of this, though its an extreme example.)

Finally, I'm not quit sure how static typing can be applied to languages that use OOP but are not class based. For example, in JavaScript I can define a new object:

What is the type of such an object? Maybe type checking can be performed based on the properties the object implements, but properties can be dynamically added and removed at runtime:

Also, static typing often requires some extra typing and attention to details. This "wasted" time is obviously returned in spades during debugging, but everybody likes to believe their code is bug-free anyway :)

There are also some technical difficulties with static typing as applied to programming languages in general and scripting in particular. First, without generics much of the benefit of static typing is lost. Without generics, you need to do much of the type checking at runtime (see Java's collection objects for example) so its back to square one, almost. Yet adding generics to a language is no trivial undertaking, and can certainly sacrifice its simplicity (I can just imagine Dave adding templates to UserTask).

What is the point of criticizing static typing on the basis that antiquated languages like Java and C are overly restrictive when there are plenty of examples of modern languages like ML and Haskell where static typing is very expressive? If I criticized dynamic typing on the grounds that it interferes with some feature or other of Perl, I would never live it down.

Finally, I'm not quit sure how static typing can be applied to languages that use OOP but are not class based. For example, in JavaScript I can define a new object:

var x = {
 one : 1,
 var : "2",
 three : function() { return 3; }
};

What is the type of such an object? Maybe type checking can be performed based on the properties the object implements, but properties can be dynamically added and removed at runtime:

x.four = /4/;

That's not very hard. In ML, it could be coded as a record. If the methods depend on each other, you need recursive or coalgebraic types. See Abadi and Cardelli, "A Theory of Objects" for the recursive approach; their type systems are all for object-based languages. I don't think they handle adding/removing methods dynamically, but I don't see why you would want that capability in a statically typed language.

What is the point of criticizing static typing on the basis that antiquated languages like Java and C are overly restrictive when there are plenty of examples of modern languages like ML and Haskell where static typing is very expressive?

Java antiquated?! Java is the most modern language in the world, with the exception perhaps of C# :-D

Have I criticized static typing? I don't believe I have. In fact I began my post by stating that I agree with Matthias' post. The point I was trying to make is that adding static typing in a way that only adds value is not trivial, and there are some serious issues that must be addressed in the process.

Yes, ML and Haskell are better than C. But unless you get the entire scripting community to switch en mass to Huggs, you are talking about adding static typing to languages that are much closer in nature to C. Therefore the end result will look like C++ IMO. C++ generics are notoriously hard to implement, explain, and use. I'm still looking for the C++ compiler that is up to the spec on templates. (I'm not familiar with Java's generics so I can't comment on it.)

If I criticized dynamic typing on the grounds that it interferes with some feature or other of Perl, I would never live it down.

Feel free to criticize Perl as I'm not a fan either. OTOH any static typing solution that you want to seriously propose to the scripting community must integrate well with Perl.

That's not very hard. In ML, it could be coded as a record.

Maybe, I'm not familiar with ML. However, the very fact that ML has records seems to indicate that there is a difference. My point was that in a language like JavaScript objects are not an instance of a concreete type. Instead they are constructed at runtime. A simplified description is that you take a "blank" object and tack properties (fields and methods) onto it until you get what you want. How then can you define an overloaded method for such object "types"? The object's constructor function might be used as a reference, but as I've shown objects can be created without an explicit constructor. The prototype can be used, but different object "types" can share a prototype (and replace their prototype at runtime). You might overload based on the existence (or lack thereof) of a property, but properties can change over an object's lifetime, so its impossible to check at development time.

BTW, Microsoft has introduced static typing into JavaScript in the form of JScript.NET. The price is that JScript.NET is not JavaScript. It is C# with JavaScript keywords.

Java antiquated?! Java is the most modern language in the world, with the exception perhaps of C# :-D

I disagree. Java is quite a conservative language, designwise, except perhaps for the bits to do with security and class-loading. While I have no inclination to go into a full-scale criticism of Java, I can think of a few things off the top of my head.

Java's type system is relatively weak, yet doesn't support type inference. It has no generics, only single-inheritance, no mix-ins, single-dispatch, name rather than structural equivalence of types, no tuples and only an approximation to the higher-order functions in the form of inner classes. Its module system is all mixed up with its namespace management, its namespace management is mixed up with its access management, its equivalent to C's const is broken, and I have seen strong criticisms of its approach to concurrency and synchronization (though I don't know much about that).

If you think Java is state-of-the-art, even for an OO language (he said with heavy irony :), you need to go out and read a few research articles, or even a few of the books published on the subject of OO, for example the Abadi and Cardelli text I mentioned.

You will probably say something about the JVM or the size of its libraries now, but I don't consider those parts of the language itself, since they can be added to any halfway decent language, and even some that aren't halfway decent.

Have I criticized static typing? I don't believe I have. In fact I began my post by stating that I agree with Matthias' post.

I'm aware of that. I didn't mean "criticize" in the sense of "to attack" or "to denigrate" and I'm sorry you read it that way; I meant "criticize" in the sense of "to point out weaknesses". And I don't consider lack of "interoperability" with other ill-considered features a weakness, though certainly it is nicer when a useful feature is easy to integrate with others. (Perhaps I should have said "critique", but I'm uncomfortable with the trend of "verbizing" nouns.)

But unless you get the entire scripting community to switch en mass to Huggs,[sic]

What has the scripting community got to do with it? If we started designing languages based on every whim of the scripting community, we would be in deep water indeed.

you are talking about adding static typing to languages that are much closer in nature to C.

I don't see why. There is nothing stopping you from adding a C-like syntax on top of ML semantics, or even Haskell-like monadic semantics, like Mondrian's, and, as everyone knows, syntax is far more important than semantics. :/

Maybe, I'm not familiar with ML. However, the very fact that ML has records seems to indicate that there is a difference.

There is a difference, but not for the example you gave. And also, the "difference" is not that records are the wrong thing, but rather that you need something additional. For example, the Abadi-Cardelli calculus is built on records.

My point was that in a language like JavaScript objects are not an instance of a concreete type. Instead they are constructed at runtime.

I understood your point; you didn't understand mine, probably because you have never encountered an OO type system with structural equivalence of types.

In systems like Abadi and Cardelli's, two objects have the same type if and only if they have the same interface, i.e., have methods with the same names and types. There are no class declarations. For them, a class is just a function which constructs objects with a certain interface. A-C call such languages "object-based", as opposed to "object-oriented". They are similar to prototype-based languages.

You can "tack on" new methods if you like; it makes no difference. (I think I said the opposite in my last post; that was wrong.) The new object will be a subtype of the old, since it has an additional method. What you can't do, as I recall, is update a method with something of a different type, sub- or super-, since it's unsound, but I would have to look at the book to be sure of this, and I don't have it here...

Still, that doesn't change what I said about structural typing. It just means that when you create an object in the AC calculus, you have to create it all at once. You're not limited to any static class declarations.

Actually, this is an interesting point. I remember when I was reading the book and had seen the recursive approach to objects elsewhere, I always thought there was something awkward about it. Now I know about coalgebras, etc. and I wonder if a corecursive approach wouldn't be more natural. &cough& Whatever that means! (I only understand coinduction so far.)

Let's go with that corecursion idea. I like the sound of it. ;-) ;-) ;-)

Perhaps I should have said "critique", but I'm uncomfortable with the trend of "verbizing" nouns.)

No offense taken, but I wasn't attempting to critique static typing either. Stated explicitly, the points I was trying to make were:

1. Implementing static typing in a way that actually does add value is not trivial.
2. This is especially true when static typing features are added to an existing language.
3. It may be impossible when said languages are highly dynamic, e.g. JavaScript (at least without significantly detracting for the language's functionality, e.g. JScript.NET)

What has the scripting community got to do with it? If we started designing languages based on every whim of the scripting community, we would be in deep water indeed.

This thread was prompted by Don's appeal to the scripting community, therefore I've responded in that context. But beyond that, I disagree with what I perceive to be your standing on this issue. I believe that the programming community at large would be better served by the incremental introduction of improved programming practices into existing languages and tools than by the development of a revolutionary language in some ivory tower.

Not that academic pursuit is not required, on the contrary it is essential. But in order to have true impact, the output of that endeavor should filter down to "street level". Thus the wishes and whims of the scripting community, or the programming community at large must be eventually taken into account.

On a personal level, over the years as a developer working mostly with C++, I've often lamented the deficiencies of that language. As many of these deficiencies seemed to stem from the requirement to be backward compatible with C, I considered that decision to be a poor one. As I've grown older (I'm now a whopping 34) and more experienced, I've come to appreciate Bjarne Stroustrup's design choice. Indeed I now believe that had he not designed the language in this way, it would not have succeeded (in which case I would have probably used C, eeck.)

I disagree. Java is quite a conservative language, design wise

My comment was indeed tongue-in-cheek, but it again goes to my argument above. James Gosling did not decide to preserve compatibility with any previous language in form, but he did do so in spirit. I do not believe that Java would have succeeded to the extent that it has, if not for its similarity to C and C++, Sun's hype machine notwithstanding. Indeed, this POV seems to be validated, or at least indorsed, by Microsoft's design of C#.

To summarize, if static typing can be added to the main scripting languages in a way that does not detract to much from their existing feature list, nor alter their behavior to an extent that would be unacceptable to most users, it would be a very good thing.

For example, the Abadi-Cardelli calculus is built on records

Thanks for the reference, it looks very interesting.

Re: corecursion. Just another thing on my to-do/learn list. Incidentally, Charity supports higher-order coinductive datatypes, which are largely the same thing. Mark Schroeder's master's thesis, Higher-Order Charity, available here, has a couple of simple but instructive examples of object-like things, like Logo-style turtles and processes.