Lambda the Ultimate

Without debating the utility of higher-order type systems either theoretically or practically, I am curious if people think that such systems are perhaps too hard to understand for most programming and/or most people who use programming languages.

These latter mostly just want to solve their problem with as little thinking as possible.

Even with type inference, you still have to understand how to set up your type constructors and pattern matching, and if there is a type-inference error, you have to know how to fix it.

Is this just too hard for most people and domains? In other words, is this a limiting feature for a language in terms of "popularity"?

Depends what you believe is required for "popularity".

Languages are accepted and evolve by a social process, not a technical or technological one.
A successful language must not require users to have “mathematical sophistication”
slide 50, Models of Software Acceptance: How Winners Win.
Richard Gabriel

Languages (or language technologies) that solve real problems can succeed...
technology must: Alleviate real problems, What does it do?
Disruptive Programming Language Technologies
Todd Proebsting (much discussed on LtU Nov 2002)

Sorry, I seem unable to think about "language popularity" without thinking about utility.

too hard for most people and domains
Massive effort throughout the '90s went into retraining programmers in OO techniques. (30,000? trained by IBM in Smalltalk.) Wouldn't we expect the same thing to happen when HOTS go mainstream?

Playing golf like Tiger Woods may be very useful, but we don't expect every golfer to be able to effectively use his methods. ;-)

Wouldn't we expect the same thing to happen when HOTS go mainstream?

Not that I would mind, but I don't think it is a sure thing it every will go mainstream (the premise of my question). What makes you think it will be a when?

If it even has, really. ;-) There is still a LOT of code that is basically good old structured programming broken into "classes".

I would say though that it IS revolutionary, because to really get the most out of it, you have to THINK differently, more abstractly than many people are comfortable with.

I've seen some extensions to java (e.g. Pizza) that do this.

Generics are finally coming in 1.5.

What makes you think it will be a when?
Every dog has it's day. (I have no opinion either way.)

OO is not *that* revolutionary
Be(a)ware of hindsight bias or the I-knew-it-all-along phenomenon (Baruch Fischoff)

I guess not one of my finest analogies. ;-)

Suffice it to say, that some skills are just hard, and no matter how useful they might be, there will be a limit to the number of people who can pull them off, limiting there popularity.

Mmmm, pizza with sugar ...

But my opinion on this is connected to my opinion on utility. Sorry.

Basically, I think, no, sophisticated static type systems will never be as popular as less sophisticated ones, or dynamically typed languages. I think the major features of existing ones will eventually find their way into the mainstream, but newer generations of type systems will find smaller and smaller programmer communities. What will happen is that, eventually, we will have a small core of software engineers using good languages, and a very large community of technicians, just as we have a small number of electrical and structural engineers, and a large number of electricians and carpenters. What is now a craft or trade will become an engineering field, and the engineers will naturally be the ones using the most sophisticated tools.

