Lambda the Ultimate

More so, if we mean more - it's high time we tried to make sense of what that "more" means exactly.

rwuyts: Note that I take the definition quite broad, a la Guy Steele: a dynamic language is one that defers as many decisions as possible to runtime.

Here's what bothers me: I grew up in southern Indiana, stumbled across "The Little LISPer," SRI edition, at the IU bookstore while still in high school, and fell in love. Went to IU, hung out in Lindley Hall talking to folks like Douglas Hofstadter and Dan Friedman, and fell in love with Scheme and Lisp. Since it was the mid 1980s, I also was exposed to, and fell in love with, Franz Lisp and Smalltalk-80. For the entirety of the remainder of the 80s and 90s, I was competely insufferable on the subject of Scheme/Lisp/Smalltalk. I mean Erik Naggum insufferable.

Around the beginning of the 21st century, though, I discovered Ensemble, and through it, Objective Caml. Of course I'd seen Standard ML before, but had never found a compelling reason to learn the seemingly-byzantine syntax. Ensemble was a good enough reason. In addition to that, O'Caml has, as we all know by now, a rather nice object system and excellent performance, generally speaking. So I finally dug into my first type-inferred statically-typed language.

In the meantime, I continued writing software for a living, generally in the usual suspects of C, C++, assembly language, and Java, sometimes all in the same project. Upon all-too-rare occasion someone would pay me to write in Lisp, and I never did land a Smalltalk job, although I came close on one ocassion. But all of these experiences add up to me having a screaming horror reaction to "defer as many decisions as possible to runtime." My experience has been that "defering as many decisions as possible to runtime" is what most projects do anyway, regardless of what language they're written in, resulting in a whole raft of utterly predictable bad results.

As I see it, the problem is that people believe some unfortunate things about "static" vs. "dynamic" languages. For example, they tend to believe that only dynamic languages support interactive, incremental development or hot replacement of running code. Some tend to believe that only Lisp and defmacro-style (vs. Scheme's hygenic) macros make domain-specific embedded languages possible. Finally, and most perniciously, some actually believe that there's some expressive magic to "dynamic typing" that allows these languages to do things that "can't be done," modulo Turing equivalence, in any statically-typed language, no matter how rich its type system, or whether the dynamic language aficionado has ever heard of the language and its type system or not. But as a very pertinent counter to this, we can track CTM in Alice, since it remains the closest thing to an apples-to-apples comparison I've yet seen.

As I've written before about "dynamic languages," given my history, I feel a lot like Agent Mulder: I want to believe. But as type theory continues to make inroads on important subjects like safe concurrency, proofs of security properties, and type-safe distributed programming and rebinding of local resources, it gets harder and harder every day. The "dynamic language" response to TyPiCal, Flow Caml, and Acute seems to be, quite literally, "you and your users don't need it."

This bothers me. A lot.

In response to TyPiCal and Acute, I would point out Erlang. And in response to Flow Caml I'd point out E. Is there something I'm missing here as far as the relative advantages of these languages?
Not to say I'm a "dynamic language" guy, but these languages seem to respond to these issues pretty well.

... but they all "defer as many decisions as possible to runtime," i.e. they don't provide me any guarantees before I deliver code to my users. Partially as a consequence, they're forced to do some of what they do in a particular way: for example, Erlang and E both must implement message-passing concurrency in order to be able to make any strong claims about avoiding deadlock and race conditions. Don't get me wrong; I love message-passing concurrency, in general. But as per CTM, sometimes I really do want to be able to take advantage of shared state, and I'd like not to have to give up safety against deadlock and race conditions to do so.

The same applies to object capability security: I love that E generally makes the secure thing the default/easy thing, and E and EROS remain the places I point people to for the best currently available thinking on security. But I want more; I want proofs before I deliver code. It should tell you something, for example, that in order for Auditors to work, the source code needs to be attached to the delivered code!

So the issue remains what the issue has always been: who deals with the error, your users when they use your product, or you, before you ship it?

So the issue remains what the issue has always been: who deals with the error, your users when they use your product, or you, before you ship it?

Serious question: do you have any evidence to indicate that with current tools, systems developed in dynamic languages suffer from more errors in production?

One point which often seems to be missed is how succesful testing can be. I don't know if any work has been done on the kind of coverage of type errors that is achieved by typical testing processes, but experience indicates that it is surprisingly high. I suspect that some of the attitude of "how can you possibly deploy a system that hasn't been statically checked" comes from badly underestimating the effectiveness of ordinary testing in catching type errors.

I still very well might choose to use good static checking of some kind in a system that was truly mission-critical — e.g. things that'll blow up and/or kill people. For anything less critical than that, tradeoffs come into play. Erlang is used in systems that many people would call critical, although a telecom switch going down usually isn't as bad as a plane crashing. But the majority of systems are much less critical than that.

A good question to reflect on is why it is that Erlang and E are dynamically checked.

In my understanding, Erlang OTP is designed to use process isolation for fault tolerance (Making reliable distributed systems in the presence of software errors). That really is different from the situation we have in Smalltalk.

Highly recommended environment to evaluate which ideas you really trust :-)

I can positively say that I get more errors, problems, and late night debugging sessions for my daily Zope work because Python is dynamically typed. When I run across a mysterious error, I sometimes notice that some code paths could never have worked at all, so the author has obviously never executed that bit of code.


On the other hand, if all the errors had been fixed in the standard "error/headscratch" cycle, it's possible the software would never have reached me, since many of the Zope extensions I use were designed for one person to handle their immediate need.


I suspect that test driven development applied to these same projects would mean better code in less time, and fewer problems for me. In my opinion unit tests and static typing can have roughly the same functionality.


I'd still instantly switch to Hindley-Milner plus HUnit plus QuickCheck if there were an equivalent Haskell web framework available.

--Shae Erisson - ScannedInAvian.com

In my opinion unit tests and static typing can have roughly the same functionality.

I don't think this is so. There may be some overlap, but they are more complementary, IMO and IME.

One way they work together is when the type suggests what the boundary-case tests will be. The type tells you what range of inputs you need to consider, the tests what behaviours you want with respect to particular values or ranges of values of that type.

A different way of putting it is that types provide design information about the sorts of things that exist in your program, the tests tell you what you expect to do with them.

I agree that types and testing serve two different purposes. However, the real point in this case is that testing can catch a high proportion of type errors — much higher than might naively be expected. In practice, in many situations, testing is a satisfactory replacement for static type checking.

In practice, in many situations, testing is a satisfactory replacement for static type checking.

Whenever I read someone write, "but in practice X is satisfactory," I know that in five years, when people more creative than the author have found a gaggle of situations in which X is unsatisfactory, a cargo cult will be using this as a rationale for rejecting anything which breaks X. Look how long (character set) codepages, three-letter file extensions, fixed-size buffers and a million other things have survived.

But, no, you're right: worse is better, and what's more it creates employment opportunities for hundreds of people with mutually incompatible solutions, each of which also creates new problems.

testing can catch a high proportion of type errors

Testing does not catch any type errors, period. A type error is defined by an independent standard called a type system, and in its absence you cannot decide whether a dynamic error "would have" consituted a static error. Saying that a test catches a type error is like saying a string is ill-formed without specifying the language you are trying to recognize, or saying that a program is incorrect without specifying its desired behavior.

Besides, static typing has other benefits than increasing program safety, but I won't get into that.

And, BTW, what is this crap doing on an ACM conference page?:

Java and C#, the latest mainstream static languages, popularized to a certain extent dynamic language features such as garbage collection, portability and (limited forms of) reflection.

Since when are "garbage collection" and "portability" "dynamic language features"? Even "(limited forms of) reflection" are clearly not intrinsically "dynamic" (whatever that means) if they are supported by "the latest mainstream static languages" (and, in particular, in much more sophisticated ways by unpopular-but-nevertheless-well-documented-in-the-literature typed languages like MetaML).

Neither, BTW, are the following "dynamic" language features: interpretation, "duck typing", extensible syntax, significant whitespace, "lambdas", comprehensions, generators or most of the other stuff which the untyped language community likes to relabel and then appropriate as its own.

When I see such claims on webpages of non-researchers, I try to be generous and put it down to ignorance rather than willful dishonesty. But when I see it on a research page, it goes to credibility. What do you have to say about this, Peter?

Reassuring that some things can be counted on. :-)

Count me as one who favors as much meta information built into programs as is feasible, providing a roadmap of sorts.

In practice, in many situations, testing is a satisfactory replacement for static type checking.

Whenever I read someone write, "but in practice X is satisfactory," I know that in five years, when people more creative than the author have found a gaggle of situations in which X is unsatisfactory, a cargo cult will be using this as a rationale for rejecting anything which breaks X.

Sure, but mob behavior doesn't change the fact that in practice, in many situations, testing is a satisfactory replacement for static type checking. Note the qualifier, which you elided in your generalized quote.

Testing does not catch any type errors, period.

A type error is defined by an independent standard called a type system,

