Tomas Petricek @ Computer Lab
I'm first-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
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.
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
Teaching
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.
My 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:
Effect and Coeffect Systems. Currently, I'm working on type systems that track how computation depends on some context. Example is tracking where can a function in a distributed language execute (server, phone, web browser, etc.). Such context-dependence is in some sense dual to effects, so we use the term coeffects. See a recently submitted draft for more information.
Reactive and Concurrent Programming. I designed a language extension for F# computation expressions that can be used for encoding reactive, concurrent and parallel programming models. Some ideas from this work has made it to the stnadard F# library and there is a a Haskell Symposium paper that simplifies the theory.
Distributed and Web Programming. During the first internship at MSR, I developed an F# web framework that allows writing client/server applications in an integrated, type-safe way.
The ideas from this work influenced an industrial product WebSharper. For more information see an technical report and my bachelor thesis.
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
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.
Coeffects: typing context-dependent computations using comonads
We describe a type-system for tracking how computations depend on some context, such as execution environment or required security permissions. Following the work on tracking effects using monads, we show how to track context-dependence (or coeffects) using comonads. We also show how coeffects differ from effects.
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.
Published papers
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: October 2011] 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
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.