Lambda the Ultimate

I am more convinced than ever that 10 years out we'll see a convergence of the current directions of more expressive, less intrusive type systems and kind of disciplined, test-driven, programming that's catching on now in dynamic programming languages world.

Designing and implementing industrial strength stic type systems (and module languages etc.), that have a dynamic flavour (think type inference, think genericity) is clearly (?) the way to go.

(1) Compare a dynamic object-oriented design and a functional combinator design in some subject area... a beginning to this comparison would be an understanding of objects and combinators. Alongside this would be a comparison of the corresponding tests in say, xUnit and Quickcheck.

(2) Compare how a good dynamic language programmer develops a system of objects for some subject area to how a good functional programmer develops a system of types for the same subject.

The domain could be financial analysis tools. Specific examples that could be drawn from might be Ward Cunningham's Smalltalk-based WyCash and Simon Peyton-Jones' Composing Contracts. A problem: WyCash is proprietary, not owned by Ward, and he's no associated with the owner any more. The two systems are not 1:1, but it would make an interesting comparison.

Not statically typing means that a whole range of errors are removed, however if this comes at the price of larger programs...

More lines of code => More chances to screw-up

Stronger types => Less chances to screw-up

It depends on the type-system in question. The ML type system infers type and basically only rejects things that can't work anyway. Python is untyped, but keeps code simple. Java on the other hand... *shudders*

This isn't something that can be resolved as a matter of principle, horses-for-courses, etc.

If your imagination gets REALLY out there, test-oriented programming languages could be a stepping stone to genetic programs that write themselves. Your code is a black box that is generated by a genetic "compiler" guided by your (exhaustive) test specifications.

Isn't the distinction mainly cultural? I'm sure you could turn dynamic typists into static typists if you used the right words.

• type annotation: interface test script
• type checking: running tests
• type inference: automatic test script generation
• type system soundness: provably complete test set

The main difference is that static typists always run all their interface tests before their other tests, while dynamic typists are a bit lazy about running tests because they say running all those tests takes too much time.

It's a bit like interpreted vs. compiled. I'm sure you could easily sell a compiler to a fan of interpreted languages, when the compiler is fast enough and the tools' interface looks like that of an interpreter. Main thing is to tell them the compiler is an interpreter, otherwise prejudice steps in.

This is a very strong claim which you have so offhandedly made.

On the face of it, there is a world of difference between typing and testing. Typing makes essential use of the structure of programs and, in particular, static typing does not require execution of those programs. Conversely, testing does not require knowledge of the structure of programs, and always executes those programs.

OTOH, getting `full coverage' for a test set would clearly require structural information about the program, and I have wondered sometimes if it isn't possible to engineer a type system which somehow determines a test harness that is guaranteed to exercise every part of the program.

But anyhow, to convince me of any relationship between typing and testing you would have to do some serious formal analysis. It's certainly not just a cultural difference.

Tests can be structural tests. In a dynamic language there usually is reflection so you can do tests that assert things like "this object replies to this message (or this object has a function of such name and arity)" which is a structural test, the test is really a type annotation.

Static typing is a claim of structural soundness, therefore structural tests achieve the same as an incomplete type checker. Static typing is structural testing achieved through the use of formal methods. This leads us to want completeness, which is a difference, but even that is a bit elusive as most type systems in practical use are not formally sound.

testing always executes those programs.

Why not run some tests with a theorem prover? Even with a current C compiler, I guess some simple tests can be proved at compile time. Let's say you write an incrementer:

 int increment (int c) { return c+1; }

 assert (increment (3) = 4);

 assert (3+1 = 4); /* inlining */
 assert (4 = 4); /* partial eval */
 assert (1);
 /* no op */

I'd not be surprised that some C compilers can compile that to:
assert (3+1 = 4); /* inlining */
assert (4 = 4); /* partial eval */
assert (1);
/* no op */

The fact that the C optimizer might be able to eliminate tests that pass does not mean it will be able to generate compile-time notifications for tests that fail. Even if you write the explicit:

assert(0);

you will not get a compile-time notification, at least not on any compiler I'm familiar with. As a result I use the following macro for compile-time assertions for C/C++ :

#define COMPILE_TIME_ASSERT(pred)     switch(0){case 0:case pred:;}

but the compilers I use don't allow me to write:

COMPILE_TIME_ASSERT(increment (3) == 4);

though I don't see a reason why they shouldn't.

Tests can be structural tests. In a dynamic language there usually is reflection so you can do tests that assert things like "this object replies to this message (or this object has a function of such name and arity)" which is a structural test, the test is really a type annotation.

In a dynamic language you can do anything. I think that, in your quest to identify or subsume type-checking with testing, you will enlarge the meaning of `test' so much that it becomes trivial. Is there anything which is not a `test', according to you?

If I can do reflection, then perhaps I can even extract the source code of an implementation via reflection. Then my `test' can try to type-check that source. If you consider that a `test', fine, but I don't. I think this suggests that a reasonable definition of `test' should not allow reflection.

Also, in a way, the ability to do reflection on a program is part of a its interface. Since `testing' should be done w.r.t. an interface, programs which don't support reflection in their interface cannot be tested structurally.

Why not run some tests with a theorem prover?

Sounds sensible to me.

Yes. The main point of presenting type checking as tests is to sell type checking to dynamic typists, who seem to be practical people who are adverse to being introduced directly to formal concepts and whose cult^wphilosophy is centred on testing.

This is true this view brings very little to more formally inclined people, if may be one point: that there may be some excessive balkanisation of concepts and vocabulary in (computer) science, which may leave people working on similar or connected problems from different angles unable or less able to communicate, so sometimes trying to bridge those barriers may be productive, while being careful not to throw away the useful bits of course.