and in its absence you cannot decide whether a dynamic error "would have" consituted a static error.

Even with your definition of type, this is incorrect, and I suspect you probably know it. The reason is that programmers in dynamically-checked languages use informal static type systems to reason about their code. They infer static types for terms.

The fact that these programmers can't easily write these static type systems down in a form you would be happy with is actually a demonstration of what a hard problem they're solving: years of effort, and soft typing tools still have a hard time duplicating this feat which human programmers perform.

Saying that a test catches a type error is like saying a string is ill-formed without specifying the language you are trying to recognize, or saying that a program is incorrect without specifying its desired behavior.

Sure, but mob behavior doesn't change the fact that in practice, in many situations, testing is a satisfactory replacement for static type checking.

Let me give an approximate analogy. Let's say we are talking databases. I have a number of programmers who hit that database for various purposes. Let's say each of these groups has a set of unit tests for their software. Now, having said that, does this mean I need not worry about formally specifying the schema for the database? I'd say that even given all the tests, you'd be insane not to use the type system provided by the database (referential integrity, etc...). If you don't enforce this stuff on the database, sooner or later the data is gonna get corrupted. This is the case, even though the languages provided for typing a database system are very crude, hard to use, and cumbersome for all sorts of problems that will be encountered.

I suppose Frank believes that those who don't avail themselves of formal type mechanisms are as insane as those who use databases but don't formally enforce integrity. If I really want to know what the database does and is capable of doing, I'd rather have a schema than a bunch of code that hangs off that schema. In the same sense, if I want to know what a program does, I'd rather have a definition of the types manipulated by the program rather than have to read the program itself.

Even with your definition of type, this is incorrect, and I suspect you probably know it. The reason is that programmers in dynamically-checked languages use informal static type systems to reason about their code. They infer static types for terms.

Sure, but mob behavior doesn't change the fact that in practice, in many situations, testing is a satisfactory replacement for static type checking.

I don't think it is a satisfactory replacement, exactly because tests have little extractable meta information concerning the program behavior.

I agree about that. Being pedantic in my defense, note that I said that testing can be a satisfactory replacement for static type checking, not for static types. I meant that tests can be a satisfactory replacement for the error-checking behavior which static type checks provide, not that static types don't have other benefits.

I'd agree that types are present in any program ever written. The question is whether that type information is implicit (vaguely defined), or whether it's explicit. If it's implicit, then it is inseperable from the code itself and will defy any attempts to be seperated from said code.

I don't think it's as bad as that, in many or even most cases. Some languages are better than others, and some programmers are more careful with types than others. Look at any term in any program and it's possible to infer various things about the type of value which is expected at that term, just by looking at the operations directly involved. What's more difficult is proving that this expectation will always be satisfied. Automating such proof is even more difficult. Because of these difficulties, human programmers can reason about programs in ways that are difficult for even whole-program compilers to duplicate, and we know that they succeed at doing this, otherwise most programs in dynamic languages simply wouldn't work.

Static type checking limits programs to only expressing things that the static type system can prove are OK, as opposed to expressing things that the human programmer believes are OK. That's the source of both the expressiveness loss with statically checked languages, and the class of runtime type errors which are unique to dynamically checked languages.

...I really don't have much more to forward the discussion beyond all the web ink that's already been spilled on LtU and various other fora. We definitely need both types of languages, as the things we do with PLs varies from the mundane to the sublime.

Come to think of it, I guess I do have one other parting shot. :-)

Unit tests really should involve checking the types of the parameters being passed around to verify nothing out of the ordinary is occuring. Which means, of course, a Unit Test in a language that has no formal type mechanism winds up having to do the same kind of work that a static compiler has to do. And if you're going to have to write a bunch of type checks, wouldn't it be easier to leave that up to an automated system (i.e. you don't have to write your own type checking system within the Unit Tests).

Granted, most times the Unit Tests are not really checking types being manipulated, but then isn't that a hole in the Unit Test itself?

It's also worth pointing out that a typed language offers additional, neat ways for doing unit testing - for example, the type-driven random testing performed by QuickCheck.

Unit tests really should involve checking the types of the parameters being passed around to verify nothing out of the ordinary is occuring.

Which means, of course, a Unit Test in a language that has no formal type mechanism winds up having to do the same kind of work that a static compiler has to do.

And if you're going to have to write a bunch of type checks, wouldn't it be easier to leave that up to an automated system (i.e. you don't have to write your own type checking system within the Unit Tests).

With the assertion approach I mentioned, you effectively do get an automated system. The type assertions are exercised "automatically" by the unit tests, without the unit tests having to do any type checking themselves. The difference is that the actual checks are less comprehensive: static-checking compilers are proving type safety at every term in the program, for all possible runs of the program, whereas unit tests and assertions are only testing what happens in certain test cases.

However, although the checks are less comprehensive, they have results that (superficially) seem disproportionately reliable. To coopt a phrase we've seen around recently, this could be called "the unreasonable effectiveness of testing".

My "testing is often a satisfactory alternative" claim relies on the same properties of programs that type inferencers rely on: data flows through programs in predictable ways, and the types of terms have strong interdependencies. Because of this, even though tests can only exercise a fraction of the possible program states, such testing can nevertheless ensure, to a high degree of confidence, that you won't get any type errors in a tested, deployed program.

Of course, this isn't the kind of proven guarantee that you get with static checking. However, in many situations, that really isn't important enough to override other considerations. And I'm not just talking about "mundane" systems. There are quite a few sophisticated systems out there written in dynamic languages.

The unreasonable effectiveness of testing is what I was getting at when I asked earlier about any evidence of errors in production for dynamic vs. static languages. The only direct response to that point was from shapr, with an anecdotal observation about code that hadn't been properly tested. The question of evidence is still open. My own experience is that type errors in tested, deployed code are not a big concern, even in dynamic languages.

This is also where I was coming from in a discussion some time back, when I suggested that the main practical benefit of static type checking today is in the convenience it offers programmers, in terms of cutting down the edit/run/fix cycle by detecting type errors earlier, as well as in the meta-benefits mentioned related to extra information embedded in the code.

The "guaranteed type-safe in production" point is just not as big a deal in practice, much of the time, as many of its proponents would like to believe — other than from a marketing perspective, where it's a very effective hook which plays to a desire for perfection. Many people like to believe that their systems are just about as mission-critical as ICBM control software, and require as much scalability as Amazon or Google. In this context, static checking seems like a no-brainer.

The future applications of static checking to other kinds of properties, like concurrency, sound very promising, and could very well provide some much stronger arguments in favor of static checking, but at the moment these seem almost entirely academic.

However, although the checks are less comprehensive, they have results that (superficially) seem disproportionately reliable.

The February issue of ACM Queue ran an article titled Too Darned Big to Test by Keith Stobie of Microsoft. Here's a seemingly relevant quote that seems to (indirectly) support your claim:

For many collections of test cases, running the minimum set of test cases that give the same coverage as all of the test cases typically finds almost all of the bugs that running all of the test cases would find.

Industrial experience at several companies appears to confirm this. For example, for an industrial program of 20,929 blocks, choosing tests only by function call coverage required only 10 percent of the tests while providing 99.2 of the same coverage. Reducing by block coverage meant that 34 percent of the tests provided the same block coverage and 99.99 percent of the same branch (segment) coverage. Further, there were no field-reported defects found that would have been caught by the full set of tests but missed by the coverage-reduced set of tests.

...after all, they are a big supplier of them. :-)


Just so we don't skip some relevant sections:

We must start again, beginning with good design (including dependency analysis), good static checking (including model property checking), and good unit testing (including good input selection).

Later in the article:

All of this data can also help independent testers later because defects found through static analysis are early indicators of pre-release system defect density. Static analysis defect density can be used to discriminate between components of high and low quality (fault-prone and non-fault-prone components).

As for the part quoted:

For many collections of test cases, running the minimum set of test cases that give the same coverage as all of the test cases typically finds almost all of the bugs that running all of the test cases would find.

I think it's possible to easily misinterpret this study. It's not claiming that a minimum set of tests finds all the bugs. It's claiming that a little testing finds a very large percentage of the bugs that can be found with that type of approach. In other words, it's actually quite negative from the standpoint of testing, in that it's claiming testing has a very steep law of diminishing returns (as we would say in economics).

In other words, it's actually quite negative from the standpoint of testing, in that it's claiming testing has a very steep law of diminishing returns (as we would say in economics).

I'm not sure this is really that negative.

A different way to put it is that it is easy to test yourself to confidence, but very hard to test yourself to certainty.

This is really more of a negative statement about the futility of striving for certainty. ;-)

I think you nailed it wrt confidence. :-)

Really, this is just the kind of practices that pervade most manufacturer concerning quality control. Random sampling gives you almost as much confidence in product quality as testing each and every widget produced. Since the costs of testing each and every widget would be exhorbitant, most manufacturers settle on the statistical confidence of random testing (with the occasional finger slipping into the product).