(I've voiced this opinion here before, and, strangely enough, was accused of being elitist, as if by predicting the future I am somehow capable of influencing it.)

But here is another question you should ask: `Do you think that it will ever be the case that the programs people use most will have been written using a programming language with a sophisticated type system?'

And I think the answer to this question is, yes. I think the good properties of good languages (productivity, correctness and efficiency) will outstrip the shrinking of the developer community. At least I hope so. :)

Right now it isn't true, of course. Though I think languages like ML are clearly better than their competitors, the increased productivity factor and so on are not large enough to make up for the small community. (Also, languages like ML currently are too inefficient and hard to make interoperate with other languages, but these are by no means problems which are intrinsic to the static typing paradigm.) But what I see is that types research is accelerating, while the quality of conventional languages is improving at a much slower pace.

I agree the terminology was imprecise, but I thought "sophisticated type system" would sound elitist. ;-)

But my opinion on this is connected to my opinion on utility. Sorry.

Well, so long as we don't start another round of static vs. dynamic... ;-)

`Do you think that it will ever be the case that the programs people use most will have been written using a programming language with a sophisticated type system?'

This is an interesting question. And I'm not sure what I think the answer is. While I agree that FPLs are better for more "mathematical" domains (such as PLT research ;-) ), I'm not sure that correctness is actually that important for most applications.

For most applications, responsiveness to changing requirements is more important, and this is the impetus behind the Agile movement in software development.

It is still possible that advances in PLT will lead to better languages that have both simplicity and correctness, and this might bring about the change you are talking about. But I'm not sure it is a given extrapolating from the current situation.

And I can't believe I've just read that!

Correctness is getting more important, not less!

In the past, systems were still largely manual processes that could accomodate software errors. Now, with automation running end-to-end there isn't the same opportunity to absorb and nullify an error.

I became interested in Eiffel primarily thanks to Design-by-Contract, and expanded that interest into Haskell (and also now Oz) partly because I believe that declarative higher-order programming should enable more *correct* programs to be written, (and usually more quickly).

Returning to Frank's (to my mind accurate) prediction, the correct software will be written by the engineers, and the bad software will be bodged together by those "less-skilled". This is not elitist however. Not every musician can be a Sibelius, Bach or Mozart, just as not every Sibelius, Bach or Mozart could be a top chef/architect/chemist/whatever.

Perhaps I should clarify. Correctness is not the same as reliability. The former is a mathematical concept with practical implications, the latter a purely practical one.

A correct program can be used inappropriately to yield "bad" results for the problem domain; an incorrect one can be used in such a way that it is bullet-proof in its problem domain.

the correct software will be written by the engineers

As I've said in other threads, I think programming is by definition a specialized and skilled profession. I must nonetheless confess to a personal bias against the term "engineer" in this context. ;-)

This remark is belied by the fact that you felt compelled to put `mathematical' in quotes: the distinction between `mathematical' and `non-mathematical' domains is not well-defined, and largely historical. Or, to put it another way, mathematics is an approach to analyzing a domain, and not a domain (or class of domains) itself.

Conversely, there is nothing particularly `unmathematical' about untyped languages (or simply typed ones). Untyped lambda-calculus and Turing machines were both created and developed by mathematicians...

I'm not sure that correctness is actually that important for most applications.

Well, I have to agree with David here: our world is getting more automated, not less, and automation tends to propagate and magnify errors not reduce them. The fact that entropy increases in a closed system is a fundamental fact.

Furthermore, fault-tolerant systems are harder, not easier, to build than -intolerant ones.

Another problem is that I know no way of quantifying error distance for (untyped) program behaviors in general, so there is no good way to keep errors in check below a certain minimal acceptable threshold.

This suggests that a rational way to regard correctness for untyped programs right now is as a binary property: a program is either right, or wrong. There is no in-between. (For particular domains, of course, you can do better.)

For typed programs, you can always do better: a program is `more correct' than another if it is well-typed and the other is not. I would say this is a good candidate for a minimum requirement of correctness, especially since in almost all typed languages well-typedness is decidable.

Of course, in the future we would like to have methods to push that threshold up further.

For most applications, responsiveness to changing requirements is more important, and this is the impetus behind the Agile movement in software development.

First, how can you use a comparative like `more' when you can quantify neither adaptability nor correctness, much less compare them?

Second, I don't even find this sort of argument consistent. If my spec changes from A to B, and I have a program P which implements A, and correctness is less important than adaptability, then there must be situations in which it is tolerable for me simply to submit P as my implementation for B. In other words, I don't even have to make any changes to adapt! When is this acceptable, and when isn't it? Obviously one wants to force a change in P when the `distance' between A and B gets too big, but there is no good way of measuring it.

Third, I am simply not convinced that sophisticated typing makes a program inflexible. On the contrary, my experience is the opposite.

In fact, I find myself thinking more and more that the essence of a type system is not that it guarantees some minimum standard of correctness, but rather that it guarantees some minimum degree of abstraction. This in turn guarantees that there is a larger number of implementations. (More abstractness => more models.) And that allows a program to be reused in more contexts with differing performance requirements.

The increase in correctness, then, is rather a side effect of the fact that the programmer is forced to think more carefully about his program, because the type system demands a more explicit account of which program parts contribute to the behavior, and which contribute to the implementation.

I think you are well justified in that. Although software development has reasonable analogues for the practical aspects of engineering, such as project planning and team management, it has no analague for the technical aspects, such as specification and programming.

Programming is currently a craft or a trade, where novices learn almost entirely through experience. To make programming into a part of an engineering science, it has to be practiced in such a way that it cannot but succeed. In other words, it has to be (for the most part) an algorithm. But there is no such algorithm now: instead of analyzing the problem and applying formal methods from a relevant field of science, programmers rely largely on experience and `good taste'.

As for specification, the problem is even bigger.

Though I will agree that the there is no definite line between the two, I will offer an informal definition which I think is quite effective in practice:

A mathematical domain is one where a) mature mathematical models for that domain exist and b) there is a high correspondence between those models and the applications of the domain.

our world is getting more automated, not less, and automation tends to propagate and magnify errors not reduce them. The fact that entropy increases in a closed system is a fundamental fact.

I think there is a fundamental difference of perspective here. (Though this doesn't reduce entropy) an application is NOT a closed system. It co-exists and interacts with people who want it to achieve some practical end for them.

An application that does something provably without error. but that something is the "wrong thing" from the user's point of view is still "wrong" for that user. Conversely, if it does the thing the the user does want, even if theoretically it is inconsistent, the user feels that it is "right".

Third, I am simply not convinced that sophisticated typing makes a program inflexible. On the contrary, my experience is the opposite.

I agree with you, but, as you suggest, it is its power of abstraction more than its correctness that makes this so.

This is a bold rhetorical move, but of course you know that a partial order does not have to be quantified. ;-)

If it's automated, it's closed. If it's not closed and people have to maintain it every time it breaks down, it's clearly not automated.

Besides, systems of the second sort breed second-order automation: they tend to try to automate the maintenance. An example is automatic program updates, like you have probably seen in Adobe Acrobat Reader. Of course, these things break down, too. Soon we will get third-order automation, to fix the broken things which are supposed to be fixing our broken things.

Do you think this is a desirable situation? It seems counterproductive to me. Maybe it's a good way to decrease unemployment, though.

Maybe we should call the practice of building such software something other than `programming', like, oh, I don't know, SATAN?!? (Sorry, I'm having Church Lady flashbacks.) ---no, maybe we should call it system administration.

Your post suggests that perhaps you think software development should or could be like this.

I contend that it can't (in the general case). The reason has to do with user expectation.

If you build a bridge, the expectations of the user are fairly clear: it must bear loads of a certain magnitude and remain standing in spite of weather and other environmental calamities.

But with software, users want it to "do what I mean", even if they are a little fuzzy on the details of what they mean themselves.

This has even become a design principle in some PLs, which isn't surprising, given that users of a PL are thereby also software users.

What every software user wants is the perfect servant who knows what they want better than they do themself, and performs it flawlessly and without complaint.

Now of course, this is impossible, but it becomes part of the job of a developer to interpret take on a little bit of that role, since whether the application is a success or not is not determined by its load bearing capacity or something objective like that, but based on the subjective assessment of the user that it does something they find useful.

That's why the perfect spec and the iron-clad proof will never solve the problem of software development (in the general case).

Frank, I admire your prose!

Still, I think the debate would be more constructive if it be made more concrete. What specific features are you (that the plurla "you") thinking about?

Notice that when it comes to actual language design, it may be possible to expose similar functionality either via the type system or via other means, for example the module system. Usually this means things will not have "first class" status, but in some cases this is not a show stopper.

For example, C++ templates and Ada generic units allow type parameterization. Many programmers take these features for granted, and understand them. A different approach for achieving similar functionality would have been to directly enhance the type system.

I guess I'm not sure that anything is totally automated in a more general sense.

Almost any application of fair scope interacts with people through both input and output. Humans have the annoying habit of changing what they want to input and output with great regularity. Even humans can't deal with this reliably ("Parker get me the sales report for last month... <two days later>... No,no, I wanted it broken down my region and with a blue border.")

Sorry, I'm having Church Lady flashbacks Hmmm, makes me think of baby boomers when I was growing up yammering on about their "flashbacks". ;-) I guess we must be geezers now. ;-)

the correct software will be written by the engineers, and the bad software will be bodged together by those "less-skilled"
I read "we will have a small core of software engineers using good languages, and a very large community of technicians" and came to quite a different understanding. More like a statement about industrial process, predictability, and tiny steps in the maturation of a software industry.

I'll give a specific example: functional types.

Let's say you come across a function of type a->b->c->d.

What is the intent? A currying series? A combinator? An index on curried functions? The reader has to understand both how these are formally equivalent and how they differ in the concrete instance.

This makes it more work to figure out the theory of the code, which makes more work to use it, modify it, etc.

One can argue that this extra work is worthwhile, but one can also argue that this just "gets in the way" of solving the programming problem at hand (as most "dynamic" advocates do ).

Personally, I'm caught in the middle. I can understand both points of view, and there are circumstances where I prefer one over the other. Like so many things, I think it is a trade-off decision.

I think currying is fairly easy to understand if explained properly, and I think partial application will be standard in most future languages...

One can live in mortal fear of function pointers and still be a competent C programmer. ;-)

If you don't like function types in, say, SML, you might as well go home.

I think currying is fairly easy to understand if explained properly, and I think partial application will be standard in most future languages

I agree, and specifically I would like to contrast the situation with that in Scheme. If you understand the concept of currying, it is rather simple to understand it in a Scheme program.

Since the details of the typing are hidden from you, you simply focus on the implementation. This makes it easier to create a mental model of what is going on operationally, even if it might open you up to missing a detail that might have severe consequences for your application.

With explicit static typing systems for the same features, you must understand the typing to understand the program. This has advantages (it catches subtle problems, it requires a more thorough model of what is going on, etc.) but is also more demanding.

I know, I know, LtU, programming languages, to digress is human?

Humans have the annoying habit of changing what they want
Too user luser for my taste - the world changes, people need to respond.

What every software user wants is the perfect servant
Seems to be conflating the difficulty of figuring out system requirements, with the way people ascribe agency to some systems.

Smiley notwithstanding, I think communicating intent IS one of the core concerns of PLs.

the world changes, people need to respond

Precisely my point. People who develop systems need to respond likewise.

Seems to be conflating the difficulty of figuring out system requirements, with the way people ascribe agency to some systems.

The thing to remember is that "system" requirements are just implementational expressions of "people" requirements.

Now you can focus on building the correct system that does X, and this could be an end in itself.

But most software is made to fulfill some practical purpose for particular users right now. Most users don't judge effectiveness based on correctness, which is objective, but rather on utility, which is subjective.

There will be different priorities for the designer of a PL that is focused on one scenario or the other, and the effort cost of a complex typing system may be worth it for one and not for the other.

Although software development has reasonable analogues for the practical aspects of engineering, such as project planning and team management, it has no analague for the technical aspects, such as specification...

Or to put it in other terms, if we have a specification language that can be used by programmers to proveably implement a correct solution in a given programming language, then what we've just done is create a new programming language (with the one we used to call a language now becoming little more than a compiler).

Programming is currently a craft or a trade, where novices learn almost entirely through experience. To make programming into a part of an engineering science, it has to be practiced in such a way that it cannot but succeed.

The thing to remember is
Yes, these are the things I have daily experience of ;-)

