Portrait of Simon Peyton Jones

Simon Peyton Jones

Principal Researcher

About

Who I am and What I do

I’m a researcher at Microsoft Research in Cambridge, England. I started here in Sept 1998. I’m also an Honorary Professor of the Computing Science Department at Glasgow University, where I was a professor during 1990-1998.

I am married to Dorothy, a priest in the Church of England. We have six children (three adopted).

I’m interested in the design, implementation, and application of lazy functional languages. In practical terms, that means I spend a most of my time on the design and implementation of the language Haskell. In particular, much of my work is focused around the Glasgow Haskell Compiler, and its ramifications.

I co-supervise a number of PhD students at the Cambridge University Computer Lab. If you are interested in doing a PhD at Cambridge in my area, then I am very happy to discuss it with you.

A brief biography, suitable for seminar announcements and suchlike

Simon Peyton Jones, MA, FACM, FBCS, CEng, graduated from Trinity College Cambridge in 1980. After two years in industry, he spent seven years as a lecturer at University College London, and nine years as a professor at Glasgow University, before moving to Microsoft Research (Cambridge) in 1998.

Simon’s main research interest is in functional programming languages, their implementation, and their application. He was a key contributor to the design of the now-standard functional language Haskell, and is the lead designer of the widely-used Glasgow Haskell Compiler (GHC). He has written two textbooks about the implementation of functional languages.

More generally, Simon is interested in language design, rich type systems, compiler technology, code generation, runtime systems, virtual machines, and garbage collection. He is particularly motivated by direct use of principled theory to practical language design and implementation — that is one reason he loves functional programming so much.

Simon is also chair of Computing at School, the grass-roots organisation that was at the epicentre of the 2014 reform of the English computing curriculum.

Useful information and links

Haskell stuff

 

Papers

