Wadler's Blog

Sky Welch's Fractal Maps updates Alasdair Corbett's Mandelbrot Maps. It renders faster, and displays the two curves side-by-side (rather than displaying one large and one tiny). Mandelbrot Maps is the most popular Mandelbrot app in Google Play, with over 10,000 downloads. I expect Fractal Maps to catch up soon. Try it today! (Disclaimer/boast: both Sky and Alasdair produced their software as part of UG4 projects under my supervision.)

Labels: Graphics, Mathematics, Recursion

I'm performing at Bright Club, Edinburgh, Tuesday 28 April at The Stand. Doors open 7:30, show begins 8:30. See you there! Details, tickets £5.

Labels: Comedy, Computing

The Prime Minister of Singapore, Lee Hsien Loong, plans to learn Haskell.

My children are in IT, two of them – both graduated from MIT. One of them browsed a book and said, “Here, read this”. It said “Haskell – learn you a Haskell for great good”, and one day that will be my retirement reading.

Spotted by Jeremy Yallop.

Labels: Functional Programming, Haskell, Programming Languages

Via @ReifyReflect (Sam Lindley) and @PedalKings. Previously: Multiple inheritance.

Labels: Object-Oriented

A complement to blame
Philip Wadler.
SNAPL, May 2015.

Contracts, gradual typing, and hybrid typing all permit less-precisely typed and more-precisely typed code to interact. Blame calculus encompasses these, and guarantees blame safety: blame for type errors always lays with less-precisely typed code. This paper serves as a complement to the literature on blame calculus: it elaborates on motivation, comments on the reception of the work, critiques some work for not properly attending to blame, and looks forward to applications. No knowledge of contracts, gradual typing, hybrid typing, or blame calculus is assumed.

Labels: Functional Programming, Programming Languages, Types

Blame and Coercion:Together Again for the First Time
Jeremy Siek, Peter Thiemann, Philip Wadler.
PLDI, June 2015.

C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop three calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are: λB, based on the blame calculus of Wadler and Findler (2009); λC, inspired by the coercion calculus of Henglein (1994); λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006) and the threesome calculus of Siek and Wadler (2010). While λB is little changed from previous work, λC and λS are new. Together, λB, λC, and λS provide a coherent foundation for design, implementation, and optimisation of gradual types.

We define translations from λB to λC and from λC to λS. Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: λC has a particularly simple definition, and the subtle definition of blame safety for λB is justified by the simple definition of blame safety for λC. Our calculus λS is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from λC to λS to validate the challenging part of full abstraction between λB and λC; and, second, using full abstraction from λB to λS to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.

Labels: Functional Programming, Programming Languages, Types

Aleks Krotoski tackles programming languages in BBC Radio 4's Codes that Changed the World. The five episodes comprise: Fortran, Cobol, Basic, Java, and The Tower of Babel. Functional programming and Haskell are singled out for special attention in the final programme, which includes a interview with Haskell developer Elise Huard; online is a clip of interview with Simon Peyton Jones that did not make it on air.

Labels: Computing, Functional Programming, Haskell, Java, Programming Languages

An article on programming languages aimed at a general readership, from MIT Technical Review. Spotted by De Lesley Hutchins.

When the Japanese computer scientist Yukihiro Matsumoto decided to create Ruby, a programming language that has helped build Twitter, Hulu, and much of the modern Web, he was chasing an idea from a 1966 science fiction novel called Babel-17 by Samuel R. Delany. At the book’s heart is an invented language of the same name that upgrades the minds of all those who speak it. “Babel-17 is such an exact analytical language, it almost assures you technical mastery of any situation you look at,” the protagonist says at one point. With Ruby, Matsumoto wanted the same thing: to reprogram and improve the way programmers think....When I meet Yaron Minsky, Jane Street’s head of technology, he’s sitting at a desk with a working Enigma machine beside him, one of only a few dozen of the World War II code devices left in the world. I would think it the clear winner of the contest for Coolest Secret Weapon in the Room if it weren’t for the way he keeps talking about an obscure programming language called OCaml. Minsky, a computer science PhD, convinced his employer 10 years ago to rewrite the company’s entire trading system in OCaml.

Labels: Functional Programming, Programming Languages

The UCU has lain down its placards and ended the strike to avoid cuts to pensions. Our one remaining hope is for members to make their outrage known in the USS consultation exercise, which ends 22 May 2015. I hope everyone with a USS pension will respond. Suggested responses from UCU Left and UCU are linked; please comment below, especially to list other suggested responses.

Universities UK argue that the reductions are necessary to avoid a deficit, but their claim has been widely criticised. A group of prominent statisticians point out Universities UK inflated the deficit by assuming a buoyant economy when predicting future salaries but assuming a recession when predicting investment returns.

In 2011, Universities UK imposed vastly reduced pensions on new hires. Old hires who pay into the pension fund for forty years receive a pension of one-half their final salary; new hires who do the same receive a pension of one-half their average salary. Basing pensions on average rather than final salary may be sensible, but to do so with no little or no adjustment in multiplier suggests employers used this as an excuse to slip in a large cut; new hires receive about 2/3 the benefits received by old hires. All staff also suffered other cuts to pensions: additional caps and less good adjustment for inflation. At the time, it was predicted that within a few years old hires would be moved to the inferior scheme for new hires, and that is what has now come to pass.

Like many in USS, employees and employers alike, I am concerned that the changes will make UK academia a less attractive option for potential scholars.

Labels: Academia, Politics, UK, University