Professor Emeritus

After retiring last July, the University Senate have approved my emeritus status. I'm grateful to Julian Bradfield for his work drafting the generous minute that accompanied the approval.

Special Minute

Professor Philip Wadler BSc, MSc, PhD, FRSE, FACM, FRS

Emeritus Professor of Theoretical Computer Science

We are pleased to nominate Professor Philip Wadler for the title of Emeritus Professor at the University of Edinburgh. Professor Wadler is a popular educator and has had an extensive career in both academia and industry, with seminal contributions to the field of computer science, particularly in the theory and practice of programming languages. Philip Wadler obtained a BSc with honours in mathematics from Stanford University in 1977, followed by a MSc and PhD in computer science in 1979 and 1984 from Carnegie-Mellon University. He took up a postdoc at Oxford University, and in 1987 he was appointed as a lecturer at the University of Glasgow. In 1996, Phil switched to industry, working at Bell Labs and Avaya Labs. He returned to academia in 2003, taking up the Chair of Theoretical Computer Science at the University of Edinburgh.

Professor Wadler’s research centres on the theory and practice of programming languages. He served as first editor of the Haskell report, and introduced what are arguably its two main innovations, type classes and monads. Haskell saw widespread use, and type classes and monads were adopted by a wide variety of other programming languages and proof assistants. He contributed to the design of the programming language Java, and introduced a model of it widely used by researchers. By influencing the design of popular programming languages, Phil has had a profound impact not only on programmers, but also on the users of the systems those programmers build. If you’ve used Facebook or X, Android or iPhone, you’ve run code that exploits concepts Phil pioneered.

Professor Wadler has published many seminal monographs and textbooks throughout his illustrious career. His contribution has been honoured in many ways. He served as chair of the ACM Special Interest Group on Programming Languages (SIGPLAN) from 2009–2012 and received its Distinguished Service Award in 2016. He was appointed a Fellow of the Royal Society of Edinburgh in 2005, a Fellow of the Association for Computing Machinery in 2007, and a Fellow of the Royal Society in 2022. He regularly delivers keynotes at both academic and developer conferences. In 2016, his sixtieth birthday was marked by a two-day Wadlerfest, and an accompanying festschrift published by Springer.

Phil is a passionate and popular teacher. On moving to Edinburgh in 2003, he introduced a first-year programming languages course based on Haskell and was shortlisted for the EUSA Teaching Award (Overall Best Performer) in 2009. His Honours courses on programming language theory have been among the most popular theoretical courses. Phil is widely known for theatrical performance and applies this talent outside academia, often performing stand- up comedy via Bright Club, and appeared in the Fringe via the Cabaret of Dangerous Ideas in 2024.

Since 2017, Phil has worked closely with industry, including consulting for IOG where he helped to design the smart contract system for its Cardano blockchain and applied formal methods to ensure its reliability. After retirement from Edinburgh, he plans to write a version of his online text for the proof assistant Agda updated to the proof assistant Lean. He will appear again this summer at the Fringe.

To conclude, Professor Philip Wadler's career is characterised by groundbreaking research, impactful teaching, and significant professional service. His work has shaped the landscape of programming languages and computer science education. Conferring the title of Emeritus Professor on Professor Wadler would honour his substantial contributions to the University of Edinburgh and the broader scientific community.

A good life for the 99% isn’t a pipe dream: it can be done. Here’s how

Thomas Piketty is at it again. He and his colleagues at the World Inequality Lab have produced a report outlining, with quantitative modelling, what a just world might look like and how to get there. A summary appears in the Guardian, and their full report is online.

Imagine a future in which everyone enjoys high levels of wellbeing; where 90% of the world’s population doubles their income but works half the hours we work today. A world in which the bottom half of humanity sees its share of global wealth rise from just 2% today to 30%; a world where we consume enough, but nobody over-consumes. And imagine achieving this on a planet that can comfortably sustain human life without its climate breaking down.

Against the bleak techno-authoritarian futures now being sold to us, a radical new vision for global progress in the 21st century feels urgently needed. ...

What would this transition deliver? At its heart is convergence between countries. Average per capita national income, today separated by a 16-fold gap between the poorest (€290 a month in sub-Saharan Africa) and richest (€4,590 in North America/Oceania) regions of the world, would rise towards a common level of about €5,000 a month in all countries by 2100.

But this convergence is not just monetary. Annual working hours per employed person would fall from roughly 2,100 to about 1,000, continuing the long shift towards shorter working time; while the share of global working hours devoted to education and health would rise from 11% to 43%. Women and men would converge on equal pay and on an equal share of economic and domestic labour.

All of this would unfold within a habitable climate. Thanks to sustainable convergence and fast decarbonisation, global heating would reach 1.8C, against more than 4C on current trends.

None of this will be possible without a deep contraction of inequality. The income scale between individuals would narrow to a ratio of one to five and the wealth scale to one to 10, prolonging what western and Nordic Europe achieved over the 20th century. The share of global wealth held by the poorest half of humanity would rise from 2% to 30%, while the share held by the billionaire class would fall from 6% to 0.05%.