We may agree that a programming language designer can tip the balance of a language towards what they feel will provide more flexibility or more of some other appealing qualities.

Whether or not in practice that results in more flexibility seems less obvious to me, because we inevitably bring a supporting framework of techniques and tools into play. Maybe some other quality of the language makes easier (or motivates) development of other tools, which in combination give real flexibility. (Often PL discussions have a tacit all-other-things-being-equal; perhaps that should be many-things-being-different-as-appropriate.)

From the outside, it seems like there's still a lot of work being done on raw aspects of "higher-order type systems". My guess is they'll be different cooked and ready-to-serve.

What Do You Get When You Cross a Computer 
   with an Airplane? 
   with a Camera? 
   with an Alarm Clock? 
   with a Car? 
   with a Bank? 
with a Warship? 

(Apologies to the Ericsson AXD 301 ATM Switch team, and... )

That's an interest topic to pursue; what would "cooked and ready to serve" look like?

I must confess that I'm having a hard time imagining it without sacrificing some of the expressiveness (or to extend the metaphor "flavours" ;-) ) that it brings to the table.

That's an interest topic to pursue
I don't know.

(With apologies to vegetarians, those tired of bad analogies and my off-topic self-indulgence)
I'm watching people discuss what joints of meat could be cut from a carcass. I don't know of filet mignon or ribs or... Although I have tasted maguro and tuna steak, so I think there must be some interesting possibilities.

