TITLE: OOPSLA Day 3: Philip Wadler on Faith, Evolution, and Programming Languages AUTHOR: Eugene Wallingford DATE: October 28, 2006 7:36 PM DESC: ----- BODY: Philip Wadler "Of course, the design should be object-oriented." Um. "Of course not. The design should be functional". Day 3's invited speaker, Philip Wadler, is a functional programming guy who might well hear the first statement here at OOPSLA, or almost anywhere out in a world where Java and OO have seeped through the software development culture, and almost as often he reacts with the second statement (if only in his mind). He has come to recognize that these aren't scientific statements or reactions; they are matters of faith. But faith and science as talking about different things. Shouldn't we make language and design choices on the basis of science? Perhaps, but we have a problem: we have not yet put our discipline on a solid enough scientific footing. The conflict between faith and science in modern culture, such as on the issue of evolution, reminds Wadler of what he sees in the computing world. Programming language design over the last fifty years has been on an evolutionary roller coaster, with occasional advances injected into path of languages growing out of the dominant languages of the previous generation. He came to OOPSLA in a spirit of multiculturalism, to be a member of a "broad church", hoping to help us see the source of his faith and to realize that we often have alternatives available when we face language and design decisions. The prototypical faith choice that faces every programmer is static typing versus dynamic typing. In the current ecosystem, typing seems to have won out versus no typing, static typing has usually had a strong upper hand over dynamic typing. Wadler reminded us that this choice goes back to the origins of our discipline, between the untyped lambda calculus of Alonzo Church and the typed calculus of Haskell Curry. (Church probably did not know he had a choice; I wonder how he would have decided if he had?) Wadler then walked us through his evolution as a programming languages researcher, and taught us a little history on the way. Church: The Origins of Faith Symbolic logic was largely the product of the 19th century mathematician Gottlob Frege. But Wadler traces the source of his programming faith to the German logician Gerhard Gentzen (1909-1945). Gentzen followed in footsteps of Frege, both as a philosopher of symbolic logic and as an anti-Semite. Wadler must look past Gentzen's personal shortcomings to appreciate his intellectual contribution. Gentzen developed the idea of natural deduction and proof rules. (Wadler showed us page of inference rules using the notation o mathematical logic, and then asked for a show of hands to see if we understood the ideas and the notation on his slides. On his second question, enough of the audience indicated uncertainty that he slowed down to explain more. He said that he didn't mind the diversion: "It's a lovely story.") Next he showed the basics of simplifying proofs -- "great stuff", he old us, "at least as important as the calculus", something man had searched for thousands of years. Wadler's love for his faith was evident in the words he chose and the conviction with which he said them. Next came Alonzo Church, who did his work after Gentzen but still in the first half of the 20th century. Church gave us the lambda calculus, from which the typed lambda calculus was "completely obvious" -- in hindsight. The typed lambda calculus was all we needed to make the connection between logic and programming: a program is a proof, and a type is a proof term. This equivalence is demonstrated in the Curry-Howard isomorphism, named for the logician and computer scientist, respectively, who made the the connection explicit. In Wadler's view, this isomorphism predicts that logicians and computer scientists will develop many of the same ideas independently, discovered from opposite sides of the divide. This idea, that logic and programming are equivalent, is universal. In the movie, Independence Day, the good guys defeat the alien invaders by injecting a virus written in C into its computer system. The aliens might not have known the C programming language, and thus been vulnerable on that front, but they would have to have known the lambda calculus! Haskell: Type Classes The Hindley-Milner algorithm is named for another logician/computer scientist pair that made the next advance in this domain. They showed that even without type annotations an automated system can deduce the most general data types that make the program execute. The algorithm is both correct and complete. Wadler wanted to show us that this idea is so important, so beautiful, that he took a step to the side of his podium and jumped up and down! Much of Wadler's renown in the programming language derives from his seminal contributions to Haskell, a pure functional language based on Curry-Howard isomorphism and the Hindley-Milner algorithm. Haskell implements these ideas in the form of type classes. Wadler introduced this idea into the development of Haskell, but he humbly credited others for doing the hard work to make things work. Java: Adding Generics Java 1.4 was in many ways too simple. We had to use a List of some sort for almost everything, in order to have polymorphic structures. Trying to add C-style templates threatened to make things only worse. What the Java team needed was... the lambda calculus! (At this moment, Wadler stopped his talk Superman-style and took off his business suit to reveal his Lambda-man outfit. The crowd responded with hearty applause!) Philip Wadler as 'Lambda Man' Java generics have the same syntax as C++, but different semantics. (He added parenthetically that Java generics "have semantics".) The templates are merely syntactic sugar, rewritten into older Java in a technique called "erasure". The rewrite produces identical byte codes that a programmer's own Java might. Much was written about this language addition both before and after he it was made to the Java specification, and I don't want to get into that discussion. But, as Wadler notes, this approaches supports the evolution of the language in a smooth way, consistent with existing Java practice. Java generics also bear more than a passing resemblance to type classes, which means that it could evolve into something more different -- and more. Links: Reconciliation Web applications typically consist in three tiers: the browser, the server, and the database. All are typically programmed in different languages, such as HTML, CSS, JavaScript, Perl, and SQL. Wadler's newest language, Links, is intended to be one language used for all three tiers. It compiles to SQL for running directly against a database. Links is similar to the similar-sounding LINQ, a dynamic query language developed at Microsoft. The similarity is no coincidence -- one of its architects, Erik Meijer, came from Haskell community. Again, type classes figure prominently in Links. Programmers in the OO community can think of them in an OO way with no loss of understanding. But they may want to broaden their faith to include something more. Wadler closed his talk by returning to the themes with which he began: faith, evolution, and multiculturalism. He viewed the OOPSLA conference committee's inviting him to speak as a strong ecumenical step. "Faith is well and good", but he would like for computer science to make inroads helping us to make better decisions about language design and use. Languages like Links, implemented with different features and used in experiments, might help. -----