Eff 3.0

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!

Programming with Algebraic Effects and Handlers

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.

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

While making a comment on Stackoverflow I noticed something: suppose we have a term in the $\lambda$-calculus in which no abstracted variable is used more than once. For example, $\lambda a b c . (a b) (\lambda d. d c)$ is such a term, but $\lambda f . f (\lambda x . x x)$ is not because $x$ is used twice. If I am not mistaken, all such terms can be typed. For example:

# fun a b c -> (a b) (fun d -> d c) ;;
- : ('a -> (('b -> 'c) -> 'c) -> 'd) -> 'a -> 'b -> 'd = <fun>

# fun a b c d e e' f g h i j k l m n o o' o'' o''' p q r r' s t u u' v w x y z ->
q u i c k b r o w n f o' x j u' m p s o'' v e r' t h e' l a z y d o''' g;;
- : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j ->
'k -> 'l -> 'm -> 'n -> 'o -> 'p -> 'q -> 'r -> 's -> 't ->
('u -> 'j -> 'c -> 'l -> 'b -> 'v -> 'p -> 'w -> 'o -> 'g ->
'q -> 'x -> 'k -> 'y -> 'n -> 't -> 'z -> 'r -> 'a1 -> 'e ->
'b1 -> 'c1 -> 'i -> 'f -> 'm -> 'a -> 'd1 -> 'e1 -> 'd -> 's
-> 'h -> 'f1) -> 'v -> 'b1 -> 'z -> 'c1 -> 'u -> 'y -> 'a1
-> 'w -> 'x -> 'e1 -> 'd1 -> 'f1 = <fun>


What is the easiest way to see that this really is the case?

A related question is this (I am sure people have thought about it): how big can a type of a typeable $\lambda$-term be? For example, the Ackermann function can be typed as follows, although the type prevents it from doing the right thing in a typed setting:

# let one = fun f x -> f x ;;
val one : ('a -> 'b) -> 'a -> 'b =
# let suc = fun n f x -> n f (f x) ;;
val suc : (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c =
# let ack = fun m -> m (fun f n -> n f (f one)) suc ;;
val ack :
((((('a -> 'b) -> 'a -> 'b) -> 'c) ->
(((('a -> 'b) -> 'a -> 'b) -> 'c) -> 'c -> 'd) -> 'd) ->
((('e -> 'f) -> 'f -> 'g) -> ('e -> 'f) -> 'e -> 'g) -> 'h) -> 'h = <fun>


That’s one mean type there! Can it be “explained”? Hmm, why does ack compute the Ackermann function in the untyped $\lambda$-calculus?

Running a classical proof with choice in Agda

As a preparation for my part of a joint tutorial Programs from proofs at MFPS 27 at the end of this month with Ulrich Berger, Monika Seisenberger, and Paulo Oliva, I’ve developed in Agda some things we’ve been doing together.

Using

for giving a proof term for classical countable choice, we prove the classical infinite pigeonhole principle in Agda: every infinite boolean sequence has a constant infinite subsequence, where the existential quantification is classical (double negated).

As a corollary, we get the finite pigeonhole principle, using Friedman’s trick to make the existential quantifiers intuitionistic.

This we can run, and it runs fast enough. The point is to illustrate in Agda how we can get witnesses from classical proofs that use countable choice. The finite pigeonhole principle has a simple constructive proof, of course, and hence this is really for illustration only.

The main Agda files are

These are Agda files converted to html so that you can navigate them by clicking at words to go to their definitions. A zip file with all Agda files is available. Not much more information is available here.

The three little modules that implement the Berardi-Bezem-Coquand, Berger-Oliva and Escardo-Oliva functionals disable the termination checker, but no other module does. The type of these functionals in Agda is the J-shift principle, which generalizes the double-negation shift.

Bob Harper has a blog

Bob Harper of CMU, has recently started a blog, called Existential Type, about programming languages. He is a leading expert in Programming Languages. I remember being deeply inspired the first time I heard him talk. I was an incoming graduate student at CMU and he presented what the programming languages people at CMU did. His posts are fun to read, unreserved and very educational. Highly recommended!