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.
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?
Thank you to the crew at Type Theory for All for their thoughtful and well-prepared interview.
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
_ == _ = FalseWe 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 = FalseIn 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 = FalseAnd 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 = FalseAnd 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 -> awhich 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 xwould 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 xOn 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 xOne 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?
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.
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.
Philip Wadler is a man who wears many different hats. Both literally: fedoras, trilbys, even the occasional straw hat, and metaphysically: recently retired Professor of theoretical computer science at the University of Edinburgh; Fellow of the Royal Society; senior researcher at the blockchain infrastructure company IOHK; Lambda Man; often-times favourite lecturer of the first year computer science students; and, occasionally, stand-up comedian. It is the latter role that leads me to ask Phil if he will participate in a Q&A.[Previous post repeated below.]
Brave New BullshitIn an AI era, who wins and who loses?
Your future workday might look like this:Will AI help you to do your job or take it from you? Is it fair for AI to be trained on copyrighted material? Will any productivity gains benefit everyone or only a select few? Join Professor Philip Wadler’s talk as he looks at the hopes and threats of AI, exploring who wins and who loses.
- You write bullet points.
- You ask a chatbot to expand them into a report.
- You send it to your boss ...
- Who asks a chatbot to summarise it to bullet points.
[Reposting with update.]Brave New BullshitIn an AI era, who wins and who loses?
Your future workday might look like this:Will AI help you to do your job or take it from you? Is it fair for AI to be trained on copyrighted material? Will any productivity gains benefit everyone or only a select few? Join Professor Philip Wadler’s talk as he looks at the hopes and threats of AI, exploring who wins and who loses.
- You write bullet points.
- You ask a chatbot to expand them into a report.
- You send it to your boss ...
- Who asks a chatbot to summarise it to bullet points.
A powerful op-ed by Gabor Maté in the Toronto Star.
Just as nothing justifies the atrocities of October 7, nothing about October 7 justifies Israeli atrocities against the Palestinians, either before or since October 7. Recently, I listened to orthopedic surgeon Dr. Deirdre Nunan, like me a graduate of UBC’s Faculty of Medicine, recount her harrowing experiences serving in a Gaza hospital under the siege that followed Israel’s breaking of the ceasefire in March. Her depictions of unspeakable horror, enacted as policy by one of the world’s most sophisticated militaries, were soul shattering. Many other physicians — Canadian, American, Jewish, Muslim, Christian — who have worked in Gaza speak in similar terms. British doctors describe witnessing “a slaughterhouse.” All their testimonies are widely accessible. The leading medical journal Lancet editorialized that in its assault on health care facilities and personnel in Gaza, “the Israeli Government has acted with impunity … Many medical academies and health professional organizations that claim a commitment to social justice have failed to speak out.” ...
It may be true that antisemitic animus can lurk behind critiques of Zionism. But in my decades of advocacy for Palestinian rights including medical visits to Gaza and the West Bank, I have rarely witnessed it. When present, it has a certain tone that one can feel is directed at Jewishness itself, rather than at the theory and practice of Zionism or at Israel’s actions. What is far more common and genuinely confusing for many is that Israel and its supporters, Jews and non-Jews, habitually confound opposition to Israeli policy with antisemitism. This is akin to Vietnam War protesters being accused of anti-Americanism. How is opposing the napalming of human beings anti-American or, say, deploring Israel’s use of mass starvation as a weapon of war in any sense anti-Jewish? ...
People deserve the right to experience as much liberty to publicly mourn, question, oppose, deplore, denounce what they perceive as the perpetration of injustice and inhumanity as they are, in this country, to advocate for the aims and actions of the Israeli government and its Canadian abettors amongst our political leadership, academia, and media.
Even if we feel powerless to stop the first genocide we have ever watched on our screens in real time, allow at least our hearts to be broken openly, as mine is. And more, let us be free to take democratic, non-hateful action without fear of incurring the calumny of racism.
Thanks to a colleague in the Scottish Universities Jewish Staff Network for bringing it to my attention.
An intriguing talk by Gabriella Gonzalez, delivered at Haskell Love 2020. Based largely on the famous marketing book, Crossing the Chasm. Gonzalez argues that marketing is not about hype, it is about setting priorities: what features and markets are you going to ignore? The key to adoption is to be able to solve a problem that people need solved today and where existing mainstream tools are inadequate. Joe Armstrong will tell you that the key to getting Erlang used was to approach failing projects and ask "Would you like us to build you a prototype?" Gonzalez makes a strong case that Haskell should first aim to capture the interpreters market. He points out that the finance/blockchain market may be another possibility. Recommended to me at Lambda Days by Pedro Abreu, host of the Type Theory Forall podcast.
Following two sell-out shows at the Fringe last year, I'm on at the Fringe again:
As a new student at the uni, Philip Wadler was the first introductory lecture I had, and his clear passion for the subject made me feel excited to begin my journey in computer science. In particular he emphasised the importance of asking questions, which made the idea of tutorials and lectures a lot less intimidating, and went on to give really valuable advice for starting university. I enjoyed this session so much, and so was looking forward to the guest lectures he was going to do for Inf1A at the end of semester 1. They certainly did not disappoint, the content he covered was engaging, interesting, and above all very entertaining to listen to, especially when he dressed up as a superhero to cement his point. Because I found these talks so rewarding, I also attended the STMU that he spoke at about AI and ChatGPT, and everyone I talked to after the event said they had a really good time whilst also having a completely new insightful perspective on the topic. In summary, Philip Wadler has delivered the best lectures I have attended since starting university, and I have gotten a lot out of them.
Thank you, anonymous first-year student!
I'm part of the programme committee for Lambda Days, and I’m personally inviting you to submit your talk!
Lambda Days is all about celebrating the world of functional programming, and we’re eager to hear about your latest ideas, projects, and discoveries. Whether it’s functional languages, type theory, reactive programming, or something completely unexpected—we want to see it!
Submission Deadline: 9 February 2025
Never spoken before? No worries! We’re committed to supporting speakers from all backgrounds, especially those from underrepresented groups in tech.
Submit your talk and share your wisdom with the FP community.
From my colleague, John Longley, a treat.
‘Informatics Lecturer Song’
(Based on Gilbert and Sullivan’s ‘Major General song’)
John Longley
Happy Election Day!
The above shows an average of five recent polls for my constituency, Edinburgh North and Leith, and comes courtesy of Stop the Tories. Clearly, the Tories have no chance, but I will still be voting tactically. I am a member of the Greens. But if everyone who intends to vote Green instead votes SNP, the SNP will beat Labour (rather than the other way around). While the SNP has made some awful missteps of late, they are the best hope to push Labour toward the more progressive policies from which Starmer has dragged them away. My tactical vote goes to the SNP.
I'm looking forward to speaking in Lisbon.
On June 4, Professor Philip Wadler will give an INESC-ID Distinguished Lecture organized in the scope of the BIG ERA Chair Project, titled “(Programming Languages) in Agda = Programming (Languages in Agda)”.
Registration: here (free but mandatory)
Date: June 4, 2024
Time: 15h00-16h15
Where: Anfiteatro Abreu Faro – Complexo Interdisciplinar, Instituto Superior Técnico (Alameda)
Abstract: The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. Proof by induction is just programming by recursion. Finding a proof becomes as fun as hacking a program. Dependently-typed programming languages, such as Agda, exploit this pun. This talk introduces *Programming Language Foundations in Agda*, a textbook that doubles as an executable Agda script—and also explains the role Agda plays in IOG’s Cardano cryptocurrency.
I am delighted to have made this list. Lesley Lamport and John Reynolds also appear on it, but at positions lower than mine, and Tony Hoare and Robin Milner don't appear at all---so perhaps their methodology needs work.
Congratulations on being named an inaugural Highly Ranked Scholar by ScholarGPS
I'll be appearing at the Fringe in the Cabaret of Dangerous Ideas, 12.20-13.20 Monday 5 August and 12.20-13.20 Saturday 17 August, at Stand 5. The 5 August show is joint with Matthew Knight of the National Museums of Scotland, the 17 August show is all mine. Both shows are hosted by comedian Susan Morrison.
You can book either via the Fringe or via the Stand. If one is sold out, try the other.
Here's the brief summary:
Chatbots like ChatGPT and Google's Gemini dominate the news. But the answers they give are, literally, bullshit. Historically, artificial intelligence has two strands. One is machine learning, which powers ChatGPT and art-bots like Midjourney, and which threatens to steal the work of writers and artists and put some of us out of work. The other is the 2,000-year-old discipline of logic. Professor Philip Wadler (The University of Edinburgh) takes you on a tour of the risks and promises of these two strands, and explores how they may work better together.I'm looking forward to the audience interaction. Everyone should laugh and learn something. Do come!
I'm looking forward to Lambda Days 2024 and catching up with friends in Krakow.
A sensible proposal in The Atlantic from philosopher Daniel Dennett. Is anyone campaigning for a law or regulation to this effect?
Creating counterfeit digital people risks destroying our civilization. Democracy depends on the informed (not misinformed) consent of the governed. By allowing the most economically and politically powerful people, corporations, and governments to control our attention, these systems will control us. Counterfeit people, by distracting and confusing us and by exploiting our most irresistible fears and anxieties, will lead us into temptation and, from there, into acquiescing to our own subjugation.
There may be a way of at least postponing and possibly even extinguishing this ominous development, borrowing from the success—limited but impressive—in keeping counterfeit money merely in the nuisance category for most of us (or do you carefully examine every $20 bill you receive?).
As [historian Yuval Noah] Harari says, we must “make it mandatory for AI to disclose that it is an AI.” How could we do that? By adopting a high-tech “watermark” system like the EURion Constellation, which now protects most of the world’s currencies. The system, though not foolproof, is exceedingly difficult and costly to overpower—not worth the effort, for almost all agents, even governments. Computer scientists similarly have the capacity to create almost indelible patterns that will scream FAKE! under almost all conditions—so long as the manufacturers of cellphones, computers, digital TVs, and other devices cooperate by installing the software that will interrupt any fake messages with a warning.