New Papers

  • [March 2016] Backpack to work: towards practical mixin linking for Haskell, with Edward Yang, Scott Kilpatrick, and Derek Dreyer.  Submitted to ICFP’16.
  • [March 2016] Non-recursive Make Considered Harmful, with Andrey Mokhov, Neil Mitchell, and Simon Marlow.   This paper describes a complete re-engineering of GHC’s build system using Shake instead of Make.  Submitted to ICFP’16.
  • [March 2016] Desugaring Haskell’s do-notation Into Applicative Operations, with Simon Marlow, Edward Kmett, and Andrey Mokhov.   Describes the ApplicativeDo language extension.  Submitted to ICFP’16.
  • [March 2016] Sequent calculus as a compiler intermediate language, with Paul Downen, Luke Maurer, and Zena Ariola.  This paper describes how to replace GHC’s Core language (based on lambda calculus) with a new one based on sequent calculus.  Submitted to ICFP’16.
  • [Jan 2016] A reflection on types, with Richard Eisenberg, Stephanie Weirich, and Dimitrios Vytiniotis, for Phil Wadler’s 60th birthday celebrations in April 2016.  This paper gives a tutorial introduction to the new type-indexed type representations that GHC supports (or will do soon), and the kind-equality technology that is necessary to support it.
  • [July 2015] Injective type families for Haskell, with Jan Stolarek and Richard Eisenberg, Haskell Symposium 2015.
  • [July 2015] GADTs meet their match: Pattern-matching warnings that account for GADTs, guards, and laziness, with Georgios Karachalias, Tom Schrijvers, and Dimitrios Vytiniotis. ICFP 2015.
  • [June 2014] Refinement types for Haskell, with Niki Vazou, Eric Seidel, Ranjit Jhala, Dimitrios Vytiniotis, ICFP 2014.  Here we describe Liquid Haskell, and in particular how to adapt refinement types for a lazy language.
  • [Apr 2014] Call arity, by Joachim Breitner.   This interesting new analysis is in GHC; Joachim implemented it during an internship at MSR.
  • [June 2014] Safe zero-cost coercions for Haskell, with Joachim Breitner, Richard Eisenberg, and Stephanie Weirich.  Describes the new Coercible mechanism that allows zero-cost coercions between deeply-nested newtypes.
  • [July 2013] Backpack: retrofitting Haskell with interfaces, with Scott Kilpatrick, Derek Dreyer and Simon Marlow.  An exploration of a mixin-module approach to separate modular development (SMD) for Haskell.  In submission.
  • [July 2013] Higher order cardinality analysis in theory and practice,with Ilya Sergy and Dimitrios Vytiniotis, describes an analysis that detects when a lambda is called at most once, or a thunk is used at most once, and shows how to exploit that information to generate better code. Much improved version 2! In submission.
  • [July 2013] Closed type families with overlapping equations, with Richard Eisenberg,Dimitrios Vytiniotis, and Stephanie Weirich.  In submission.
  • [May 2013] Computing at school  in the UK, with Simon Humphreys and Bill Mitchell; submitted to CACM.  This paper summarises the rapid and radical developments during 2012-2013 in the K-12 school computing curriculum in UK. We draw out lessons fromour experience that may be useful to others.
  • [May 2013] Call-by-need supercompilation, PhD thesis, Max Bolingbroke, Cambridge University, May 2013.  Max’s thesis summarises three years work on supercompilation as an optimisation technique. Lots of great insights.
  • [Apr 2013] Equality normalization for System FC, with Dimitrios Vytiniotis, describes how GHC optimses big coersions into little ones.  This turns out to be extremely important in practice; without the optimisation GHC can choke on type-function-rich programs.
  • [July 2013] Exploiting vector instructions with generalised stream fusion describes how Geoff made stream fusion work so well that we can write numerically intensive Haskell programs that run faster than their C equivalents. ICFP’13.
  • [Sept 2012] Bringing Computer Science Back Into Schools: Lessons from the UK, with Neil Brown, Michael Kolling, Tom Crick, Simon Humphreys, and Sue Sentance.  This paper tells the still-developing story of the UK’s Computing at School Working Group.
  • [July 2012] Vectorisation avoidance, with Gabriele Keller, Manuel Chakravarty, Roman Leshchinskiy, Ben Lippmeier, Haskell Symposium 2012.  Describes a major improvement to the “vectorisation transformation” in Data Parallel Haskell.
  • [July 2012] Safe Haskell, with David Terei, David Mazieres, and Simon Marlow, describes how to make Haskell safe enough to confine and safely execute untrusted, possibly malicious code.
  • [July 2012] HALO: Haskell to Logic through Denotational Semantics, with Dimitrios Vytiniotis, Koen Claessen, and Dan Rosen.  Describes how to translate Haskell and user-specified contract specifications into first order logic, and thereby prove that the program satisfies the contract.
  • [July 2012] Guiding parallel array fusion with index types, with Ben Lippmeier, Manuel Chakravarty, and Gabriele Keller, Haskell Symposium 2012.  This paper describes the Repa 3 array library, using indexed type families to control the data representation.
  • [May 2012] The Glasgow Haskell Compiler, in The Architecture of Open Source Applications, Volume II, ed Brown & Wilson. This paper gives an up to date (2012) technical overview of GHC.
  • [March 2012] Equality proofs and deferred type errors, with Dimitrios Vytiniotis and Pedro Magalhaes (ICFP12).  An exploration of what happens when you take equality proofs seriously in a compiler.  (A predecessor was our unpublished paper Practical aspects of evidence-based compilation in System FC, still available on the same URL as above.)
  • [March 2012] Work-efficient higher-order vectorisation, with Ben Lippmeir, Gabriele Keller, Manuel Chakravarty, and Roman Leshchinskiy (ICFP12).  It turns out that a naive application of the “vectorisation transformation” in Data Parallel Haskell can be asymptotically less efficient than the original program.  Bad news!  This paper describes how to fix the problem.
  • [Dec 2011] Closer to Nirvana a Channel 9 interview with Charles Torre.
  • [October 2011] Giving Haskell a promotion (with Brent Yorgey, Stepanie Weirich, Julien Cretin, and Dimitrios Vytiniotis).  How to (a) add kind polymorphism and (b) promote data types to become data kinds.  TLDI 2012.
  • [July 2011] Termination combinators forever (with Max Bolingbroke and Dimitrios Vytiniotis) describes a nice modular combinator library for doing online termination checking.  Very useful in a supercompiler, but with other applications too. Haskell Symposium, Tokyo, Sept 2011.
  • [June 2011] Multicore garbage collection with local heaps (principal author Simon Marlow), International Symposium on Memory Management, June 2011.
  • [May 2011] Parallel and concurrent programming in Haskell.  Simon Marlow’s 70-page Summer School tutorial.
  • [April 2011 (JFP final)] Modular type inference with local assumptions (with Dimitrios Vytiniotis, Tom Schrijvers, Martin Suzmann).  This epic 83-page JFP paper brings together, in a single uniform framework, a series of our earlier papers on type inference for type systems involving local constraints, including GADTs and indexed type families.  This is the camera ready copy for JFP.
  • [Mar 2011] Improving supercompilation: tag-bags, rollback, speculation, normalisation, and generalisation, with Max Bolingbroke. Max is on a roll; this paper describes the progress we have made in supercompilation since last year’s Haskell Symposium paper.  Rejected by ICFP’11.
  • [Mar 2011] Efficient Parallel Stencil Convolution in Haskell, with Ben Lippmeier, Gabriele Keller. This paper desribes (mainly) Ben’s adventures in applying Repa to a practical problem. New stuff includes a multi-region, cursored representation for arrays. Haskell Symposium 2011.
  • [June 2011] Towards Haskell in the cloud, with Jeff Epstein and Andrew Black.  Imitation is the sincerest form of flattery, and this paper does homage to Erlang. We try to combine Erlang’s best ideas with Haskell strong typing. On the way we describe a neat new approach to giving programmers control over serialisation for function closures. Haskell Symposium, Tokyo, Sept 2011.
  • [June 2011] A monad for deterministic parallelism, with Simon Marlow and Ryan Newton.  Using par/seq to write parallel Haskell programs can be frustrating; this paper explains why and offers a possible solution.  Haskell Symposium, Tokyo, Sept 2011.
  • [Mar 2011] Parallel = functional: the way of the future: slides (7Mbyte PDF), video.  A keynote talk at the London FP Exchange (18 March 2011), giving a whirlwind overview of what’s going on in the world of parallel Haskell.
  • [July 2010] Generative Type Abstraction and Type-level Computation (with Stephanie Weirich, Dimitrios Vytiniotis, and Steve Zdancewic).  This paper, which appeared in POPL’11, describes how to combine Haskell’s new abilities to do type-level computation with the old ability to do type abstraction using newtypes.  Rather surprisingly (to me) the two are in tension, and the solution is quite interesting.
  • [June 2010] Seq no more (by Simon Marlow, Patrick Maier, Phil Trinder, Hans-Wolfgang Loidl, and Mustafa Aswad).  A new take on the “algorithms + strategies = parallelism” story, providing a nice Haskell library to support parallel computation.  Haskell Symposium 2010 .
  • [June 2010] Supercompilation by evaluation (with Max Bolingbroke).  This is our first foray into supercompilation.  To appear at the 2010 Haskell Symposium.
  • [June 2010] The performance of Haskell ‘containers’ package (by Milan Straka).  Milan did this work while an intern here at MSR Cambridge.  Haskell Symposium 2010.
  • [April 2010] Hoopl: A Modular, Reusable Library for Dataflow Analysis and Transformation (with John Dias and Norman Ramsey). This paper, completely rewritten in April 2010, describes our framework for doing dataflow optimisation on imperative C– programs. Haskell Symposium 2010.
  • [April 2010] Regular, shape-polymorphic, parallel arrays in Haskell (with Manuel Chakravarty, Gabriele Keller, Roman Leshchinskiy, and Ben Lippmeier) describes a high-performance data-parallel library for regular arrays. To appear at ICFP 2010.
  • [Oct 2009] Let should not be generalised, with Dimitrios Vytiniotis and Tom Schrijvers. This paper argues that local let-bindings should not be generalised: although taken for granted, it is a feature that is seldom used, and it greatly with recent type-system developments, such as GADTs and type functions. Appeared at TLDI 2010.
  • [May 2009] Types are calling conventions (with Max Bolingbroke), and its discussion page. Describes an intermediate language that supports much more precise calling conventions than GHC’s current Core language. Haskell Symposium 2009.

