Tomas Petricek @ Computer Lab
I'm a second-year PhD Student in the Computer Laboratory at the University of Cambridge and a member of the Programming, Logic and Semantics Group. My supervisors are Alan Mycroft from the Computer Laboratory and Don Syme from Microsoft Research.
Before joining the Computer Laboratory, I finished Master's degree in theoretical computer science at the Faculty of Mathematics and Physics of Charles University in Prague. I also did two internships with Don Syme.
Besides my studies, I'm an active member of the F# community, I sometimes speak at various .NET or Functional Programming industry events and I wrote a book about F# and I write a blog. See my professional home page.
I can be contacted at
Supervisions and Teaching
I'm happy to supervise Part II (final year) projects that are related to functional programming, F# (or other functional languages), JavaScript and web programming or other interesting projects.
- See a list with my project ideas.
- If you want to discuss your idea,
I supervised the following Computer Laboratory courses and I'm happy to supervise them again:
- Concepts in Programming Languages (Easter 2011/12)
- Optimising Compilers (Michaelmas 2011/12)
- Types (Michaelmas 2011/12)
- Denotational Semantics (Lent 2011/12)
Real-World Functional Programming
I'm a functional programmer and I think that F# and functional programming should be used in practice. I wrote a book that explains functional concepts to professional developers with C# background using C# and F# examples.
It is available from Manning or from your favorite store.
[New: February 2012]Try F# joinads online
Joinads extend monadic notation in F# and Haskell with a feature that is useful for concurrent, parallel and reactive programming.
To learn more and experiment with joinads in a web browser visit Try Joinads!
Latest writings from my blog
Photography
I'm a lazy photographer with no online gallery at the moment, but I have been uploading a new photo to my online calendar every month for quite some time.
2005 | 2006 | 2007 | 2008 | 2009 | 2010 | 2011 | 2012
Academic community
I was a member of the Program Committee (PC) for ML 2012, CUFP 2012 and PSW 2012 and a member of External Review Committee (XRC) for ISMM 2012 and ISMM 2011.
I also reviewed some papers for ECOOP 2012 and CC 2013.
I'm happy to review papers for conferences or journals that (broadly) match my interest in programming models; functional programming and type systems; concurrent, distribtued and reactive programming (and also any controversial, provocative and novel work).
Teaching in Prague
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 lecture 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).
Elsewhere on the internet
If you want to keep up to date, you can subscribe to my blog or only to my research posts via RSS. You can also follow @tomaspetricek on twitter.
For my other activities and projects that I am or was involved in, visit my professional home page.
I'm active member of the F# developer community. I usually come to F#unctional Londoners meetings and participate on StackOverflow.
Check out my F# Snippets web site. It is an online pastebin for the F# langauge that type-checks posted snippets and generates nice JavaScript tooltips with type information.
Research interests
I'm interested in programming models. That is, what is the best “language” for solving problems from a particular domain, how to encode these models in programming languages and how to guarantee that the programming model avoids certain kinds of errors. More specifically, I'm interested in meta-programming, embedded languages, monads and other abstract representations of computations, as well as clever type systems.
You can read about my current research programme in a first-year report. Briefly, the areas that I'm working on now or have worked on in include:
Coeffect systems. I'm working on types for tracking how computation depends on some context. For example, on which nodes (server, phone, web browser, ...) can a function execute in a distributed language. Such properties are dual to effects, so I use the term coeffect. See a recent draft for more information.
Reactive and concurrent. I designed a language extension for F# that can be used for encoding reactive, concurrent and parallel programming models. You can and experiment with it on the TryJoinads web site.
Distributed and web programming. I developed an F# framework that allows writing client/server applications in an integrated, type-safe way. See an technical report and my bachelor thesis. Recent implementations of the idea include commerical WebSharper and open-source Pit.
Publications and talks
Below are links to accepted papers as well as drafts that I'm currently working on. Comments and suggestions are welcome. If I missed some important related work, let me know!
Work in progress
Coeffects: The Essence of Context Dependence
We consider three examples of context-dependence analysis: liveness analysis, tracking the use of rebindable resources, and calculating caching requirements for data-flow programs. Informed by these cases, we present a unified calculus for tracking context dependence in functional languages together with a categorical semantics based on indexed comonads.
Syntax Matters: Writing abstract computations in F#
Abstractions such as monads, monoids and applicative functors are a useful way of expressing various computations used in practice. However, they are hard to use without a convenient syntactic sugar. In this parper, we describe F# computation expressions, which provide such syntax for a large number of practically useful computations.
Teaching Functional Programming to Professional .NET Developers
Functional programming is often taught at universities. With the recent rise of functional programming in the industry, it is becoming important to teach functional concepts to experienced developers. This paper presents our experience with taching functional ideas to professional developers through C# and F#.
Published papers
Evaluation strategies for monadic computations
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.
details | download pdf | bibtex
Extending Monads with Pattern Matching
Tomas Petricek, Alan Mycroft and Don Syme.
In Proceedings of Haskell Symposium 2011.
The paper introduces a docase notation for Haskell. The notation 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.
details | download pdf | bibtex
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.
details | download pdf | bibtex
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.
details | download pdf | bibtex
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#.
details | download pdf (backup) | bibtex
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.
details | download pdf | bibtex
Talks and materials
[New: April 2012] Tracking context-dependent properties using coeffects (slides)
Talk at the Institute of Cybernetics (Tallin University) that describes coeffect systems for tracking how expressions depend on some context. Coeffects are associeted with the context and can be modelled using comonads. They can be used to express properties from distributed programming, secure information flow and others.
Coeffect Systems and Typing (slides)
Preliminary talk from Computer Laboratory that introduces coeffect systems for tracking how expressions depend on some context. The talk discusses relations between effects and monads & coeffects and comonads.
Reactive pattern matching for F# (recorded)
I presented joinads at the Lang.NET Symposium 2009. The talk presents the F# language extension and examples focusing on reactive programming. Updated slides from a talk at MSR Cambridge contain more information.
video | lang.net slides | msr slides
Reactive programming in F# (recorded)
Some ideas from my reactive programming research have made it to the standard F# library. This talk from the F# user group in London shows how to write real-world reactive programms in F#.
Collecting Hollywood’s Garbage (slides)
This talk from ISMM 2010 discusses garbage collection of events in a reactive programming framework. It presents an astonishing duality between traditional references and references between events.
Theses and older projects
Effect and coeffect type systems
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.
Reacitve programming with events (Master's thesis)
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.
details | download pdf | bibtex
Encoding monadic computations in C# using iterators
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. The paper was presented at ITAT 2009.
details | download pdf | bibtex
Client-side scripting using meta-programming (Bachelor's thesis)
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.