I think that in some respects this is false, partly because people's expectations of what software is supposed to do is so much higher.

Take the airplane example. We don't expect that a layman should be able to fly a plane, do we?

But software, no matter how complex its task, has to be able to be easy enough for my grandmother to use.

We don't expect the airplane to be flown in all kinds of weather, but we assume that software should run on any platform, no matter what other crud is running on it.

Running around saying the sky is falling is a great way to make a living as a consultant, but that doesn't mean it's true.

Take the airplane example - You need to look at the example in the book.

easy enough for my grandmother - Not unless your grandmother is somehow a representative user.

we assume that software should run on any platform - Nope.

saying the sky is falling - Have you read enough to come to that conclusion?

I really don't see a reason for this sentence to end with a smiley.

Sadly true. ;-) I will therefore resist the temptation to respond in full, and simply bring back the point to type systems.

I wish to refute the chain of reasoning that goes:

most software is horribly bad compared to equivalently complex activities -> this is because developers lack rigour -> therefore we should strive to make programming "mathematically correct" (e.g. introduce complex type systems) -> the problem with software will be solved

My own chain is: software problems are often human problems, including changing requirements and unrealistic expectations -> more rigorous type systems (or rigour of any kind) won't necessarily solve the problem.

Of course they will not necessarily solve the problem. But do they have the potential? Can they help a bit?

That's a completely different question isn't it? ;-)

My personal bias is in favour of typing systems in general, because they (mostly) help to communicate intent and they "document" design decisions that can otherwise get lost.

An example of the latter is that when I was into Scheme, I would frequently forget how I had decided to represent a particular data structure as a list. I didn't find a system for this that was as simple and consistent as having a type that shows you (and can catch inconsistencies).

However, many people in the TDD community, whose opinion and reasoning I respect, feel that tests give you the same effects without the overhead of figuring out the complicated situations, such as the functional type example I gave earlier.

I've become more sympathetic to this position so that I'm sitting on the fence now. ;-)

