TITLE: OOPSLA Day 3: Philip Wadler on Faith, Evolution, and Programming Languages
AUTHOR: Eugene Wallingford
DATE: October 28, 2006 7:36 PM
DESC:
-----
BODY:
"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!)
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.
-----