I have had the honor to lecture at the Oregon Programming Language Summer School 2018 on the topic of algebraic effects and handlers. The notes, materials and the lectures are available online:

• the GitHub repository with the course material
• the OPLSS lecture materials, including notes and video recordings of the lectures

I gave four lectures which started with the mathematics of algebraic theories, explained how they can be used to model computational effects, how we make a programming language out of them, and how to program with handlers.

→ continue reading (3 comments)

I am looking for a PhD student in mathematics. Full tuition & stipend will be provided for a period of three years, which is also the official length of the programme. The topic of research is somewhat flexible and varies from constructive models of homotopy type theory to development of a programming language for a proof assistant based on dependent type theory, see the short summary of the Effmath project for a more detailed description.

The candidate should have as many of the following desiderata as possible, and at the very least a master's degree (or an equivalent one):

1. a master's degree in mathematics, with good knowledge of computer science
2. a master's degree in computer science, with good knowledge of mathematics
3. experience with functional programming
4. experience with proof assistants
5. familiarity with homotopy type theory

The student will officially enrol in October 2015 at the University of Ljubljana. No knowledge of Slovene is required. However, it is possible, and even desirable, to start with the actual work (and stipend) earlier, as soon as in the spring of 2015. The candidates should contact me by email as soon as possible. Please include a short CV and a statement of interest.

Update 2015-03-28: the position has been taken.

→ continue reading

Matija and I are pleased to announce a new major release of the eff programming language.

In the last year or so eff has matured considerably:

• It now looks and feels like OCaml, so you won't have to learn yet another syntax.
• It has static typing with parametric polymorphism and type inference.
• Eff now clearly separates three basic concepts: effect types, effect instances, and handlers.
• How eff works is explained in our paper on Programming with Algebraic Effects and Handlers.
• We moved the source code to GitHub, so go ahead and fork it!

→ continue reading (6 comments)

With Matija Pretnar.

Abstract: Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel ways. We give a denotational semantics of eff and discuss a prototype implementation based on it. Through examples we demonstrate how the standard effects are treated in eff, and how eff supports programming techniques that use various forms of delimited continuations, such as backtracking, breadth-first search, selection functionals, cooperative multi-threading, and others.

Download paper: eff.pdf

ArXiv version: arXiv:1203.1539v1 [cs.PL]

To read more about eff, visit the eff page.

→ continue reading (19 comments)

[UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.]

**Let's keep the blog rolling! Here are delimited continuations in eff, and a bunch of questions I do not know the answers to.

→ continue reading (6 comments)

[UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.]

From some of the responses we have been getting it looks like people think that the io effect in eff is like unsafePerformIO in Haskell, namely that it causes an effect but pretends to be pure. This is not the case. Let me explain how eff handles built-in effects.

→ continue reading

[UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.]

**This is a second post about the programming language eff. We covered the theory behind it in a previous post. Now we turn to the programming language itself.

Please bear in mind that eff is an academic experiment. It is not meant to take over the world. Yet. We just wanted to show that the theoretical ideas about the algebraic nature of computational effects can be put into practice. Eff has many superficial similarities with Haskell. This is no surprise because there is a precise connection between algebras and monads. The main advantage of eff over Haskell is supposed to be the ease with which computational effects can be combined.

→ continue reading (7 comments)

[UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.]

I just returned from Paris where I was visiting the INRIA ?r² team. It was a great visit, everyone was very hospitable, the food was great, and the weather was nice. I spoke at their seminar where I presented a new programming language eff which is based on the idea that computational effects are algebras. The language has been designed and implemented jointly by Matija Pretnar and myself. Eff is far from being finished, but I think it is ready to be shown to the world. What follows is an extended transcript of the talk I gave in Paris. It is divided into two posts. The present one reviews the basic theory of algebras for a signature and how they are related to computational effects. The impatient readers can skip ahead to the second part, which is about the programming language.

A side remark: I have updated the blog to WordPress to 3.0 and switched to MathJax for displaying mathematics. Now I need to go through 70 old posts and convert the old ASCIIMathML notation to MathJax, as well as fix characters which got garbled during the update. Oh well, it is an investment for the future.

→ continue reading (18 comments)