Personally, I think software tests are cheap so that running a complete suite of tests is not costly. However, writing those tests does involve tests, so the question is how do you write tests that are not comprehensive, but still catch the errors.

The reason is that programmers in dynamically-checked languages use informal static type systems to reason about their code. They infer static types for terms.

True, but not all programmers do this very well, and even those who do don't necessarily leave a record of their thinking for others (or their future selves) to understand or verify as the situation changes.

Again, there is a complementarity with testing: you typically only test obvious boundary cases and a few typical cases under an assumption about the possible range of inputs.

Without an explicit record of what this possible range is, it is very difficult, even for the "smart guys", to see if all important cases have been tested or if later changes have mutated the assumptions so that the test cases are no longer sufficient.

For quick and dirty solutions this may be OK, but if you want to maintain it long term, not so much.

True, but not all programmers do this very well

Perhaps not "all", but enough seem to do it well that deployed programs in dynamic languages don't have a poor track record, and aren't notorious for generating large numbers of runtime type errors. (Ignoring edge cases like Javascript written by web page designers.)

even those who do don't necessarily leave a record of their thinking for others (or their future selves) to understand or verify as the situation changes.

That can be mitigated by good practices, including type assertions. The TDD movement has gone some way towards methodologizing this kind of thing.

Without an explicit record of what this possible range is, it is very difficult, even for the "smart guys", to see if all important cases have been tested or if later changes have mutated the assumptions so that the test cases are no longer sufficient.

I'm not arguing against making an explicit record of type information, and embedding it in the code, and again, assertions can do that. As for test coverage, that's an issue for either kind of language. However, a dynamically-checked program which contains type assertions still tends to be very effective at detecting type errors even as the tests get out of date, except, of course, in code which just isn't covered at all by tests. But in that case, the code could as well fail for other reasons, even if it were statically checked. The classic argument goes: you've gotta test anyway, and in the process of testing, you catch a large majority of type errors, particularly if you're paying some attention to types.

For quick and dirty solutions this may be OK, but if you want to maintain it long term, not so much.

That's an overstatement. Again, there are plenty of real, reliable, non-quick-and-dirty systems out there, implemented in dynamic languages.

That can be mitigated by good practices, including type assertions. The TDD movement has gone some way towards methodologizing this kind of thing.

I'm not saying you can't mitigate the risk otherwise, just that type gives you a cheap and easy way to do it simply and reliably.

Another benefit of type that improves the effectiveness of TDD is the assistance it provides for refactoring (the thing that distinguishes TDD for merely having automated testing).

It is MUCH easier to do major refactorings in complex systems if you can rely on your IDE and other tools to be able to find all uses of a given type to decide how and where you need to refactor. Even putting type assertions EVERYWHERE they apply won't give you the same power, and it would cost a lot more.

Again, there are plenty of real, reliable, non-quick-and-dirty systems out there, implemented in dynamic languages.

This says nothing about their maintainability: how well do they tolerate change over time by people other than those that built it or have learned all its quirks.

Again, my argument isn't "dynamic" can't build working systems, or that testing isn't good (I'm a committed TDDer myself).

It is rather that type and testing are BOTH needed to get the biggest bang for your reliability and maintainability buck. They ultimately solve different problems of verification and together they are worth much more than the sum of their parts.

Either one alone is good, but nowhere near as good for as little time and effort cost as the two working together.

I agree. Why does everything have to be a silver bullet?

There seems to be some innate human desire to wrap things up in a single abstraction. A system with two abstractions, to many, seems to be incomplete... I have no why this is.

What's one of the fundamental PLT principles we all learned as undergraduates? The Zero-One-Infinity principle. Of course, that rule primarily speaks to the cardinality of (possibly) parameterizeable features in a programming language (i.e. it's a questionable design to allow pairs but not triples)...but many extrapolate it to mean that everything must be an object (or whatever their pet abstraction is).

A lot of bad designs, I suspect, have been motivated by this phenomenon.

[Note: URL fixed]

It is rather that type and testing are BOTH needed to get the biggest bang for your reliability and maintainability buck.

That's true, as long as you recognize that "type" is also exploited in dynamically checked systems, albeit in different ways. What I've been getting at hasn't been about types vs. testing, but about the fact that in dynamically-checked systems, testing, in conjunction with type assertions, can provide a good enough equivalent, in many cases, to static checking of types.

It is MUCH easier to do major refactorings in complex systems if you can rely on your IDE and other tools to be able to find all uses of a given type to decide how and where you need to refactor.

You would think so, although Smalltalk programmers have claimed that their refactoring browsers do a fine job of this, without static types. I don't know how they work, but I imagine those browsers are performing some kind of static reasoning, beyond simple string searches. Even if they aren't, my point here is that static reasoning doesn't necessarily require that every term in every program have its type be automatically statically identifiable.

[The existence of reliable dynamic systems] says nothing about their maintainability: how well do they tolerate change over time by people other than those that built it or have learned all its quirks.