I'm intrigued by Isaac's suggestion that there might be a "fully-cooked" version of complex typing that would allow the best of both worlds. If anyone has any good suggestions, it could knock me back off the fence. ;-)

"types entail tests ... XP calls this TDD. The static typing community calls this typeful programming." LtU Dec 2002

Given that TDD is much used with Java (not exactly an agile language), what would it be like to use TDD with a Typeful Language? (Has it been tried? Is there some inherent incompatibility?)

I will therefore resist the temptation to respond in full
Email is fine. I'd just like to keep my LtU postings more on topic.

Someone asked about this on a TDD list a couple months ago, and received no responses.

I haven't tried TDD with typed FP(yet) but I don't see why it would be incompatible. People do DbC with TDD (another thread on the list). The general feeling seems to be that you can use whatever additional techniques you think work for you, but many practitioners don't see that need for things like type systems or contracts since the tests cover it.

I'd just like to keep my LtU postings more on topic

An excellent and wise policy. I was getting too ranty there for my taste anyway. ;-)

Marc: This is a bold rhetorical move, but of course you know that a partial order does not have to be quantified. ;-)

Fine, but what is the partial order?

If you build a bridge, the expectations of the user are fairly clear ... But with software, users want it to "do what I mean", even if they are a little fuzzy on the details of what they mean themselves.

Some users may want that, but I wouldn't feel bad about telling them that what is impossible is impossible. On the contrary, I would feel it is my duty as a professional to do so. If somebody tried to contract a structural engineer to build a bridge over the Atlantic he or she would waste know time telling them it was impossible, and suggest alternatives.

This has even become a design principle in some PLs, which isn't surprising, given that users of a PL are thereby also software users.

I think it's not surprising either, but for a different reason: not because programmers are also users (now I'm having "Hair Club For Men" flashbacks...), but rather because so many programmers lack a basic grounding in computer science. That's why we teach it.

What every software user wants is the perfect servant who knows what they want better than they do themself, and performs it flawlessly and without complaint.

Yeah, and I wanna pony. :)

Now of course, this is impossible, but it becomes part of the job of a developer to interpret take on a little bit of that role, since whether the application is a success or not is not determined by its load bearing capacity or something objective like that, but based on the subjective assessment of the user that it does something they find useful.

That may be your job as a company employee or a merchant, but it is not your job as a programmer; likewise, one can draw a distinction between the commercial/popular success and the technical success of a project. I don't see any advantage to mixing the two up. Indeed, I think it is a kind of dishonesty to do so.

I can certainly agree that there is no technical method that will guarantee commercial/popular success and maybe that even implies that you shouldn't try to sell products based on their technical quality. But, I do believe, and indeed I think it should be obvious, that technical methods have a powerful effect on technical success, and that "practicing in such a way that one cannot but succeed" has to be the ideal of any field which one could reasonably call engineering.

That's why the perfect spec and the iron-clad proof will never solve the problem of software development (in the general case).

They wouldn't solve the commercial problem---which BTW I acknowledge is part of engineering in practice---but they would solve the correctness problem, which has to be the foundation of the technical problem.

Isaac: Engineering doesn't seem to have achieved [perfect practice] yet!

I don't claim it does, but I claim it must be an ideal for anyone who wants to call him or herself an engineer.

Marc: a->b->c->d. What is the intent? A currying series? A combinator? An index on curried functions? The reader has to understand both how these are formally equivalent and how they differ in the concrete instance.

No, they don't.

Do I have to be Picasso to use a paintbrush? Do I have to be Michael Jordan to use a basketball? Do I have to be Zaphod Beeblebrox to use a towel?

Anyway, your point would be only the truer in a dynamically typed language. Given any value, how do I know the intent? At least in a typed language I know the type, and so I know, if it's a function type, that to use it I need to apply it; if it's a tuple, I need to project out a field; etc. Is that enough to know the intent? No, for that you need to look at the context or, better, the documentation. But in the absence of those things having a type would irrefutably be better than nothing.

One can live in mortal fear of function pointers and still be a competent C programmer. ;-) If you don't like function types in, say, SML, you might as well go home.

I agree, and perhaps that suggests something vis-a-vis SML, but 1) it's not a limitation which is intrinsic to languages with sophisticated static type systems, and 2) the same problem would exist for a DT language like Scheme (see below).

BTW, one way to communicate `intent' via a type system is to define a type isomorphic to an exisiting one. For example, if you are using a->b as a form of indexing you define the type Map a b, perhaps even fixing one or both arguments: IntMap b.

If you understand the concept of currying, it is rather simple to understand it in a Scheme program. Since the details of the typing are hidden from you, you simply focus on the implementation. This makes it easier to create a mental model of what is going on operationally, even if it might open you up to missing a detail that might have severe consequences for your application.

This is completely bogus.

It's much easier to explain currying if you write down the types involved because they give you a coarse-grained view of what's going on. One can ignore the effect on values at first and just absorb the overall pattern of the transformation. Then you `fill in the details' by observing what's going on at the value level. This is an instance of separation of concerns making a cognition task easier.

