Mathematicians are often confused about the meaning of variables. I hear them say “a free variable is implicitly universally quantified”, by which they mean that it is ok to equate a formula $\phi$ with a free variable $x$ with its universal closure $\forall x \,.\, \phi$. I am addressing this post to those who share this opinion.

→ continue reading (31 comments)

I spent a week trying to implement higher-order pattern unification. I looked at couple of PhD dissertations, talked to lots of smart people, and failed because the substitutions were just getting in the way all the time. So today we are going to bite the bullet and implement de Bruijn indices and explicit substitutions.

The code is available on Github in the repository andrejbauer/tt (the blog-part-III branch).

→ continue reading (6 comments)

I am on a roll. In the second post on how to implement dependent type theory we are going to:

1. Spiff up the syntax by allowing more flexible syntax for bindings in functions and products.
2. Keep track of source code locations so that we can report where the error has occurred.
3. Perform normalization by evaluation.

→ continue reading (9 comments)

I am spending a semester at the Institute for Advanced Study where we have a special year on Univalent foundations. We are doing all sorts of things, among others experimenting with type theories. We have got some real experts here who know type theory and Coq inside out, and much more, and they're doing crazy things to Coq (I will report on them when they are done). In the meanwhile I have been thinking how one might implement dependent type theories with undecidable type checking. This is a tricky subject and I am certainly not the first one to think about it. Anyhow, if I want to experiment with type theories, I need a small prototype first. Today I will present a very minimal one, and build on it in future posts.

Make a guess, how many lines of code does it take to implement a dependent type theory with universes, dependent products, a parser, lexer, pretty-printer, and a toplevel which uses line-editing when available?

→ continue reading (9 comments)

It seems to me that people think I am a constructive mathematician, or worse a constructivist (a word which carries a certain amount of philosophical stigma). Let me be perfectly clear: it is not decidable whether I am a constructive mathematician.

→ continue reading (44 comments)

I am sitting on a tutorial on categorical semantics of dependent type theory given by Peter Lumsdaine. He is talking about categories with attributes and other variants of categories that come up in the semantics of dependent type theory. He is amazingly good at fielding questions about definitional equality from the type theorists. And it looks like some people are puzzling over pullbacks showing up, which Peter is about to explain using syntactic categories. Here is a pedestrian explanation of a very important fact:

Substitution is pullback.

→ continue reading (14 comments)

Egbert Rijke successfully defended his master thesis in Utrecht a couple of weeks ago. He published it on the Homotopy type theory blog (here is a direct link to the PDF file (revised)). The thesis is well written and it contains several new results, but most importantly, it is a gentle yet non-trivial introduction to homotopy type theory. If you are interested in the topic but do not know where to start, Egbert's thesis might be perfect for you. As far as I know it is the first substantial piece of text written in (informal) homotopy type theory.

What I find most amazing about the work is that Egbert does not have to pretend to be a homotopy type theorist, like us old folks. His first contact with type theory was homotopy type theory, which impressed on his mind a new kind of geometric intuition about $\Pi$'s, $\Sigma$'s and $\mathrm{Id}$'s. If we perform enough such experiments on young bright students, strange things will happen.

→ continue reading (4 comments)

This is an advertisement for two great meetings we are organizing in Ljubljana from June 15 to June 20, 2012:

• Fourth workshop on formal topology (June 15—19)
• Workshop on Higher Dimensional Algebra, Categories and Types (June 20)

There are many reasons why you should come: Ljubljana is lovely in June, with many cafes and restaurants on the Ljubljanica river bank, we have a very interesting programme, and when will you next be able to attend a meeting in which the keynote speakers are Per Martin-Löf, Ieke Moerdijk and Vladimir Voevodsky? Not to mention that the schedule is fairly light, everything is within walking distance, and we are organizing dinners at some excellent restaurants.

If you decide to come, make sure to book a hotel early and register today!

→ continue reading (4 comments)

I remember how hard it was to assimilate category theory when I was a student. A beginning student on math.stackexchange.com is asking for a solution to a basic lemma about pullbacks. It really is the sort of thing one should do by oneself. Nevertheless, here it is, in gory details.

Download: pullback.pdf

→ continue reading (1 comment)

It is well known that, both in constructive mathematics and in programming languages, types are secretly topological spaces and functions are secretly continuous. I have previously exploited this in the posts Seemingly impossible functional programs and A Haskell monad for infinite search in finite time, using the language Haskell. In languages based on Martin-Löf type theory such as Agda, there is a set of all types. This can be used to define functions $\mathbb{N} \to \mathrm{Set}$ that map numbers to types, functions $\mathrm{Set} \to \mathrm{Set}$ that map types to types, and so on.

Because $\mathrm{Set}$ itself is a type, a large type of small types, it must have a secret topology. What is it? There are a number of ways of approaching topology. The most popular one is via open sets. For some spaces, one can instead use convergent sequences, and this approach is more convenient in our situation. It turns out that the topology of the universe $\mathrm{Set}$ is indiscrete: every sequence of types converges to any type! I apply this to deduce that $\mathrm{Set}$ satisfies the conclusion of Rice's Theorem: it has no non-trivial, extensional, decidable property.

To see how this works, check:

• A short paper with the proofs in mathematical vernacular, and further discussion of the intuitions, motivations and consequences.
• Literate proofs in Agda of the universe indiscreteness theorem and Rice's Theorem for the universe.
• Agda proofs of related facts.

The Agda pages can be navigated be clicking at any (defined) symbol or word, in particular by clicking at the imported module names.

→ continue reading (2 comments)

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)

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 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 = 
</pre>

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 = 
</pre>

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

→ continue reading (5 comments)

With Peter LeFanu Lumsdaine.

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.

Download paper: bw.pdf
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).

→ continue reading