Static information in the source code is just as important in either the dynamic or statically checked scenario. In a good dynamic system, containing type assertions or even just type comments (an approach which HtDP promotes), I don't believe there's a significant maintainability difference overall. [Edit: that's partly because the various pros and cons of the approaches roughly seem to balance out.] If anything, my experience is that statically-checked languages tend to result in less flexible programs that are more difficult to change, and thus less maintainable.

Automatic static checking focuses on the ability of tools to extract, prove and enforce static program properties. Most current tools in this area require a great deal of well-defined static information to be present in the program, otherwise they don't work at all. Programs that don't provide sufficient static information to support these tools may still contain a great deal of static information which is apparent to a human reader, and can be exercised and exploited in conjunction with testing, reflection, and so on.

What do you have to say about this, Peter?

Touché, since I am on the program committee! One could say that these features were originally explored in "dynamic" languages (mainly Lisp, in the golden 60s and 70s) and then made their way into other languages (including "static" languages). I agree that the CFP is a bit on the woolly side. But I look at this conference mainly as a way for people from different communities to come together and exchange ideas.

In the case of Python, a test like type('foo') == type(x) does catch type errors, but not at compile time (Python doesn't really have a compile time).

Unit testing in Python does not even begin to make up for Haskell's lovely type system. But, test driven development will usually catch the totally broken code paths that I occasionally find.


PS. I would like to hear about other benefits of static typing.

--Shae Erisson - ScannedInAvian.com

Static type-checking in Camelot guarantees RAM usage -- not only its safety but also its amount.

Static type-checking in my controlled pi-calculus (definitely not a real programming language) guarantees statically properties of access control ("only X can use the printer", "I can only read this information for the purpose of transferring it to you", ...) or resource management ("this program will never require more than x threads, y RAM and z printers").

Static type-checking in TyPiCal guarantees the respect of some protocols. In Acute, you can check the safety of communications...

Is this convincing enough ?

Yes, thanks for these pointers on the benefits of static typing outside of program safety. Likely I can find more examples in the references of the papers describing these.

--Shae Erisson - ScannedInAvian.com

Python has no runtime representation of types. Asking for a type of something actually returns it's class, i.e. how it's type is implemented. The actual type of an object is however it responds when you call its methods.

In practice, you want to test what an object does, not test which actual class provides its implementation. The class is an implementation detail and testing for it will make tests so brittle as to be impractical.

The "dynamic language" response to TyPiCal, Flow Caml, and Acute seems to be, quite literally, "you and your users don't need it."

All of these things are research projects and/or prototypes. A big advantage of dynamic languages historically is that they've made it possible to practically deploy many advanced ideas before they've been successfully cast in statically-checked concrete. Lisp, Smalltalk and Forth did things that you couldn't do with their predecessors and contemporaries such as FORTRAN, COBOL, and Simula. The former three dynamic languages have stood the test of time much better than their static counterparts. That in itself says something about the benefits of dynamic languages.

On points like "interactive, incremental development" and "hot replacement of running code", the best dynamic languages still have an edge over the best static languages which support such features. The "expressive magic" which dynamic languages support is easy to demonstrate -- there's no mystery about it. Sure, it's modulo Turing completeness, but embedding a dynamically checked system within a static one is a hack at best, and has a clear expressivity cost.

And if we're going to be discussing the future, then let's look at type inferencing for dynamic languages, like MrFlow. There's a version of that built into current versions of DrScheme [edit: versions in CVS, that is]. Based on the history, I wouldn't be surprised to see some of the future features you're concerned about becoming available in dynamic languages, in some form. For example, dynamic languages often have static qualities when it comes to linking modules, i.e. they'll report missing symbols prior to runtime. There's nothing wrong with some appropriate mixing of features — it isn't necessarily the case that to achieve certain static benefits, we'll need to statically determine the type of every term in a program.

Existing statically typed languages still tend to trip up over some very basic issues. We discussed one the other day: numeric handling. Haskell, ML and OCaml all have serious issues when it comes to doing ordinary calculations of the kind done in many ordinary commercial programs. Simple arithmetic involving more than one type of number is a minefield of type conversions and type errors which, from the perspective of many applications, are utterly pointless. I think you'll be able to start declaring victory for static languages when some of these basics have been dealt with satisfactorily in actual, available languages.

Until then, we should at least be realistic and acknowledge that (a) there's still a tradeoff between dynamic and static, and different tasks have different requirements which may affect the choice; and (b) that dynamic languages continue to serve a very valuable role in the language space, and are likely to do so for a long time to come.

I'll state for the record that I don't like what I see as a false dichotomy in the static/dynamic debate — what I'm really looking forward to in the future is a more sophisticated attitude towards types from both camps. Dynamic advocates who see absolutely no benefit to static checks are missing the fact that the programs they write are full of static types which they actually reason about, even if they don't realize it; but static advocates who think that a universal type encapsulates everything there is to know about dynamic languages are, funnily enough, missing the exact same point.

Types exist, ignoring them doesn't help, but that doesn't mean that we need to statically identify the type of every term in every program.

See SoftTyping for an interesting halfway point.

Where the type checker can prove that the program is type safe, all is fine and dandy. Where the type checker can't prove correctness it informs the programmer and inserts appropriate type checks, but doesn't reject the program

Can you elaborate on this ?

Factor (factor.sf.net) will have this, essentially, once type inference is more mature. Factor is dynamically typed but its compiler uses stack depth inference and type inference. These are intended for optimization, mostly, and usually incremental development with lots of testing works out better, but Factor will still reject mistyped programs as a side effect of the compiler. BTW, Slava (Factor's creator) says Factor's a dynamic language, but I hate the term.

Simple arithmetic involving more than one type of number is a minefield of type conversions and type errors which, from the perspective of many applications, are utterly pointless.

I think this tells us more about the fuzziness of our notions of "simple arithmetic" rather than problems with static typing.

I think it is a strength of explicit coversion between numeric types that it brings issues around this fuzziness out into the open.

If you don't understand how these conversions are made explicitly, you probably don't understand how they work implicitly in a "dynamic" setting, and you WILL shoot yourself in the foot post haste when you try to do non-trivial numerical computation.

More specifically, numerical analysis (in the general case) isn't simple. Far too many people try to equate numerical analysis with simple (heh) symbolic manipulation, and get the wrong answer as a result.

We're all aware of the following common numerical bug:

 for (double d = 0.0; d != 1.0; d += 0.1)
 {
     // do something
 }

On many platforms, this will run forever; depending on how double is implemented (IEEE 754 implementations generally won't terminate). Some blame the programming language for providing "approximate" types like double; others blame the IEEE spec itself for not being decimal-friendly.

But the problem is more fundamental than that, and not likely to be fixed by any tools of type theory. For certain applications (such as finance), there are reasonable solutions (like use of base-10 floating point, or use of rationals rather than floats)--but these solutions are known to be just as bad in the general case (still producing wrong answers, and/or increasing the time complexity of the algorithm).

I think this tells us more about the fuzziness of our notions of "simple arithmetic" rather than problems with static typing.

If you don't understand how these conversions are made explicitly, you probably don't understand how they work implicitly in a "dynamic" setting, and you WILL shoot yourself in the foot post haste when you try to do non-trivial numerical computation.

A large proportion of the numerical computations performed in commercial programs probably qualify as trivial in the sense you're thinking of. I'm saying that fine static type distinctions don't make much sense in that context, and their lack doesn't lead to foot-shooting.

Scott Johnson wrote:

More specifically, numerical analysis (in the general case) isn't simple.

Right, it's the general case that's the problem. The examples I'm thinking of are financial applications. Certainly, static languages have an "excuse" for their issues in that area. However, there are ways to address those issues, including by dealing with types differently. The dynamic languages may take an easy way out, but it works well.

This goes back to my point that dynamic languages make it easy to implement things that take much longer to get right statically. IMO, static languages have a ways to go in this area.

It's not as bad as all that. You know what people like about "dynamic languages." If someone produces a statically typed language with the same feel then I'm sure it will be welcomed as a "dynamic language." If this can really be done then it will be great fun when the static typing guys come and join the party :-)

...I think Haskell has the nicest story for number handling of any programming language I've ever seen, bar none. Making numeric literals members part of a typeclass lets the programmer overload literal numbers in a very flexible and clean way.

I've also been wondering how Haskell's typeclass hierarchy is different from Scheme's numeric towers, so I used the smart half of my brain (google) to read up on Scheme's towers before saying something uninformed.

I looked at R5RS Numerical Types, and it looks like the same thing as in Haskell. Am I missing a difference because I haven't tried to use the Scheme numeric towers?

--Shae Erisson - ScannedInAvian.com

I suppose one obvious difference is the automatic type coersion performed by scheme...

guile> (integer? (* (sqrt 2) 0))
#t

...whereas...

GHCi> :t (sqrt 2) * 0
(sqrt 2) * 0 :: (Floating a) => a

foo x = (x,y,z) where y = x ** (1/4); z = take x [4,5,6]

No instance for (Floating Int)
arising from use of `**' at :1
In the definition of `y': x ** (1 / 3)

There are, of course, ways to fix this, but in general they're messy. For example, 'x' is required by 'take' to be an Int, so the problem isn't directly fixed by using e.g. (fromInteger x) ** (1/4). However, declaring x as Int still requires a conversion for use with '**'.

Having to do explicit type conversions is not necessarily a big deal in general — they're par for the course in C++ and Java. But combined with type inferencing and the various numeric types, it seems to get particularly messy. This is just a simple example of the issue — in real code, it's less simple.

In Scheme, you write:

(define (foo x)
  (let ((y (expt x 1/3))
        (z (take (list 4 5 6) x)))
    (list x y z)))

...then you know were to find it. But typeful language usually require explicit conversions on purpose. Sure it would be no problem to collapse all numeric types into one (that's what Miranda did, IIRC), but the sentiment in the types camp is that relying on implicit conversions that are partial, such as say, float to int, begs for trouble.

This sentiment even exists in parts of the dynamic world - not all dynamic languages will happily perform such conversions. Oz is one example.

Sure it would be no problem to collapse all numeric types into one (that's what Miranda did, IIRC), but the sentiment in the types camp is that relying on implicit conversions that are partial, such as say, float to int, begs for trouble.

I think the "sentiment in the types camp" is not based on the kinds of requirements that arise in a lot of real-world programming with numbers. I suspect that if/when some of these languages move further into the mainstream, you'll see different sentiments being expressed.

What is (take (list 4 5 6) x) if x = 1.5 ? Always ?

What is (take (list 4 5 6) (* 3.0 (/ 1.0 3.0))) ? Mh, dependent on the machine and its floating point representation, precision, rounding mode?

In the program in question, as I mentioned, x is an ordinal and is always an integer. That can be checked in various ways if you don't trust that the program has been written correctly. It would be great if it could be automatically checked statically, but the point I'm making is that with most current static languages, that's like pulling on a thread which winds its way through every numeric calculation in a program, and you end up paying a price in many of those calculations. As I mentioned, it's a tradeoff.

foo x = (x,y,z) where y = x ** (1/4); z = take x [4,5,6]

Assume the programmer knows that x is constrained to be an integer
.... However, in the above, Haskell infers it as Double, because of
the way it's used in the calculation of y. Without giving Haskell any
other hints, this leads to a failure ... There are, of course, ways to
fix this, but in general they're messy. For example, 'x' is required
by 'take' to be an Int, so the problem isn't directly fixed by using
e.g. (fromInteger x) ** (1/4). However, declaring x as Int still
requires a conversion for use with '**'.

If one wishes for an analogue of Scheme's expt in Haskell, one can easily obtain that:

{-# OPTIONS -fglasgow-exts #-}
module Foo where

import Prelude hiding ((**))
import qualified Prelude ((**))

class (Floating b) => Expt a b where (**)::  a -> b -> b
instance Expt Float Float   where (**) = (Prelude.**)
instance Expt Double Double where (**) = (Prelude.**)
instance (Floating b) => Expt Int b where 
    x ** p = (Prelude.**) (fromInteger (toInteger x)) p

foo x = (x,y,z) where y = x ** (1/4); z = take x [4,5,6]

(define (##expt x y)

  (define (type-error)
    (##trap-check-number 'expt x y))

  (define (exact-int-expt x y) ; y >= 0
    skipped)

  (define (real-expt x y) ; y > 0
    (if (##zero? y)
      (if (##eq? y 0) 1 (inexact-+1))
      (if (##zero? x)
        (if (##eq? x 0) 0 (inexact-0))
        (complex-expt x y))))

  (define (complex-expt x y)
    (##exp (##* (##log x) y)))

  (define (invert z)
    (let ((result (##/ 1 z)))
      (if (##not result)
        (##trap-check-range 'expt x y)
        result)))

  (if (##complex? x)
    (number-dispatch y (type-error)
      (if (and (##flonum? x) (##flonum.nan? x))
        x
        (if (##fixnum.negative? y)
          (invert (exact-int-expt x (##negate y)))
          (exact-int-expt x y)))
      (if (and (##flonum? x) (##flonum.nan? x))
        x
        (if (bignum-negative? y)
          (invert (exact-int-expt x (##negate y)))
          (exact-int-expt x y)))
      (if (and (##flonum? x) (##flonum.nan? x))
        x
        (if (##negative? (ratnum-numerator y))
          (invert (real-expt x (##negate y)))
          (real-expt x y)))
      (if (and (##flonum? x) (##flonum.nan? x))
        x
        (if (##flonum.nan? y)
          y
          (if (##flonum.negative? y)
            (invert (real-expt x (##flonum.- y)))
            (real-expt x y))))
      (if (and (##flonum? x) (##flonum.nan? x))
        x
        (complex-expt x y)))
    (type-error)))
(define (expt x y) (force-vars (x y) (##expt x y)))

It should be noted that not all Scheme systems implement the full numeric tower (actually, relatively few). It should also be noted that not everybody in Scheme world is happy with the R5RS way of dealing with numbers. Here's the excerpt from the recent R6RS progress report:

A subcommittee was formed with a mandate to propose revisions to the numerical tower to the whole committee. While the full proposal is not yet finished, the subcommittee believes that sets of operations for exact arithmetic and floating-point arithmetic should be separated out. The subcommittee is still debating the semantics of the generic numerical operations...

Regarding Haskell code: one can go further and let the programmer specify conversions rules from one datatype to the other. The function (**) could then be defined, for example, as

(**):: (Convertible a Double, Convertible b Double) =>
 a -> b -> Double

This nicely demonstrates some of Haskell's coolness. However, when I wrote "in general they're messy" about fixes for these kind of problems, part of what I meant was that to solve these kind of problems in general, you would need to rewrite many of Haskell's operations, and not only numeric ones.

For example, I mentioned the issue of 'take' expecting an Int (i.e. a integer 30 or so bits wide) — however, in these sorts of applications it is often necessary to deal with the larger Integer type. That introduces another area which requires type casting for an essentially trivial reason. Division is another issue. The list goes on.

I haven't tried to do an analysis of what would be needed to completely "fix" Haskell for these kinds of things, or whether it's possible at all; my sense is that the general approach is wrong for some applications, that some of these static distinctions are pointless in some contexts.

While the full [Scheme numerics] proposal is not yet finished, the subcommittee believes that sets of operations for exact arithmetic and floating-point arithmetic should be separated out.

I think this is another example of the attitude to numbers which people heavily involved in numerical analysis have. Again, this attitude usually seems to introduces nothing but unnecessary complexity for many applications.

However, even if Scheme does make such a change, there's a sense in which it'll still be better off than Haskell: the change will result in a type error on 'expt', but it will not result in values that ought to be integers being inferred by the language as being floating point values, for example, so the Scheme case would only result in errors at the 'expt' call site, not elsewhere in the code.

The issue here is not just that type conversions are necessary at all, but that the combination of multiple closely related types in the presence of static type inference results in unnecessary complexity for certain ubiquitous applications.

...it's simply a matter of either (a) using the compilers/interpreters complex rules of autocasting; or (b) being explicit in the type conversions. As others have said, I don't think this is an issue of dynamic vs. static, as autoconversion (or lack thereof), can be bolted onto either.

Now, the question would be why more dynamic languages tend to favor autoconversion and more static languages frown on it? The answer from the static side is that these languages are generally geared towards type rigour. If you don't need types in a rigorous sense, then you don't really need a statically typed language?

Personally, I favor even more numeric types wherein you specify the range of any particular number (ala Pascal), though most programs would probably just use the default min-max settings.

(P.S. Should also mention how horribly broken Javascript's autocasting of strings to numbers, and vice versa, is broken. I'd rather they not have done that at all - being a source of constant irritation.)

I agree that the complexity is there in either case, but in the case where autocasting is done transparently and correctly, then it is hidden from the application programmer, which is as it should be unless there's a reason for the application programmer to care.

This is precisely my point: in many cases, there's no reason for the application programmer to care, but existing static languages force them to deal with the issue anyway. I'm not saying statically typed languages can't do a better job of this (by my definition of "better"), but they don't do it right now.

Dynamic languages have an easier time dealing with this because they don't have to do static inference. They're not trying to prove, ahead of time, which terms might fail. They just run the code, and if they hit a mismatch, they generate an error.

My original point was that this is an example of the kind of issue where dynamic languages can effortlessly do something that static languages have a hard time duplicating.

I'm not saying that this means that all programming should be in dynamic languages, just that both approaches have their pros and cons, as balance to the perspective which Paul originally posted. Both sides can learn from each other, too, although not as long as they dismiss the other side as not having anything interesting to offer.

Naked programming on naked street by Sean McGrath. An interesting exercise in reasoning by analogy:

Question:

How do you stop people driving cars in built-up areas from injuring themselves and others?

Obvious answer:

Put in place speeding limits, stop signs, traffic lights and generally as much stuff as you can think of, to control who/what goes where, and when they get there.

Less obvious answer:

Strip out all the traffic controls. Let cars and pedestrians mingle as they like and let it all just sort of work itself out.

Apparently, that's how they solve the problem of traffic control in India. The author claims it works so well, the same method is currently being piloted in a few select European municipalities. If the parallels to the static/dynamic typing debate aren't obvious yet, read the entire piece.

An interesting comparison, but is the analogy even close? Both of the cases given seem more like dynamic checking — drivers drive until they see either a sign or, say, a donkey, at which point they perform the appropriate action. In both cases, you're depending on reactions and decisions "at runtime".

Static checking for traffic would involve a phase prior to actually driving, which would reduce the need to watch for signs or donkeys en route.

Perhaps a better analogy might be along the lines that with static checking, you only drive on predefined, paved roads, whereas with dynamic checking, you're in an all-terrain vehicle and you can cut across country to get somewhere, although you run the risk of hitting rocks or ditches along the way.

Naked programming on naked street by Sean McGrath

What a terrible piece!

In Mumbai, traffic is so heavy and congested, you can't possibly go fast enough to be likely to have a fender bender!

With more wide open space, people are used to moving fast and as they please, and then have to make quick or unexpected shifts of thinking when they hit heavier traffic. No wonder you have more accidents.

If the author were willing to draw the analogy to what this would mean for programming, I might respect his conclusions more.

There are, of course, ways to fix this, but in general they're messy. For example, 'x' is required by 'take' to be an Int, so the problem isn't directly fixed by using e.g. (fromInteger x) ** (1/4). However, declaring x as Int still requires a conversion for use with '**'.

Yes, fromInteger wouldn't work, but that's what fromIntegral :: (Integral α, Num β) ⇒ α → β is for.

I gave this code to GHC,

foo x = (x,y,z) where y = fromIntegral x ** y; z = take x [4,5,6]

and it inferred the type (Floating α, Num β) ⇒ Int → (Int,α,[β]).

Less elegantly, we can use genericTake from Data.List:

bar x = (x,y,z) where y = fromIntegral x ** (1/4); z = genericTake x [4,5,6]

Now the inferred type is (Floating α, Num β, Integral γ) ⇒ γ → (γ,α,[β]).

Thanks. That looks like the right solution in this specific case.

I'll risk a bit more pounding on the horse, though, because I don't think the fixability of the example is really the issue. The general point is that getting this right requires care on each term (in principle), and getting it wrong can result in indirect errors elsewhere, with values not being the expected type. Also, getting it right requires dealing with a larger set of operators that only exist because of static type distinctions.

This sort of thing actually ends up being less surprising in a non-inferencing static language, like C++ or Java, because then inferencing can't introduce errors. Part of the issue I'm raising is that inferencing is introducing its own tricky class of errors here -- instead of reporting operator mismatches as type errors at the site of the problem, the inferencing system can jump to the wrong conclusion and contaminate the types in other parts of the program.

One way to mitigate this is to declare the expected types, of course, which is ultimately a good idea anyway, for reasons of redundancy, documentation, etc. However, having to do that as a matter of course just to avoid what in some situations are spurious errors, brings the inferencing languages down to the level of a C++ or Java in terms of the overhead for dealing with types.

I'm very aware that one class of answers to all of this is just to suck it up and deal with the types, in exchange for all those wonderful static guarantees. However, this could be made more automatic in at least some widely-used contexts. At the very least, dynamic languages provide a competing approach so that the static languages can't get away with saying "sorry, that's impossible".

Perhaps I should be posting this to the Links thread so Philip Wadler can take care of it. :)

Something tells me that the class of errors that you are speaking involve are in the compile phase? I personally prefer dealing with errors during the compile phase, as I can always try to work with the type system. Run time errors are a bit sneakier in terms of when they are noticed.

Yes, these are compile errors. But remember, these are errors which don't actually need to be errors at all — essentially, for some applications at least, they're artificial errors.

Re the timing of noticing runtime errors, see my other post, "The unreasonable effectiveness of testing".

In contrast, extensive use of external XML configuration and metaprogramming means that my source code loses the information to reason about what will happen at compute-time, and there are fewer "bad things" that I can rule out by inspecting the source code.

...

Does anyone else find this different way to slice the pie illuminating, or at least an interesting reframing of the issues?

I've seen this line of reasoning pop up in quite a few places lately. (Maybe it's simply because it's come to the forefront of my conscious attention. Kinda like learning a new word — you start seeing it everywhere once you've learned it.)

A couple of examples. My coworker graydon (of One-Day Compilers fame, among other things) expressed it thusly:

I have an ongoing thesis at the moment which I'm exploring in the programming language literature, which is that programming language features do well (all other things being equal) when they eliminate either distant or dynamic state and replace it with either close or lexical state. the underlying point being that we may favour language features that facilitate copying and modifying small bits of code — which work in their new context — a fundamental programming activity.

A central issue in the recent AOP considered harmful debate was the issue of reasoning about code fragments on a local level. Here's how Jonathan Aldrich put it:

AOP *does* make it easier to understand and evolve a concern that *crosscuts* an ordinary OO decomposition--and it does so even without tool support.

However, without tool support, AOP makes it harder to understand and evolve *base* code, for the reason that everyone cites: you can't see which aspects apply to it, and so you can't tell what's going on, and if you edit the code you might break the aspects.

(This post is also interesting.)

Somewhat along the same lines: http://calculist.blogspot.com/2005/04/balance-of-expressiveness-and.html.

I've seen this line of reasoning pop up in quite a few places lately.

I think your examples are similar to where I'm coming from, though I think that global/local modularity is only one component (though an important one) program-time (or edit-time) reasoning. For example, clarity (lack of ambiguity) and explicitness apply even within a module.

Even on the particular issue of modularity, I've been wondering quite a bit about different kinds and degrees of modularity, for example the difference between two objects running in the same VM that are modular with respect to each other, versus the modularity between different nodes on a distributed network of computation.

Joel refers to this as code collocation.

So yes, some people cut it not at the compile time, but at the edit time. I think the main reason this is not so widely accepted because in popular languages edit-time tools are a bit less type-oriented than compilers - but I may be wrong about this.

I usually prefer to see it as "edit time"

That term has some merits, though I think it obscures what the key activity is with respect to source: reasoning.

You may or may not be editing the code, but when you read source (code or model) your are reasoning about what the system it defines will do once you hand it off to the computer.

I think the main reason this is not so widely accepted because in popular languages edit-time tools are a bit less type-oriented than compilers

I think it has more to do with the fact that "program-time" or "edit-time" is a human process. ;-) We are more comfortable debating between two computational processes (compiling and executing).

But my search for formalizable "human factors" goes on, and I think I'm starting to get close with the notion of "reasoning via source code" (my definition of programming) as mappings with certain properties to and from semantic models.

is a function of how intelligent your editor is. If you edit in vi (like I like to do, luddite that I am :)), your edit-time analyses are probably limited.

However, an editor which has the compiler integrated, can (conceivably) do any analyses which the compiler itself can due. A practical limitation is response time--it wouldn't be a good thing if every keystroke required a full compile before the next one--but modern IDEs are quite good at this.

The important phase distinction remains at the point where the code starts "running"--in other words, when the behavior of the program starts depending on the user input, environment of deployment, or other factors beyond the control of the programmer.

I'm surprised that the editors are still not as intelligent as they could be on modern hardware.

In circuit design the interactive tools are pretty heavy. I am a programmer on a 3Ghz machine with 1Gb of RAM. My development enviroment should use 80+% of CPU and use up hundreds of Mb's to assist me as much as possible while I am editing.

Fully agreed. It always makes me wonder how we (programmers) can come up with 3D environments for biologists so that they can do modelling of molecules (or environments for engineers designing circuits etc.), while *our own* development tools are typically very low-level tools. Compared to the Lisp and Smalltalk environments of about 30 years ago we have made very little progress in that respect.

A 3D environment for a biologist is simple, in the sense that it merely has to provide a nice virtual model of physical objects like molecules. The environments for circuit designers are similar: the problem they solve mainly relates to generating and modelling the physical layout of circuits. How much do those tools help with the original logic expressed in languages like VHDL?

Dijkstra claimed that programming is one of the most difficult branches of applied mathematics. I think that has a lot to do with the lack of tools that can simplify the activity.

The difference between edit-time and compile-time is a function of how intelligent your editor is

Scott has just demonstrated that my concern about the term "edit-time" was justified. ;-)

If your "editor" does the kind of checks that we normally expect a compiler to do, it is still part of the "compute-time" phase, in my scheme.

With the term "programming-time" I'm interested in capturing the reasoning (done by the programmer) that is possible about the behaviour of a computation solely from inspecting the source code (or source diagram).

I think the characteristics of this reasoning can be formalized by talking about mappings from the source code (as accessible to the programmer) into various semantic models of the program, and then from these models to the observable behaviour of a computing machine.

Above, you (Marc) wrote:

The normal static vs. dynamic discussion usually makes the dividing line between compile-time properties and run-time properties, and I'm beginning to think that this isn't actually the interesting dividing line. (Not inconsequential, just not as interesting.)

For me, the interesting line is starting to be between what I'll call program-time and compute-time: what information can be reasoned about directly in the source code, versus what will happen once the computer takes over (compiling and executing).

Even with primitive editors like "vi" or "notepad", the computer is involved, at some extent--unless you write code in longhand, I suppose. Ignoring pen and paper, the computer "takes over" as soon as you start typing your code in.

How much the editing software assists you depends on the software; however a sufficiently smart editing program/IDE can do anything that a compiler can do. And no more. Any program analysis or transformation that can be performed by the compiler can be performed by your editor; the simple proof is that the editor can invoke the compiler in the background and examine its output. Anything that isn't available to the compiler (such as determining if an arbitrary pointer will ever be NULL, a problem known to be undecideable via static analysis) is also out of reach of your editor.

So, I stand by my remark that that it makes little sense to distinguish "compile time" from "edit time".

Run time, of course, is a different kettle of fish, as analyses which are undecideable at compile-time become possible. In general, undecideable-at-compile-time analyses (as well as decideable-but-intractable ones) have to be dealt with in the following ways (or some combination):

* Ignoring them.
* Performing "best-effort" analysis--attempting to find an answer, but giving up if it takes "too long".
* Only accepting a subset of programs which are amenable to such analysis (ie strong static type systems)
* Instrumenting the generated code so they are verified at runtime, at each instance the construct in question is encountered--for example, dynamic typing or bounds-checking
** Doing so in hardware--for example, depending on the MMU or ALU to check invalid pointers or division by zero

Note that several of the above possibilities defer the analysis to program execution--changing an undecideable question ("will this pointer ever be NULL?") to a trivial one ("Is this pointer, at this instant in time, NULL?"). To do so requires that the program actually BE executed; and the result of one execution won't (in general) say anything about the results of a different execution of the program, with different input data and such.

(Of course, there's always the technique of arranging for several trial executions of the program/module, with different input datasets, chosen strategically and/or randomly, with the goal of probablistically exposing any possible defects. Unit testing, as it's called...)

Admittedly, there are lots of other complicating factors, such as environments which do program transformations at program load time (ie .NET) or even while the program is running (any JIT compiler). Currently, most production examples runtime program transformation is done for reasons of performance--chaning slow bytecode into fast(er) machine code, etc. The Java bytecode verifier is one example of a runtime environment that does program analysis at load-time for correctness reasons. However, the analyses performed by the bytecode verifier can be done (and are done) without running the program (and certainly could be performed by a Java IDE).

If we take your paragraph above, and replace "compiling and executing" with just "executing", then I'll be in complete agreement with you. Execution is the boundary where the phase distinction ought to occur, as it's the point where variance beyond the programmer's control begins.

So, I stand by my remark that that it makes little sense to distinguish "compile time" from "edit time".

In the sense that you mean "edit time", I agree. Remember "edit time" is Andris' term as a synonym for what I was talking about.

What I was talking about has nothing to do with the power of the editor or the act of editing per se, which is why I wasn't crazy about its usage. (The confusion we have already had about this bears that misgiving out. ;-) )

I prefer the term "programming-time" or "reasoning-time" (a better term may be forthcoming) for what I meant, which is all about the programmer's understanding of the program, "how it runs in the programmer's head", if you will.

If we take your paragraph above, and replace "compiling and executing" with just "executing", then I'll be in complete agreement with you.

Doesn't that just take us back to "static" vs. "dynamic"?

"A Priori time" anyone?

Do you mean, everyone should explain their assumptions before we proceed, Ehud?

I'm starting to think no one is actually reading what I've posted, or else I've accidentally posted in a language even I don't understand. ;-)

You are too revolutionary for us...

Of course, the "vs" in the phrase "static vs dynamic" is unfortunate, as it has lead to far too many unproductive (if not counter-productive) flamewars as to which is better.

At any rate, your remark about the analyses performed by programmers "in their head" leads back to the discussion a while back on computer-generated proofs. Much as a mathematician is able to "construct" proofs (or approximations thereof!) of non-trivial propositions in systems where brute force theorem-proving is WAY undecideable :), via heuristically knowing which infinite number of cases to ignore--programmers (good ones) can do the same thing.

Those of us who program in C/C++ for a living often write code containing potentially unsafe casts, which we "know" is type-safe (but cannot be written in C/C++ without a cast), because we have "proven" it to ourselves in our mind. Likewise, we "prove" to ourselves that array operations will stay in-bounds; that pointers won't be NULL, etc. We develop these proofs using various heuristic techniques that are common nature to us, but excruciatingly difficult to describe to the computer.

Of course, we're frequently wrong about such matters, which is why we a) test the hell out of our code, b) use languages which automatically insert runtime checks (and fail in a controlled fashion), c) use assertions and other explicit runtime checks when the language doesn't do them implicitly for us, or d) use more powerful formal methods (i.e. languages with stronger typing systems) to make machine proof tractable. Obviously, d) isn't always available--many problems being undecideable, so we're left with a, b, and c in those cases.

And of course, far too many programmers do e), which is ignore the issue and hope they're right--but I think we all agree that e) is not a good solution to this problem.

At any rate, I think we're in non-violent agreement on pretty much all important points here.

The normal static vs. dynamic discussion usually makes the dividing line between compile-time properties and run-time properties, and I'm beginning to think that this isn't actually the interesting dividing line. (Not inconsequential, just not as interesting.)

For me, the interesting line is starting to be between what I'll call program-time and compute-time: what information can be reasoned about directly in the source code, versus what will happen once the computer takes over (compiling and executing).

In the usual academic usage of "static" and "dynamic", static refers to properties of programs that can be determined and reasoned about without running the program, and dynamic refers to things that happens when the program is running. These definitions seem to correspond exactly to your "program time" and "compute time" distinctions.

The association of "static" with "compile-time" is because compile-time analyses are, of course, static. That doesn't mean that all static information is dealt with at compile time, and it doesn't mean that there isn't useful static information [edit: including types] in dynamically-checked languages, for example.

With this distinction, I now realize that what I really favour is maximizing program-time reasoning (whether static or dynamic in the conventional sense), and minimizing the use of intervening compute-time intervention that obscures such reasoning.

So metaprogramming, in all its flavours, is solidly a "compute-time" feature.

In the usual academic usage of "static" and "dynamic", static refers to properties of programs that can be determined and reasoned about without running the program, and dynamic refers to things that happens when the program is running. These definitions seem to correspond exactly to your "program time" and "compute time" distinctions.

The key distinction here is "when the program is running". Normally, this line is drawn AFTER compile time, so that, for example, a type-cast exception is dynamic, but a compiler typing error is static.

I want to draw the line BEFORE compile-time so that both types of type-checking are grouped together.

The proprerty I want to promote is that the programmer can predict by inspecting the source code that certain types of unsafe operations will not occur (wherever they will be ruled out in the compile-execute chain).

So, in my scheme, certain extreme forms of static type-inference where it was very hard to predict what the type-checker would rule out would group together with a situation where there was no static type checking at all, and the dynamic type was dependent on unspecified implementational details "under the hood".

...is difficult to reason about formally, unfortunately.

But I'll bite (further). By "inspecting the source code", how much source do you mean?

Are we talking stuff that fits on the screen? The current module, plus the transitive closure of its dependencies? Entire programs? Every line of code for every program which might run on a system?

One area which programmers are (alledgedly) better than machines is certain "whole program" optimizations/analyses--this is especially true in environments where incremental compilation is performed and the machine might not have the whole program available. Some key functionality might be in a DLL that's dynamically loaded, and might not even be installed. Humans, it is claimed, can understand the program as a whole where the machine only sees a chunk of it as a time. Humans might be able to make assumptions (like only module foo will call function bar) that the compiler won't (as bar is publicly exported, thus anyone might call it).

But to repeat the drum I've been beating furiously in this thread (or is it a dead horse? Or a drum maid out of the hide of a dead horse?), humans are notoriously unreliable in this regard. Assumptions change, and the maintenance programmer who comes along might not know that correction functioning of the program depends on some unspecified invariant remaining true.

This is, of course, one of the advantages for manifest typing, contracts and assertions, unit tests, function prototypes, const, protection mechanisms (public/private), and other ways of explicitly stating invariants--invariants specified in these fashions can be checked by the development environment and/or the running code. Even if the checking is dynamic (and thus not guaranteed), it still beats a note in the comments, or in the ISO-compliant design docs that nobody bothers to read.

What the programmer can predict is difficult to reason about formally, unfortunately.

This is a key problem I'm trying to reduce down to size.

I have an approach I've been working on for some time based on normal CT and semantic modelling ideas, that I have been trying to write up.

I was hoping to test drive some of the ideas here, but apparently I haven't got things "bite-sized" yet. ;-)

By "inspecting the source code", how much source do you mean?

I think this is a very interesting question. It gets at the heart of what we mean by modularity and compositionality.

At whatever "size of source code chunks", I want the "prediction property" to operate and to respect modularity and compositionality, i.e. composing two chunks of the "same size" should combine them in a sensible way, and I shouldn't have to drop into the internals to figure out what the interaction will do.

Again, I think we can go a long way to formalizing this, and I'll just have to try harder to unpack it all and write it up. ;-)

The property I want to promote is that the programmer can predict by inspecting the source code that certain types of unsafe operations will not occur (wherever they will be ruled out in the compile-execute chain).

So, in my scheme, certain extreme forms of static type-inference where it was very hard to predict what the type-checker would rule out would group together with a situation where there was no static type checking at all, and the dynamic type was dependent on unspecified implementational details "under the hood".

Still trying to confirm my understanding: are you making a distinction here between whether a human programmer can predict something statically (i.e. by source code inspection), vs. whether an automated tool like a type checker can predict it?

In both cases, static reasoning is occurring, about static properties (by the usual definitions). The difference is whether it's automated or not. Also, if it's not automated, chances are good it doesn't rise to the level of proof (not that manual proofs aren't possible in principle, they just aren't usually done).

I'll refrain from further comment until I'm sure I understand the distinction being made.

Let me give you an example that is uniformly "dynamic" in the normal sense but that contrasts code that can be reasoned about and code that can't in the sense that interests me.

Let's start with a Python snippet (about as complex as my Python skills allow ;-))

def foo ( o )
    return o.doSomething(1)

Does this function make sense? What will it do? I have absolutely nothing to go on.

Now if I add dynamic checks to this function to test some facts about the parameter and to test the output range, I can create invariants that allow me to become confident that for all possible inputs there is a reasonable output. As you pointed out earlier in the thread, my confidence can be as great as if these things were statically checked.

In this latter scenario, even though I have not used any statically checked guarantees in the normal sense, I have nonetheless ensured that I can reason about my function, I can modularize it and compose it with other functions without having to worry that some bizzare, completely unconsidered outcome will arise upon execution, even if what is fed to my method at runtime is a totally new object whose source I will never see.

Do you still consider this "static" just because I can reason about what will happen from inspecting the source code?

If so, it would seem that we have competing versions of "static" running around. (All the more reason to stop worrying about the contrast and find a better model. ;-) )

Do you still consider this "static" just because I can reason about what will happen from inspecting the source code?

If so, it would seem that we have competing versions of "static" running around. (All the more reason to stop worrying about the contrast and find a better model. ;-) )

The word "static" alone isn't sufficient to capture the various concepts we're dealing with, which is why we have terms like "static property", "static reasoning", "static checking", and the equivalents for "dynamic".

Forgive me if I get too pedantic here, but I want to be clear since we definitely seem to have some terminology issues.

A static property is a property of the program which can be determined without running the program. It doesn't matter whether a compiler or some other tool checks for it.

A dynamic property is a property of a program which can only be determined (in general) by running that program.

In your Python example, the original function has very few static properties. Then you add those dynamic checks. They're called dynamic checks because they only execute at runtime. However, their presence in the program may add static properties to the program, even if those properties aren't automatically checked statically.

For example, in the lines of code after an assertion that a variable x is of type string, the program has the static property that x is of type string, which may in turn imply other static properties. You, as a human reader of the code, can determine these properties by static reasoning, even if no tool does any static checking, and even if a failure of the assertion will only occur dynamically, at runtime.

An additional distinction which we need to make in this discussion is between automated reasoning, done by tools, and manual (human) reasoning. Automated static reasoning is what e.g. typecheckers do. Manual static reasoning is something that humans often do when reasoning about their code — reasoning in the abstract, without actually using specific values to determine results. Dynamic reasoning corresponds to running the program, or at least simulating some aspect of that. Dynamic human reasoning is running the program in your head, e.g. by using specific values for particular inputs to determine results.

(Note that some of the latter terms are not ones I recall having seen in the literature, since you'd usually see terms like "runtime", "evaluation", or "execution" instead of "automated dynamic reasoning"; however, I'm just laying out a consistent grid of combinations of the terms.)

At first I was thinking that your "program-time" corresponded to static reasoning, but on rereading some of the thread, I'm wondering if you're also considering dynamic reasoning by a human to be "program-time". (Automated dynamic reasoning is definitely "compute-time".) IOW, any non-tool-based human reasoning (ignoring the smart editor issue) would be "program-time" reasoning; whereas running the compiler and/or typechecker, running the program itself, or using a debugger is "compute-time", where a tool is being relied on to do the thinking. Am I getting warm?

Am I getting warm?

I think so.

I realized in thinking about our discussion that there is an implicit false analogy in my choice of comparison to "static" and "dynamic".

The problem is that normally we think of static and dynamic as sequential: one is before some dividing line in time or process and the other is after.

The idea I really want to get at is parallel or alternating (this meshes with what Andris is saying I believe.)

(I'll bite the bullet and take a shot at the model I've been pussyfooting around, and see if that clarifies or obscures. ;-) )

We have a human reasoning process that maps source code to a semantic model, and from that model to some observable behaviour (in your terms, the human static and human dynamic processes as a chain).

At the same time or alternatingly, I also pass the same source code through the mapping represented by computer's static and dynamic processes.

I want both mapping paths to map from the same source code to the same observable behaviour . (In CT terms, I want both paths to commute.)

If they don't give the same behaviour, I want to be able to change the source (map from source to source) so that they do. (In CT terms, I want to find an endomorphism on source that is an equalizer of the two mappings)

To add another level of complexity, I can actually have multiple parallel semantic models (e.g. different levels of modularity or abstraction) that I map through on the human side.

In this case, I want each path from source through a given model to commute with the other human paths and with the computational path.

The appeal of this system (for me anyway)) is that all the objects are formalizable (no need to rely on introspection or other messy phenomenological scariness) and all of the interesting properties about them can be evaluated in terms of mappings between them. ( A well-studied and valuable formalism )

In spite of these "limitations", I think it captures a lot of what we mean by the "human factors" or human process of programming.

In particular, I think some ideas about modularity, compositionality, levels of abstraction, required information etc. could be formalized by examining or constraining these mappings further.

If I am following, you are interested in the same kind of properties related to separate compilation, information hiding and locallity of language constructs.

What axioms do we know that can provided by various automated and assisted tools to state what can safely be postulated, what can not be postulated, and what is fuzzy.

I really don't think this line of semantic assistance can be set in concrete terms of sequence. For example, I'd like to know the invariant, pre and post conditions of the procedure being called (be it via formal contracts, in-place assertions, or known test point ranges). I'd like to know what exact assumptions the original programmer was operating in when they wrote the foobar function. I'd like to know the type information that a static compiler can infer, which will help in creating several axioms for reasoning.. I'd like to know the range of test points that the unit tests cover, so that I can make an inference of further axioms.

And even beyond that, I wish I had a large amount of emperical data about the function that could be feed back both from the unit tests and even on into a runtime environment. After all, I should be able to deduce certain truths about all the various stimula that my little function encounters over it's useful life.

And what I really want is not to be swamped with a bunch of formal operational or denotational semantics. I want the tool to weed out all the noise and only provide me with axioms that are useful at my level of aptitude.

Anyhow, without rambling too much further down the labyrinth, I'm not sure that I would discriminate based on the isomorphism provided by the compile/interpret phase. Compilation is just one of many possible programs that can be used to analyze code and/or morph it into another form.

Second, as Marc said, what do you mean by running the program? Is any transformation of program a run? Probably not. Is partial evaluation a run? Ummm... It seems so similar... For some reason I feel we should pay more attention to partial evaluation (or staged computation) when discussing dynamic vs. static.

I agree in principle. However, I think there's a useful distinction that can be made in most cases between the "final runtime" when an end user runs a program, and stages prior to that which are typically performed by the programmer.

In general, the various distinctions I've just laboriously laid out in another post are all relative ones: a property is static or dynamic with respect to one (or more?) computational phases. But in such an environment, everything is relative, including source and object code. You just have to clearly define the phases you're dealing with.

For example, if a programmer does a partial evaluation, providing some inputs to specialize the program, those inputs become static properties of some kind in the target program, although in the source program they're dynamic properties.

You just have to clearly define the phases you're dealing with.

I don't think it's important that a programmer is invloved - imagine an interactive system (meaning it produces some of outputs before accepting some of inputs). Each time it obtains an input, some of previously dynamic properties suddenly become static. Conceptually, is it any different from the system partially evaluating itself after each additional piece of input it gets?

Regarding Marc's notion of program-time, I too have a feeling it has an element of human factor in it. But if this is true, than scope of program-time analysis differs among different programmers. It's like playing chess - in theory, the game is statically analyzable, right? E.g., the winning strategy (from any position, not only the starting one) is a static property. But different players have different opinions about the same position. All of them can statically assert that such or such move is illegal (type-incorrect?) and for very simple positions (terms) they agree what is the outcome (value), but that's mostly it. Are not usual programs much more complex than chess? Advanced chess demonstrated how a pair of computer and human plays better than any of them alone, is not the same true for programming? Cooperative interactive reasoning about programs can be more productive than either offline meditation over a printed out source code or an incredibly complex batch compiler.

I guess it's quite difficult to decypher this brain dump, but the main idea might be that programming (and computing in general) is probably a process, not a function. So static properties are those that you know when it's your turn, and dynamic are those that will become known after the next move of the opponent (which are different from static only in games with infinite choice - for reasoners with unbound finite resources, but can be different even in games with finite choice for reasoners with limited resources - like humans and modern computers are).

Cooperative interactive reasoning about programs can be more productive than either offline meditation over a printed out source code or an incredibly complex batch compiler.

Agreed. I had been going to say something similar but I wanted to be more sure of what Marc was getting at first.

There's obviously a benefit in identifying things which are difficult to reason about, and thus cause problems. The history of programming languages is full of examples of things that have been considered problematic for reasoning — avoidance of mutation is a cornerstone of FP languages for that reason; there have been papers about how metaclasses in Smalltalk were hard for ordinary programmers to reason about; and macros are also often held up as having problems in that area (uh-oh, two "meta" things with problems, I see Marc's ears pricking up... ;)

But it seems to me that these things have to be considered on a case-by-case basis, and it's not clear that a reliance on automated tools, on its own, is necessarily a problem.

So static properties are those that you know when it's your turn, and dynamic are those that will become known after the next move of the opponent

Nice point. For example, in a multi-stage computation, one might reason statically about the output of a computation, but then actually use a tool to generate specific output before reasoning any further about the overall behavior of the system.

So maybe we should think of programming as "partially evaluating the empty program"...? Actually, I'm only partially joking...

Note this paper on pluggable type systems by Gilad Bracha (of Strongtalk fame, and currently with Sun) (http://pico.vub.ac.be/%7Ewdmeuter/RDL04/papers/Bracha.pdf).

I skimmed this paper and at best it's misleading. His thesis, evidence and conclusions are questionable.

"These type systems are widely perceived to enhance software
reliability and security, by mechanically proving program
properties. Paradoxically, such mandatory type systems inhibit
software reliability and security, because they contribute to system
complexity and brittleness.

[advantanges of mandatory typing elided]

"The disadvantages of mandatory typing are not as universally
acknowledged.  Types constrain the expressiveness of the
language. While all major programming languages are Turing-complete,
and so may be considered "equally expressive", the fact is that
a mandatory type system greatly reduces the number of legal programs
that can be expressed in a language."

So he contends a smaller language leads to more complex programs. Given that a larger language has more behaviors which the developer must reason about how is the statically restricted language more complex and brittle?

"Even more importantly, mandatory type systems make systems
brittle. Once a mandatory type system is in place, the temptation to
rely upon it is irresistable.  It becomes a basis for optimizations
and for security guarantees that fail ungracefully if the underlying
assumptions of the type system do not hold.  If the type system fails,
system behavior is completely undefined."

So we need a sound type system, no shocker there.

"Of course, we all know that such type systems should not
fail. A good type system will be formally proven to be sound and
complete. However, real systems tend to be too complex to
formalize. Formalizations make simplifying assumptions.  These
assumptions tend to be make the formal model an inaccurate reflection
of reality, and invalidate any reasoning based on the formal model. In
addition, implementations tend to have bugs, so even the most
carefully vetted type system may fail in practice."

Talk about throwing out the baby with the bathwater! We can formalize languages at least as large as ML. I'm assuming that particles from space won't flip a bit of my computers memory during execution too, but that doesn't invalidate all reasoning about a program.

One small thing I wanted to pick out of this paper is his term of 'mandatory' type systems, which I prefer over 'static' type systems. ...

'mandatory' and 'static' are not comparable. You can have a static non-mandatory type system (imagine MrFlow cast into a type framework).

Well, it's one answer to "Why do they programme in C++?" I guess.