About Haskell generally

Compiler stuff

Papers about parallelism in Haskell

Papers about Software Transactional Memory

(with Tim Harris, Maurice Herlihy, and Simon Marlow). This series of papers about transactional memory in Haskell, describes a new coordination mechanism for concurrent programs.

Papers about types

  • [May 2009] Fun with type functions (with Ken Shan, and Oleg Kiselyov). A tutorial on indexed type families, and associated types in Haskell. Channel 9 video of the talk: http://channel9.msdn.com/posts/MDCC-TechTalk-Fun-with-type-functions
  • [March 2009] Complete and Decidable Type Inference for GADTs (with Tom Schrijvers, Martin Sulzmann, and Dimitrios Vytiniotis), ICFP’09. Yes, it’s another a stab at type inference for GADTs, but I think a great improvement on our previous attempt.
  • [April 2008] FPH : First-class Polymorphism for Haskell ( with Dimitrios Vytiniotis and Stephanie Weirich), submitted to ICFP 2008. This is a completely new paper, much better than our old “boxy type” paper (although you’ll still see boxes in it).
  • [April 2008] Type Checking with Open Type Functions, (with Tom Schrijvers, Manuel Chakravarty, Martin Sulzmann), submitted to ICFP’08. This is a much more thorough look at the challenge of type checking in the presence of open type functions.
  • [April 2007] Scrap your type applications, Barry Jay and Simon Peyton Jones. Have you ever thought that the type applications in System F are verbose and often redundant? Here’s a possible way to get rid of (most of) them.
  • [Sept 2007] Towards open type functions for Haskell, Tom Schrijvers, Martin Sulzmann, Simon Peyton Jones, and Manuel Chakravarty, submitted to the Implementing Functional Languages workshop, Sept 2007 (IFL07).
  • [Apr 2006] System F with Type Equality Coercions (with Martin Sulzmann and Manuel Chakravarty). This paper describes System FC, a modest extension to System F that can accommodate GADTs, associated types, and functional dependencies. GHC now uses FC as its intermediate language. (Rejected by ICFP’06; revised; rejected by POPL’07; revised again; submitted to TLDI’07.)
  • [Revised (again) April 2006] Simple unification-based type inference for GADTs (with Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn), ICFP’06. This is a completely-rewitten and much-simplified verison of our orignal “wobbly-type” paper. It has been rewritten from beginning to end so, if you liked the earlier paper, this one is probably worth reading too. The big recent change is the idea of a “fresh most general unifier”.
  • [Revised April 2006] Boxy types: type inference for higher-rank types and impredicativity (with Dimitrios Vytiniotis and Stephanie Weirich); ICFP’06. It is also now fully implemented in GHC.
  • [Revised Feb 2006] Understanding functional dependencies via Constraint Handling Rules, Martin Sulzmann, Gregory J. Duck, Simon Peyton Jones, and Peter J. Stuckey. To appear in the Journal of Functional Programming.
  • [Revised Feb 2006] Practical type inference for arbitrary-rank types (with Stephanie Weirich, Dimitrios Vytiniotis, Mark Shields), to appear in the Journal of Functional Programming. Long in gestatation, the paper describes the approach that GHC takes to type inference for higher-rank types. It has a strongly tutorial flavour, and comes with an executable implementation.
  • [April 2005] Associated type synonyms (with Manuel Chakravarty and Gabrielle Keller). Our earlier paper discussed allowing data type declarations in type-class signatures. This follow-up (submitted to ICFP’05) suggests allowing type synonyms too.

Static verification of Haskell programs

[July 2008]Static contract checking for Haskell, (with Dana Xu and Koen Claessen), submitted to POPL 2009. This paper describes progress on static verification of Haskell programs.

Other papers

Social networks

I use LinkedIn for professional networking, but I restrict my connections to people who I know personally, or with whom I have had some meaningful two-way professional interaction; that is, not simply people with whom I share a professional interest.

I use Facebook for non-work networking, but only for people who my family knows too.

I do have a Twitter account, for some reason, but I have yet to find something significant enough to say that it’s worth tweeting.

In all three cases my actual use is minimal, so don’t hold your breath.

Publications

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2002

2001

1999

1996

1995

1994

1993

1991

1986

Projects