Lambda calculus was introduced in 1936 and in 1948 it was given simple type system (along Fortran one, which, in turn, was introduced in 1958, ten years later).
Year after Simula-67 was introduced, logician Hindley presented a polymorphic type system with type inference for lambda-calculus, which was later rediscovered by Milner and incorporated into ML in 1978.
Simula-67 didn't have proper parametric polymorphism. I know no such examples before ML.
Functional programming is based on logic and could be a basis for logic on its own. Consider Type Theory by Per Martin-Loef. Or even simpler extension of polymorphic type system fo lambda calculus: Haskell's type classes, where type represents theorem, and function text serves as a proof.
OOP, on other hand, does not represent some simple kind of logic. I emphasize simple, because Luca Cardelli finally found some logic out there.
So I think that OOP is inherently less useful that FP.
Unfortunately, I don't think type theory has a whole lot to do with programming or software engineering. The most practical languages (as measured by popularity, which seems to be the best way to do it over a period of decades) do not have sound type systems, nor even particularly interesting ones theoretically.
Types allow requirements changes to be propagated through all program. State-of-the-art type systems even allow accounting of effects, like prevent deadlocks by ensuring a specific order of locking: http://www.cs.st-andrews.ac.uk/~eb/writings/fi-cbc.pdf
This is just another tool in a toolbox. You can use it. Or you can throw it away as "no one seem to use it".
I never said "no one seems to use it". What I specifically said was that I don't think type theory has a lot to do with programming: i.e., that the majority of work put into type theory in academic contexts does not, on balance, do much to improve the state of programmers writing software, or the quality of our software engineering.
"Types allow requirements changes to be propagated through all program" - what does this even mean, and why is it a justification for powerful types? I designed a system once that let you describe the program at a high level, using a DSL. I've outlined it several times on this site here (here's one link: http://news.ycombinator.com/item?id=2192322). Now that system allowed requirements changes to be propagated throughout the whole program, because the level of description of the program was dense enough that it could just about be considered detailed requirements (i.e. it was powerful - see below). It worked because it was focused on a reasonably precise niche. It did enough checks during the compilation process that you could be fairly sure that if it didn't find any errors, it would work without bugs (i.e. it was good - again, below). But the level of type system it had was no more advanced than Pascal - and I mean early Pascal, no objects etc. If you can get the same effects without a very abstract and powerful type system, isn't that better, because it reduces the overall expressiveness of the language - i.e. reducing the solution space that needs to be searched? Form can be liberating.
Preventing deadlocks by ensuring a specific order of locking. Fantastic; good work. How many people are using it? Which large shipping systems are using it? What was the prior rate of deadlocks for similar systems at that level of complexity, how long did those deadlocks take to be fixed, and how much time and money was saved by using this new technique? Because frankly, deadlocks are trivial to debug; the relevant threads are stopped, and after you attach a debugger the stack traces tell you exactly which locks were taken and in which order. Debugging races is a wee bit harder.
I have TAPL by Pierce right here on my bookshelf. Here's a typical sentence which illustrates my problem: "Perhaps the best illustration of the power of recursive types is the fact that we can embed the whole untyped lambda-calculus - in a well-typed way - into a statically typed language with recursive types." (pp 273). It seems to me to take for granted that a statically typed language is good[1], and that a good measure of power for a statically typed language is how expressive it is (i.e. what shapes of programs it can express, not e.g. how syntactically light it can be in doing so). And this is probably right and good, for type systems. But I have a different perspective of "good" and "power" in a programming language (as distinct from a type system). A good language is one whose target audience finds it easy to express their intent in such a way that the computer can understand. A powerful language is one in which complicated effects can be expressed with succinctness. And this is the core of it: type theorists spend entirely too much time on theoretical benefits, and far too little time on whether these benefits are worthwhile. Perhaps that's not their job, you say: and I agree to you to the extent that you also agree, then, that much of their work is irrelevant because of that.
[1] I happen to like statically typed programming languages, but I understand why some people don't. I wrote an extended reply on this topic to Paul Biggar some time ago, again on this site: http://news.ycombinator.com/item?id=1110653
You are right that many people don't need the results of type theory for their work. But that mainly tells on the type of work you do. For example many people think programming does not need math but if you are writing physics engines, graphics engines or doing machine learning then you need some basic level of mathematical sophistication. Similarly, if your work is related to automatic verification or the transformation from code to code then knowing type theory will save you a lot of wasted effort reinventing pitfalls. Type theory gives a foundation and a why basis so that intuition can be augmented beyond rules of thumbs. Language Oriented programming is one which would benefit from such a knowledge. Consider also that the future is not going to be dominated by one platform, powerful code transformation tools will be a strategic advantage. Know that my emphasis is not on the strength of the type system just its consistency and ability to augment human reasoning.
Software engineering is the only field of engineering whose practitioners do not use a basics grounded in math. Electrical people have Maxwell, ohm, gauss etc. Mechanical engineers and dynamics, civil continuums and so on. None of these professions you will note, came after the math. The math came as a result from studying and generalizing on these and then feeding the results back providing a net gain for both. This leads me to believe we are in early stages yet. We have the catapult without trigonometry. We do not have enough understanding to build stuff to withstand earthquakes. You say that most languages don't have well founded types but you fail to note that many of those same projects often have massive teams, massive code bases, fail often, run over time and are insecure.
But all that said, programming is different isn't it? You can get instant feedback and build something that you think is good because it fits all the white swans you put inside it. So I think before we have a foundation we will need tools that are built from and require a basic understanding of category theory and types. These can then be used to quickly iterate tests and do so with strong guarantees without having to write annoyingly tedious constructive proofs. Genetic programming is stupid but what if it could reason about types and try hypothesis on a meta level as well? Or what if tools such as http://lambda-the-ultimate.org/node/1178 were developed into the typical programmers toolchain? But yes, complex types without tools are a hard sell.
Code transformation has historically focused on syntax, but fallen down on semantics. The devil is in the fine details; C# might look superficially similar to Java, that you might create a code transformation from one to the other, but you end up falling down in really thorny areas like order of class initializers and finalization semantics, not to mention of course differences in scope and substance of libraries, standard and otherwise. When your code is pure and functional, you can make much stronger statements about it. But I think it's still an open question as to whether functional code can be made practical in the large.
"You say that most languages don't have well founded types but you fail to note that many of those same projects often have massive teams, massive code bases, fail often, run over time and are insecure" - are you suggesting that correlation is causation? Of course you aren't. But you might be guilty of thinking that something must be done, powerful type systems are something that seem good, therefore they should be used. And it's precisely this kind of implication that I'm skeptical of. When we start seeing substantial bodies of industrial software using advanced type systems rather than incorporating more limited, less orthogonal and less general subsets, I'll dial back my skepticism; but I'm willing to bet, at this point, that if that does happen, we won't have seen the end of massive software failures. I think that's a social problem, not a technical one. Our reach forever exceeds our grasp.
As I mentioned in my earlier post I do not think it is the power of the type system that is key but its consistency and the accompanying tools. I am not saying programming in Coq or dependent types are the answer. I am asking, what if programmers had access to a more polished toolkit to create domain specific versions of djinn where it would guide them or help layout some basics? Knowing that the code was derived from sound axioms. Other engineers can quickly protoype the validity of their ideas by mechanically running through some equations, why not software engineers?
Already I use types in Haskell and F# to help me figure out how to layout the code - I write some basic code where I know which function it will feed into, I don't have to think much as I try to get the code to fit the types. Nothing fancy but still highly useful.
As for code transformation I don't mean generic stuff like Visual Basic to Java, I mean having a team able to write the tools themselves with full awareness of the requisite semantic mappings. Or even better, creating a dsl for the domain and then having that map down to appropriate platform specific code. But it need not be traditional development you could extend it to machine learning - say you are doing genetic programming to fit data, using types to have some level of axiomatic reasoning rather than random cross over may be fruitful. There are all sorts of uses where application of basic - not fancy theory is helpful.
"I don't think type theory has a whole lot to do with programming or software engineering. The most practical languages ... do not have sound type systems"
well i mean most software isn't understood, using Linus's metaphor, most software works due to "years and years of testing on thousands of machines", not due to "thinking and analyzing"[1]. and, i think, teams that are capable of "think and analyse" can out-compete teams that don't.[2]
I think this more relates to mindfulness as you work through a programming problem. I know that when I am very tired, I can sometimes succumb to the "random walk" approach to debugging, where my reasoning takes a rest and I start coming up with theories as to why the program isn't working, and start changing little things to see if they fix it. If it was graphical work, it might be changing + to -; if it was one of my current bugs right at this minute (relating to dynamic linking on OS X), it would be adding an extra indirection to a pointer lookup. This "approach" is sometimes faster than the mindful "think and analyse" way, but only by chance, and only when your approach was roughly correct to begin with. And I agree that the "think and analyse" technique is better; rest is usually better than the random poking, which can also introduce a bug that bites you a few weeks later.
But "thinking and analyzing" I think also applies to my problem with type theorists! They spend a lot of time coming up with new ways to use various formalisms to capture various intents of the programmer (like the deadlocks and accounting of effects in an uncle post), but they don't spend much time doing science: the kind of science that happens when you have a control group. They've got their heads down at too low a level.
That's a bit of an attack on the whole edifice of computer "science", but I think it's long overdue. I don't think we're going to find any magic formalism that revolutionizes the world, making writing programs of arbitrary complexity trivial for schoolchildren. I think we need to spend more time looking at actual people, their strengths and weaknesses, and crafting our formalisms around those - and that work is only honest if it actually measures effects on average joes doing work, not rework of existing programs by talented graduate students.
"Unfortunately, I don't think type theory has a whole lot to do with programming or software engineering. The most practical languages (as measured by popularity, which seems to be the best way to do it over a period of decades) do not have sound type systems, nor even particularly interesting ones theoretically."
That is hilarious! I just showed this to my black, British cat, Mr. Fluffer Wickbidget, III, and he spit out the milk which he had been lapping from the palm of my hand.
You should sit down with the brilliant Hongwei Xi, the creator of the amazing ATS programming language, and see what he thinks of your jocular comment. If you're lucky, he might explain to you the reality of his Applied Type System, which not only provides for a very practical use of types, with the side benefit of theorem proving, but has also been shown to be almost as fast as C.
You seem to think that I think that the problem with languages with powerful type systems is that they are slow, and showing something as fast as C is a proof against this? I don't think your comment is relevant to the thrust of what I wrote, sorry.
Is it that hard to see different uses for different languages? Original BASIC was neither OO nor FP and came after both. Still it satisfied a particular need. C++ is the worse programming language in the world, except for all the others - in the domain it is used in.
>Is it that hard to see different uses for different languages?
Okey. How about language that could encompass all of them? The thing about such language is that it have to be functional one, at the core. Be it Lisp, or Haskell, or Agda2.
Uh certainly, FP language are certainly the most powerful and flexible languages, aside from maybe logic languages, far beyond OO. FP language definitely encompass more, you are correct there.
I just think it's important to not to confuse power and flexible with usefulness. Rigidity and limits have their uses.
As far as c++ goes, it's market share shrinks every year yet since the market grows and c++'s share began huge, c++ gains more users and more market position every years than the total users of functional programming languages. That may change in the future. FP will have to show its usefulness and not only its power and flexibility for this to happen.
Mobile seems to be generating a resurgence of interest in C++. Squeezing every last bit of performance out of tightly constrained CPU and RAM matters again.
They split program into slow and fast parts, slow parts used compact byte-code interpreter, fast parts were compiled into native code with optimizations.
They didn't used "code compression" like Forters do - Forters refactor common pieces of code into separate definitions. Nevertheless, they made quite balanced system.
Type system for OOP was developed during some 25 years: http://lucacardelli.name/Talks/2007-08-02%20An%20Accidental%...
Lambda calculus was introduced in 1936 and in 1948 it was given simple type system (along Fortran one, which, in turn, was introduced in 1958, ten years later).
Year after Simula-67 was introduced, logician Hindley presented a polymorphic type system with type inference for lambda-calculus, which was later rediscovered by Milner and incorporated into ML in 1978.
Simula-67 didn't have proper parametric polymorphism. I know no such examples before ML.
Functional programming is based on logic and could be a basis for logic on its own. Consider Type Theory by Per Martin-Loef. Or even simpler extension of polymorphic type system fo lambda calculus: Haskell's type classes, where type represents theorem, and function text serves as a proof.
OOP, on other hand, does not represent some simple kind of logic. I emphasize simple, because Luca Cardelli finally found some logic out there.
So I think that OOP is inherently less useful that FP.