## 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?

## On the Bourbaki-Witt Principle in Toposes

Abstract: The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and related principles in an intuitionistic setting. Among other things, we show that Bourbaki-Witt fails exactly when the trichotomous ordinals form a set, but does not imply that fixed points can always be found by transfinite iteration. Meanwhile, on the side of models, we see that the principle fails in realisability toposes, and does not hold in the free topos, but does hold in all cocomplete toposes.

ArXiv version: arXiv:1201.0340v1 [math.CT]

This paper is an extension of my previous paper on the Bourbaki-Witt and Knaster-Tarski fixed-point theorems in the effective topos (arXiv:0911.0068v1).

## HoTT Equivalences

On December 6th 2011 I gave a talk about homotopy equivalences in the context of homotopy type theory at our seminar for foundations of mathematics and theoretical computer science. I discuss the differences and relations between isomorphism (in the sense of type theory), an adjoint equivalence, and a homotopy equivalence. Even though the talk itself was not super-well prepared, I hope the recording will be interesting to some people. I was going fairly slowly, so it should be possible to follow the talk. I apologize for such a long video, but I really did not see how to chop it up into smaller pieces. Also, I need to figure out why I cannot fast forward the video beyond what has been downloaded.

## How to make the “impossible” functionals run even faster

A talk given at “Mathematics, Algorithms and Proofs 2011″ at the Lorentz Center in Leiden, the Netherlands. I explain how to use computational effects to speed up Martin Escardo’s impossible functionals.

## Embedding the Baire space into natural numbers

A talk given at “Computation with Infinite Data: Logical and Topological Foundations” Dagstuhl seminar 11411. I describe a realizability model based on infinite-time Turing machines in which it is possible to embed the Baire space (infinite sequences of numbers) into the space of numbers.

Also see the post Constructive gem: an injection from Baire space to natural numbers for written notes on this topic.

## Video lectures as screencasts

Last year I participated in a project whose goal was to record at low cost my lectures on video and put them on-line. Since the most expensive parts of recording are having a camera man and manual post production, we set up a static camera and just uploaded raw video online at videolectures.net. As you can see for yourself, the sound is good (I wore a microphone) but the whiteboard is mostly illegible. In addition, it took about two weeks for the lectures to show up on-line because there were men-in-the-middle. So that got me thinking whether there was a better way.
Continue reading Video lectures as screencasts

## Definability and extensionality of the modulus of continuity functional

In an earlier post I talked about the modulus of continuity functional, where I stated that it cannot be defined without using some form of computational effects. It is a bit hard to find the proof of this fact so I am posting it on my blog in two parts, for Google and everyone else to find more easily. In the first part I show that there is no extensional modulus of continuity. In the second part I will show that every functional that is defined in PCF (simply-typed $\lambda$-calculus with natural numbers and recursion) is extensional.  Continue reading Definability and extensionality of the modulus of continuity functional

## Constructive gem: an injection from Baire space to natural numbers

I am not sure whether to call this one a constructive gem or stone. I suppose it is a matter of personal taste. I think it is a gem, albeit a very unusual one: there is a topos in which $\mathbb{N}^\mathbb{N}$ can be embedded into $\mathbb{N}$. Continue reading Constructive gem: an injection from Baire space to natural numbers