|
|||||
|
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? Alg is a program for enumeration of finite models of single-sorted first-order theories. These include groups, rings, fields, lattices, posets, graphs, and many more. Alg was written as a class project by Aleš Bizjak, a student of mine whose existence I cannot confirm with a URL. I joined the effort, added bells and whistles, as well as an alternative algorithm that works well for relational structures. Alg is ready for public consumption, although it should be considered of “beta” quality. Instructions for downloading alg are included at the end of this post. [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. I get asked every so often to release the source code for my random art project. The original source is written in Ocaml and is not publicly available, but here is a simple example of how you can get random art going in python in 250 lines of code. Download source: randomart.py These are the slides and the extended abstract from my MSFP 2008 talk. Apparently, I forgot to publish them online. There is a discussion on the Agda mailing list to which the talk is somewhat relevant, so I am publishing now. Abstract: Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions as [...] I have aded to the PL Zoo a mini prolog interpreter. It really is minimalistic, as it only handles pure Horn clauses. There is no arithmetic, lists, cuts, or disjunctions. Nevertheless, it ought to be possible to write a miniml interpreter in it… If anyone does it, please send me [...] I have added two new languages to the PL Zoo. The minor addition is miniml+error, which is just MiniML with an error exception (raised by division by 0) that cannot be caught. The purpose is to demonstrate handling of fatal errors during runtime. The more interesting new animal is levy (written by Matija Pretnar and myself), [...] |
|||||
|
|
|||||
