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:
- Spiff up the syntax by allowing more flexible syntax for bindings in functions and products.
- Keep track of source code locations so that we can report where the error has occurred.
- Perform normalization by evaluation.
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?
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!
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.