Tomas Petricek

Writing about practical F# coding and programming language research

Tomas Petricek @ Computer Lab

I'm a third (final) year PhD Student in the Computer Laboratory at the University of Cam­bridge and a member of the Programming, Logic and Semantics Group. My supervisors are Alan Mycroft from the Computer Lab and Don Syme. Before joining the Computer Laboratory, I studied at the Faculty of Mathematics and Physics in Prague and I did two internships at Microsoft Research. I also did an internship at BlueMountain Capital, working on data science library Deedle.

I'm an active member of the F# community, I often speak at various industry events and user groups, I wrote a book about F# and I have a blog. For my work in the industry, see my professional home page.

To learn about my research, continue reading, or go straight to the list of publications. If you're a Cambridge student or a DoS, scroll to teaching & supervisions.

Tomas Petricek

Connect via twitter: @tomaspetricek
Email me at:
For more see my: GitHub | LinkedIn | Lanyrd

Theory of coeffects

I believe that tracking what applications require from the envirnoment in which they run is perhaps more important than tracking how they affect the envirnoment.

In a modern application, the environment includes services called, resources, system capabilities, and so on. Yet, most existing research focuses on the second problem. Coeffects attempt to provide the missing piece of the puzzle.

Data science

Data science opens many interesting questions for programming languages. How do we make data easily accessible? How do we provide safety guarantees for code that is often very dynamic and interactive?

I contributed to F# type providers which address accessing the data and some of my current work fits in the general "data science" theme.

F# theory & practice

I'm interested in bridging the gap between theory and practice in functional programming. I wrote a book Real-World Functional Programming that explains F# from a perspective of .NET developer and I teach F# in the industry.

I worked on computation expressions in F#, both by developing the theory (PADL'14) and by making them more relevant (Joinads).


Recent publications

[April 2014] What can Programming Language Research Learn from the Philosophy of Science?

Tomas Petricek. In Proceedings of AISB 2014

This essay looks how theories from philosophy of science apply to programming language research. I argue that it is important to clearly state research programme, avoid early over-emphasis on precision and I consider how to produce truly reusable experiments.

The F# Computation Expression Zoo

Tomas Petricek and Don Syme. In Proceedings of PADL 2014.

F# computation expressions F# provide a uniform syntax for computations such as monads, monad transformers and applicative functors. The syntax is adaptable and close to built-in language features of Python and C#. This article provides the details shows that the right syntax can often be determined by considering laws.

Coeffects: Unified static analysis of context-dependence

Tomas Petricek, Dominic Orchard and Alan Mycroft. In Proceedings of ICALP 2013.

Effects capture how computations affect the environment, coeffects capture the requirements that computations place on the environment. We present a unified coeffect system that can be used for checking liveness and properties of data-flow or distributed programs,

Papers published previously

Evaluation strategies for monadic computations

Tomas Petricek. In Proceedings of MSFP 2012.

When translating pure functional code to a monadic version, we need to use different translation depending on the desired evaluation strategy. In this paper, we present an unified translation that is parameterized by an operation malias. We also show how to give call-by-need translation for certain monads.

Extending Monads with Pattern Matching

Tomas Petricek, Alan Mycroft and Don Syme. In Haskell Symposium 2011.

The paper introduces a docase notation for Haskell that can be used for any monad that provides additional operations representing parallel composition, choice and aliasing. We require the operations to form a near-semiring, which gurantees that the notation resembles pattern matching.

Joinads: a retargetable control-flow construct for reactive, parallel and concurrent programming

Tomas Petricek and Don Syme. In Proceedings of PADL 2011.

Reactive, parallel and concurrent programming models are often difficult to encode in general-purpose programming languages. We present a lightweight language extension based on pattern matching that can be used for encoding a wide range of these models.

The F# Asynchronous Programming Model

Don Syme, Tomas Petricek and Dmitry Lomov. In PADL 2011.

We describe the asynchronous programming model in F#, and its applications. It combines a core language with a non-blocking modality to author lightweight asynchronous tasks. This allows smooth transitions between synchronous and asynchronous code and eliminates the inversion of control.