Explaing currying with types is easier than explaining it without, just as it's easier to paint a picture if you first draw the outline, or to find a building if you first consult a map.

With explicit static typing systems for the same features, you must understand the typing to understand the program. This has advantages (it catches subtle problems, it requires a more thorough model of what is going on, etc.) but is also more demanding.

No, this is only true for some languages, mainly OO ones and some dependent type systems. In particular, it is not true for ML, which has a type-erasure semantics: every ML program behaves the same as the equivalent untyped lambda-calculus program (or Scheme program, if you will) obtained by erasing the types. FWIW, I don't like languages in which the dynamic semantics depends on the typing.

I think communicating intent IS one of the core concerns of PLs.

Whether or not this is true, you cannot communicate more intent with a language which is demonstrably simpler; this is a basic fact of information theory. Your less-is-more argument is nonsense.

Chris: Some might say that the program is the specification.

No one who is interested in correctness, though.

Or to put it in other terms, if we have a specification language that can be used by programmers to proveably implement a correct solution in a given programming language, then what we've just done is create a new programming language

No, the difference between a programming language and a specification language is that a programming language is executable while a specification language need not be. In fact, in a way the whole point of a specification language is that it is not executable, so that the specification writer is relieved from the need to specify an algorithm at the same time as he is specifying the behavior.

Isaac: From the outside, it seems like there's still a lot of work being done on raw aspects of "higher-order type systems". My guess is they'll be different cooked and ready-to-serve.

I don't understand what this means. Could you speak English instead of Culinarian? :)

Marc: "Acceptable levels of quality for software engineers are far lower than those for more traditional engineers" I think that in some respects this is false, partly because people's expectations of what software is supposed to do is so much higher.

They may have high expectations, but they also have a very high tolerance for faulty software, a fact which the software industry is perhaps unwittingly but nonetheless effectively exploiting. But I will not say that, if one developer suddenly started producing consistently correct but inflexible software, that everyone would buy it or use it.

I wish to refute the chain of reasoning that goes: most software is horribly bad compared to equivalently complex activities -> this is because developers lack rigour -> therefore we should strive to make programming "mathematically correct" (e.g. introduce complex type systems) -> the problem with software will be solved

The technical problem with software, and, no, it won't be solved. In addition to correctness, there are also the issues of productivity and adaptability of software. My view is simply that it is meaningless to talk about productivity or adaptability without also addressing correctness, just as it is meaningless to talk about, say, the length of a path when the `path' doesn't even have endpoints!

BTW, it is not impossible to address the adaptability issue as part of the correctness issue.

software problems are often human problems, including changing requirements and unrealistic expectations -> more rigorous type systems (or rigour of any kind) won't necessarily solve the problem.

My question for you is, why do you think that `changing requirements' are necessarily incompatible with a mathematical approach to design and development? There are plenty of notions of specification morphism and whatnot.

My personal bias is in favour of typing systems in general, because they (mostly) help to communicate intent and they "document" design decisions that can otherwise get lost.

It seems to me you were arguing just the opposite above! Perhaps I misunderstood you.

The reason I asked for concrete examples is that I think this sort of question is impossible to answer unless we agree on the language features involved.

I am fairly certain that advanced type system means something completely different to C programmers and to Haskell programmers.

Easy. correctness <= adaptability ;-)

so many programmers lack a basic grounding in computer science. That's why we teach it.

The interesting thing is that many programmers DO have CS backgrounds now, but it doesn't necessarily have that big an impact on the acceptance of more complex languages, etc. Most people ignore what they learned in school. ;-)

That may be your job as a company employee or a merchant, but it is not your job as a programmer

While I understand the principle here, and believe in it myself to a degree, my experience tells me that the dividing line is much fuzzier than that.

My question for you is, why do you think that `changing requirements' are necessarily incompatible with a mathematical approach to design and development?

There not strictly incompatible, it's just that there is a time trade-off, and the kinds of problems that come up most are not necessarily addressed.

Most "failures" in software (in my experience) don't arise from incorrect algorithms, but from a failure to handle random changes in the environment (fluctuation of load, the network goes down, there is a conflict with something else on the machine.) Since it is very hard to predict all possible things that could go wrong, and even if you could, it would take too long to handle them all, the priority in the situation is going to be dealing with those practicalities rather than "proving it correct".

It seems to me you were arguing just the opposite above! Perhaps I misunderstood you.