Smaller, cheaper Plutus scripts with the UPLC command-line tool

If you want to see a use of Agda in real life, to provide certificates validating the correctness of compiler passes, check out this blog post from my colleague Ziyang Liu at Input Output. A simplified description of one of the passes appears in A Tale of Two Zippers, by myself, Jacco Krijnen, and Ramsay Taylor.

Wet Sidewalks and Odd Numbers

Phil Crissman explains Propositions as Types with a dialogue between Achilles and the Tortoise, in the style of Douglas Hofstadter (who in turn was inspired by Lewis Carrol). Lambda Man makes an appearance.

Maybe Don’t Talk to the New York Times About Zohran Mamdani

Peter Coviello explains how the New York Times enables right-wing billionaires to push their agenda.

Like so many other bits of Times coverage, the whole of the piece is structured as an orchestrated encounter. Some people say this; however, others say this. It’s so offhand you can think you’re gazing through a pane of glass. Only when you stand a little closer, or when circumstances make you a little less blinkered, do you notice the fact which then becomes blinding and finally crazymaking, which is just that there is zero, less than zero, stress put on the relation between those two “sides,” or their histories, or their sponsors, or their relative evidentiary authority, or any of it. Instead, what you get is a piece making the various more or less bovine noises of studious grey-lady impartiality, with the labor of anything resembling “appraisal” surgically excised.

... [W]hat this sort of reporting ultimately means is that if you have enough money to get somebody, anybody, to produce a white paper for you, which you can then put on some think-tank stationery? Then, my friend, you are ready to enter into the rushing current of elite reportage. For no matter how unhinged the position you’ve taken, or paid someone marginally credentialed to sketch out on your behalf—“Can Woman Think?: We Investigate,” “Is the Negro a Man: A Reconsideration”—that opinion will, by virtue of such provenance, possess all needed evidentiary gravity for the Times. And then some. (Only yesterday the Times ran this actual story, which is not parody.)

 George Monbiot points out that the same forces are in action at the BBC.

This also describes the BBC’s understanding of “impartiality”. While it no longer provides a platform for outright climate denial, almost every day it breaks its own editorial guidelines by hosting Tufton Street junktanks (which often argue against environmental action) without revealing who funds them. Shouldn’t we be allowed to know whether or not they are sponsored by fossil fuel companies?

Type Theory for All: The Goal of Science is to Communicate Ideas

 

Thank you to the crew at Type Theory for All for their thoughtful and well-prepared interview.

Curious: Brave New Bullshit

Haskell equations, thirty-eight years later

One night, while drifting off to sleep (or failing to), I solved a conundrum that has puzzled me since 1987.

Before Haskell there was Orwell. In Orwell equations were checked to ensure order is unimportant (similar to Agda today). When an equation was to match only if no previous equation applied, it was to be preceded by ELSE. Thus, equality on lists would be defined as follows:

    (==) :: Eq a => [a] -> [a] -> Bool
    [] == []          =  True
    (x:xs) == (y:ys)  =  x == y && xs == ys
    ELSE
    _ == _            =  False

We pondered whether to include this restriction in Haskell. Further, we wondered whether Haskell should insist that order is unimportant in a sequence of conditionals, unless ELSE was included. Thus, equality on an abstract type Shape would be defined as follows:

    (==) :: Shape -> Shape -> Bool
    x == y | circle x && circle y  =  radius x == radius y
           | square x && square y  =  side x == side y
    ELSE
           | otherwise             =  False

In Orwell and early Haskell, guards were written at the end of an equation and preceded by the keyword if or the end of an equation could be labelled otherwise. (Miranda was similar, but lacked the keywords.) Here I use the guard notation, introduced later by Paul Hudak, where otherwise is a variable bound to True.

Sometime two equations or two guards not separated by ELSE might both be satisfied. In that case, we thought the semantics should ensure that both corresponding right-hand sides returned the same value, indicating an error otherwise. Thus, the following:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x     =  y
             | zero y     =  x
    ELSE
             | otherwise  =  ...

would be equivalent to:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x && zero y && x == y    =  x
             | zero x && zero y && x /= y    =  error "undefined"
             | zero x && not (zero y)        =  y
             | not (zero x) && zero y        =  x
             | not (zero x) && not (zero y)  =  ...

Here the code checks that if x and y are both zero then they are the same. (I will consider a refinement to the check for sameness later.) Of course, the compiler would issue code that performs the tests zero x, zero y, and x == y at most once.

We didn’t pursue this design in Haskell for two reasons. First, because we thought it might be too unfamiliar. Second, because the ELSE on a line by itself was syntactically awkward. It would be especially annoying if one ever wanted the usual cascading behaviour:

    f :: Thing -> Thing
    f x | p x  =  ...
    ELSE
        | q x  =  ...
    ELSE
        | r x  =  ...

Here each guard is tested in turn, and we take the first that succeeds.

Today, the first problem is perhaps no longer quite so strong an issue. Many applications using Haskell would welcome the extra assurance from flagging any cases where order of the equations is significant. But the syntactic awkwardness of ELSE remains considerable. It was syntax about which I had an insight while tossing in bed.