Collecting Hollywood's Garbage: Avoiding Space-Leaks in Composite Events

Tomas Petricek and Don Syme. In Proceedings of ISMM 2010.

The article discusses memory leaks that can occur in a reactive programming model based on events. It presents a formal garbage collection algorithm that could be used in this scenario and a correct reactive library based on this idea, implemented in F#.

Encoding monadic computations in C# using iterators

Tomas Petricek. In Proceedings of ITAT 2009

The paper shows how to encode certain monadic computations (such as a continuation monad for asynchronus programming) using the iterator language feature in C# 2.0.

Articles and reports

Fun with Parallel Monad Comprehensions

Tomas Petricek. The Monad.Reader Issue 18.

The article presents several monads that can benefit from the parallel monad comprehension notation that is supported in the re-designed monad comprehension syntax in Haskell. The examples are inspired by the work on joinads and include parsers, parallel and concurrent computations.

Effect and coeffect type systems

Tomas Petricek. First year report, Computer Laboratory.

The research goal discussed in the report is to use types in an ML-style language to track additional properties of computations including various kinds of effects (communication, memory access) and coeffects (how a computation depends on a context). The document briefly summarizes the work done during the first-year (including the work on joinads and coeffects) and it proposes future research projects.

Theses and older projects

Reacitve programming with events

Master thesis. Charles University in Prague, 2010

The thesis uses early version of joinad langauge extension for F# and garbage collection for events. Based on these concepts, it builds a simple reactive library for F# that allows writing reactive computations in both control-flow and data-flow styles.

Client-side scripting using meta-programming

Bachelor thesis. Charles University in Prague, 2007

The thesis presents a web development framework for F# that automatically splits a single F# program with monadic modality annotations into client-side JavaScript and server-side ASP.NET application.

Work in progress

Start here if you want to know that I'm currently working on and what I recently completed. Unpublished drafts are marked as such and I'm always looking for feedback!

[July 2013] Draft: Analysing context dependence in programs

Tomas Petricek, Dominic Orchard, Alan Mycroft. Unpublished draft.

This paper develops structural coeffect calculus which extends our earlier work on coeffects to make it more useful for tracking contextual information related to individual variables, such as liveness and provenance.

Draft: Teaching Functional Programming to Professional .NET Developers

Tomas Petricek. In Pre-proceedings of TFPIE 2012.

Functional programming is often taught at universities, but with the recent rise of functional programming in the industry, it is becoming important to teach functional concepts to experienced developers. This requires a very different approach.

Talks and recordings


Supervisions and teaching

I'm happy to supervise Part II (final year) projects that are related to functional programming, F# (or other functional languages), data science and data access, JavaScript and web programming or other interesting topics.

I had the pleasure of supervising some great Part II students:

I supervised the following Computer Laboratory courses for various colleges and I'm happy to supervise them again:

Academic community

I was a member of the Program Committee (PC) for ML 2013, ML 2012, CUFP 2012 and PSW 2012 and a member of External Review Committee (XRC) for ISMM 2012 and ISMM 2011. I also reviewed papers for PPDP 2013, TLCA 2013, CC 2013 and ECOOP 2012.

I'm happy to review papers that (broadly) match my interest in programming models, types, concurrent & distribtued and reactive programming, data & web and langauge integration (and also any controversial, provocative and novel work).

Teaching in Prague

As an undergraduate and Master's student at the Charles University in Prague, I helped to organize and teach non-compulsory courses.

Programming languages F# and OCaml (English)

Charles University, Winter 2009/2010

The lecture teaches programming in the ML-family of languages and highlights the mathematical foundations of ML languages. As a results students should find it easier to understand many mathematical concepts. It also explains advanced F# features such as computation expressions.

WinFX Programming (Czech)

Charles University, Summer 2005/2006

A practically oriented seminar about Windows programming using the WinFX framework (now called WPF, WCF and WF), which was in beta version in 2006. It discussed graphics, working with data and communication between applications (Jointly taught with Vojtech Jakl).