|
|||||
|
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 Free variables are not “implicitly universally quantified”! 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 I am on a roll. In the second post on how to implement dependent type theory we are going to:
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? 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: 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 [...] 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 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 Berardi-Bezem-Coquand functional, or alternatively, for giving a [...] [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 Programming with effects II: Introducing eff [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. |
|||||
|
|
|||||