I guess I'm arguing a bit from both sides. ;-) My natural position is pro-type in general, but I think the "dynamic" people have a point when it comes to some more complex type constructions: it does require more thought to work it through. I will agree that, for example, currying is more explicit in typed form, but I think paradoxically that sometimes more clarity confuses people.

As I've said about very explicit and consise mathematical notation before, sometimes you have to work very hard to uncover an idea that you already had. ;-)

The exchange of opinions is entertaining.
My feeling is that these questions are best answered by measurement.

That may be your job as a company employee or a merchant, but it is not your job as a programmer
I like that. We perform multiple roles during our workday. Maybe we don't need to let the concerns from one role permeate other roles as-much-as we do.

ideal for anyone who wants to call him or herself an engineer
I'd be interested in your response to "Software engineering and the art of design" on artima.com (Although LtU probably isn't the place to post it?)

What, with bogus Psych 101 studies? ;-)

I will offer that we DO have a measure; the success of the "dynamic" camp to get converts relative to the "typeful" camp based on the claim it is "easier".

People seem to resonate with that, so it must have some relevance to their experience.

Do you have figures on this? Because it doesn't seem that way to me.

but it doesn't necessarily have that big an impact on the acceptance of more complex languages, etc.

Perhaps that's because most schools baptize them in the C++ swamp.

Most people ignore what they learned in school. ;-)

Yeah, but it's a shame they all work in the IT industry. :)

No, but seriously, I don't think that is the case with engineering majors who actually go into engineering. You can't be an engineer without knowing how to do engineering. But the sad truth is, given our current level of standards, almost anyone is qualified to be a programmer.

I will offer that we DO have a measure; the success of the "dynamic" camp to get converts relative to the "typeful" camp based on the claim it is "easier".

Popularity is only one kind of success (as I already took pains to remark above), and correlates with quality hardly at all; for evidence of this one need only look at the American music industry.

I looked at that, and even started to reply, but I realized that now I'm burnt out on this topic, and don't want to get into another long thread, especially in a new community where I have to explain all my underlying assumptions which are, frankly, probably quite radical to most software developers. Maybe it would be most expedient for me simply to write a position paper and post it on my site.

Well, at least I have an account on Artima now, so I may reply later, but since that thread is quite related to what I wrote here, you may consider posting a link. Or not.

Sadly no. I have found in general that getting meaningful and unbiased stats on what is going on in the industry is very difficult.

However, based on my experience hiring programmers, a significant percentage of the resume pile do have CS degrees.

I don't think that is the case with engineering majors who actually go into engineering.

Do you think the average engineer uses most of what he learned in school on the job? Many are really in management jobs, and probably have to worry more about costs and workplace politics than differential equations.

for evidence of this one need only look at the American music industry

Though I share your feelings about American pop music, I have to grant that the industry does have a high level of quality in an engineering sense: they can pump out polished, reliable product that many people like and buy.

Just as boy bands and Whitney Huston are effective at fulfilling the needs of their "users", the "dynamic" languages are fulfilling the needs of theirs. What interests me is, how are they doing that?

What aspects of static typing have made so many willing to throw it away? Do they have any points worth considering?

I've been wrestling with this question for a while now, since people whose knowledge and experience I respect have been touting Python and Ruby and dismissing concerns about "dynamic" features. (Admittedly, there are a fair number of former Smalltalkers among them, so there may just be a low-level bias there ;-) )

I can only conclude that there ARE valid points on the "dynamic" side, so the challenge now is to understand what they are, how they apply, and how we might be able to "have our cake and eat it too", that is, to have the benefit of static typing and "higher-order" types without any of the negative side-effects.

They may be fulfilling the emotional needs of DT language programmers, but they are not fulfilling my right as a user of their programs to a minimum standard of objective proof of correctness. Well-typedness is such a standard, and no amount of tests, assurances or experience can guarantee it. As a user of programs written by people who call themselves engineers, I demand that they use best practices.

Do they have any points worth considering?

They have no points. A DT language is just a very simple ST language, as I just demonstrated (again) in the Ruby thread. Asking whether DT is better than ST is like asking whether you can improve your handwriting by cutting off a finger, or improve your sex life by thinking chaste thoughts. It's counterproductive luddism.

I don't understand why people have such a blind spot about this. I can only conclude it's ignorance.

Another useful attribute of DT PLs is that they are more accessible to non engineers. Thus they are useful as macro languages and for customization. They are also very useful as glue languages to tie various components together, and for testing components in an interactive environment. I have used DT PLs extensively for these purposes. In this context the lack of provable correctness is compensated for by the general restrictedness of the environment and the problem domain.

Finally, we need Patrick on this thread to provide Frank with a worthy adversary.

I don't know what you mean, but if you give a clearer explanation I will (try to) show you how to do it in an ST language in the same manner as I demonstrated on the Ruby thread.