Above otherwise is a variable bound to True in the standard prelude. But say we were to treat otherwise as a keyword, and to give it the meaning that the equation applies only if no previous equation applies, and to allow it to optionally be followed by a further guard. Then our first example becomes:

    (==) :: Eq a => [a] -> [a] -> Bool
    [] == []            =  True
    (x:xs) == (y:ys)    =  x == y && xs == ys
    _ == _ | otherwise  =  False

And our second example becomes:

    (==) :: Shape -> Shape -> Bool
    x == y | circle x && circle y  =  radius x == radius y
           | square x && square y  =  side x == side
           | otherwise             =  False

And our third example becomes:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x     =  y
             | zero y     =  x
             | otherwise  =  ...

If one doesn’t want to invoke the equality test in the case that both zero x and zero y hold then one would instead write:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x            =  y
             | otherwise zero y  =  x
             | otherwise         =  ...

Similarly, the cascading example becomes:

    f :: Thing -> Thing
    f x | p x            =  ...
        | otherwise q x  =  ...
        | otherwise r x  =  ...

That’s it! The syntactic awkwardness is greatly reduced.

The proposed notation depends upon Paul’s clever insight to move the guard from the end of the equation to the middle, so evaluation works strictly left to right. But we’ve had guards in that position for quite a while now. Goodness knows why none of us hit upon this proposal thirty-odd years ago.

Of course, the change is not backward compatible. Changes to guards could be made backward compatible (with added ugliness) by using a different symbol than ‘|’ to mark guards with the new semantics. But now the old definition of (==) should not be accepted without an otherwise, and I cannot think of how to introduce that new semantics with a backward compatible syntax.

The solution, as with so much of Haskell nowadays, is to activate the new semantics with a pragma. Manual porting of legacy code would not be hard in most cases, and it would also be easy to write a tool that adds otherwisewhenever the equations are not easily shown to be independent of order.

John Hughes suggests a further refinement to the above. Using equality to check that the value of two equations is the same may not be appropriate if the values are computed lazily. Instead, he suggests that the plus example should translates as follows:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x && zero y              =  x `meet` y
             | zero x && not (zero y)        =  y
             | not (zero x) && zero y        =  x
             | not (zero x) && not (zero y)  =  ...

Here we presume a type class

    class Meet a where
      meet : a -> a -> a

which confirms that the two arguments are the same and returns a value that is the same as both the arguments. For strict data types, two arguments are the same if they are equal.

    instance Meet Integer where
      x `meet` y | x == y     =  x
                 | otherwise  =  error "undefined"

For lazy data types, we check that they are the meet lazily.

    instance Meet a => Meet [a] where
      [] `meet` []           =  []
      (x:xs) `meet` (y:ys)   =  (x `meet` y) :: (xs `meet` ys)
      meet _ _  | otherwise  =  error "undefined"

If the compiler could not verify that equations are disjoint, it would require that their right-hand sides have a type belonging to the class Meet.

In most cases, one would hope the compiler could verify that equations are disjoint, and hence would not have to resort to meet or additional checks. One might wish to allow a pragma to declare disjointness, permitting the compiler to assume, for instance, that x < y and x >= y are disjoint. An SMT solver could do much of the work of checking for disjointness.

In general, equations not separated with otherwise would be checked to ensure they are disjoint or all give equivalent results. For example,

    g :: Thing -> Thing
    g x | p x             =  a x
        | q x             =  b x
        | otherwise r x   =  c x
        | s x             =  d x
        | otherwise t x   =  e x

would be equivalent to

    g :: Thing -> Thing
    g x | p x && q x              =  a x `meet` b x
        | p x && not (q x)        =  a x
        | q x && not (p x)        =  b x
        | otherwise r x && s x    =  c x `meet` d x
        | r x && not (s x)        =  c x
        | s x && not (r x)        =  d x
        | otherwise t x           =  e x

On the other hand, if we declared that p x and q x are disjoint, and the same for s x and r x, then the first code would instead compile to something equivalent to Haskell’s current behaviour,

    g :: Thing -> Thing
    g x | p x             =  a x
        | otherwise q x   =  b x
        | otherwise r x   =  c x
        | otherwise s x   =  d x
        | otherwise t x   =  e x

One drawback of this proposal is that the source code doesn’t directly indicate when extra tests and the use of meet are required. An IDE might provide feedback to make explicit which tests are performed, or one might also add pragmas or additional syntax to reflect that information in the source.

I hope some reader might be keen to take this forward. What do you think?

Translation Table

I remember seeing a version of the above in High School. My favourite entries, which I quote to this day, are

"... accidentally strained during mounting" --> "... dropped on the floor"

"... handled with extreme care throughout the experiments" --> "... not dropped on the floor"

and

"correct within an order of magnitude" --> "wrong"

From Futility Closet. Spotted via Boing Boing.

Why are we funding this?

 

In the face of swinging funding cuts in the US, David Samuel Shiffman defends the value of scientific curiosity in American Scientist. Spotted via Boing Boing.