If it's possible in untyped lambda-calculus, then it's possible in an ST programming language. There are no exceptions. It's a theorem.

If it's impossible in untyped lambda-calculus, then it's not possible in any programming language. There are no exceptions. This is also a theorem.

We should remember that many programmers experience of ST is C, C++, Java. Given those choices perhaps the attractions of DT are easier to understand.

(ST compared DT seems to be shorthand for Typing in Java compared to Typing in Python, on artima)

Note I did not say impossible, I said not as easy or intuitive. I actually gave several examples in the past (which I recently repeated). My favorite is the database recordset example, where the table structure is only known at runtime.

Looking back to the start of this discussion (and noting Windows security flaw) the truth seems to be that C/C++ are too hard to understand for most people who use programming languages !

C++ is actually set up for truly expert programmers, but is generally used by non-experts in the field. E.g. “new” can be overridden and a really great storage allocation system can be written (by a really great programmer). Similarly other features intended as templates for experts can be overridden. It is a source of frustration to Bjarne Stroustroup, the inventor of C++, that most programmers don’t take advantage of the template nature of C++, but instead use it as a given. This usually leads to very large, slow, and fragile structures which require an enormous amount of maintenance. This was not what he intended!

Appendix B: Is “Software Engineering” an Oxymoron?
Alan Kay

It is easy and intuitive, though. Just add the following to my original datatype U:

  | Obj (FiniteMap String U)

and define:

addField = Fun (\ (Par (Obj o, Par (name, v))) ->
  Obj (addToFM o name v))
getField = Fun (\ (Par (Obj o, name)) ->
  case lookupFM o name of
    Nothing -> Uni -- or whatever
    Just v -> v)

Or I can do it imperatively, but I will spare you the Haskell IORef's. In ML it is straightforward to do with references.

I think you hit the issue exactly with the word "simple". The virtue the DT people see is that of simplicity.

As in the Einstein quote: "find the simplest possible solution to the problem... but no simpler."

The trick is to find the "no simpler" line. You say it is ST; others say it is DT.

One thing I do know about engineering is that it is all about trade-offs... ;-)

It is a theorem that all programs can be expressed in a suitable encoding as a stream of 0s and 1s.

However, I am not inspired to use that "PL" in my daily work. ;-)

I imagine that in future the same situation may exist with HOTS - languages for *real* experts doing special things and languages for everyday.

engineering is is all about trade-offs...
Yes, and radical change in engineering practice is often about uncompromising extremes. Seem to remember John Seeley Brown describing how they pushed forward: we don't want a quieter printer, we want a silent printer - go make.

It is a theorem that all programs can be expressed in a suitable encoding as a stream of 0s and 1s. However, I am not inspired to use that "PL" in my daily work. ;-)

The language is simple. Writing correct (or efficient) programs with it is not.

The proof that relates untyped LC and typed LC with recursion is an effective algorithm which, IIRC, preserves reductions, which is about as nice a correspondence as you can get. Going from typed to untyped just involves erasing the types. Embedding untyped in typed just involves inserting some embeddings and projections as I just showed you on the other thread.

The Gödel encoding algorithm which relates untyped LC with the naturals, OTOH, is extremely arbitrary and obscure.

So I think your skepticism is unjustified.

I was thinking about the more commonplace translation of all programs to binary.

The proof that relates untyped LC and typed LC with recursion is an effective algorithm which, IIRC, preserves reductions, which is about as nice a correspondence as you can get.

But from the point of view of the programmer (not the compiler writer), the hard part is getting all the type reasoning done in the first place. The conversion to "untyped" is done automatically, and doesn't make it easier or harder for me to write my program.

Let me see if I understand you. Would you agree with either or both of these statements?

1) Correctness is so important that we should be willing to expend any amount of effort achieving it.

2) Typing is actually simple and requires no extra effort, so why would anyone not do it?

As I've said before, I moderately disagree with both, but think that both could be softened to encompass the position I do hold.

Your point is correct and well taken. I would say that there isn't really such a difference between what you are proposing and what I generally do. Using the power and flexibility of Haskell you've built a DT module on of an ST PL. Given that C++ or Java are not flexible enough to do this, I simply use JavaScript on top of them (well you could probably do it, at least in C++, but the resulting syntax would probably be horrendous and nothing like "real" C++).

There are even several advantages in this approach:
1. I can easily bundle a JavaScript "development" environment as a part of my application.
2. I can constraint the functionality of the JavaScript code as much as I want (which in the module case is harder, the "scripter" can basically access anything she wants)
3. I can use it as a glue between components written in various PLs.

The main downside is having to work in two distinct PLs but that's not such an issue for me. And most of my team stayed on one side of the divide or the other.