# Posts in the category Software

### The new and improved Programming languages zoo

- 07 September 2016
- Computation, Programming languages, Software, Teaching

It is my pleasure to announce the new and improved Programming languages Zoo, a potpourri of miniature but fully functioning programming language implementations. The new zoo has a decent web site, it is now hosted on GitHub, and the source code was cleaned up. Many thanks to Matija Pretnar for all the work.

The purpose of the zoo is to demonstrate design and implementation techniques, from dirty practical details to lofty theoretical considerations:

- functional, declarative, object-oriented, and procedural languages
- source code parsing with a parser generator
- recording of source code positions
- pretty-printing of values
- interactive shell (REPL) and non-interactive file processing
- untyped, statically and dynamically typed languages
- type checking and type inference
- subtyping, parametric polymorphism, and other kinds of type systems
- eager and lazy evaluation strategies
- recursive definitions
- exceptions
- interpreters and compilers
- abstract machine

There is still a lot of room for improvement and new languages. Contributions are welcome!

→ continue reading

My student Marko Koležnik is about to finish his Master’s degree in Mathematics at the University of Ljubljana. He implemented **Agda Writer**, a graphical user interface for the Agda proof assistant on the OS X platform. As he puts it, the main advantage of Agda Writer is *no Emacs*, but the list of cool features is a bit longer:

**bundled Agda:**it comes with preinstalled Agda so there is**zero installation effort**(of course, you can use your own Agda as well).**UTF-8 keyboard shortcuts:**it is super-easy to enter UTF-8 characters by typing their LaTeX names, just like in Emacs. It trumps Emacs by converting ASCII arrows to their UTF8 equivalents on the fly. In the preferences you can customize the long list of shortcuts to your liking.- the usual features expected on OS X are all there:
**auto-completion**,**clickable error messages and goals**, etc.

Agda Writer is open source. Everybody is welcome to help out and participate on the Agda Writer repository.

Who is Agda Writer for? Obviously for students, mathematicians, and other potential users who were not born with Emacs hard-wired into their brains. It is great for teaching Agda as you do not have to spend two weeks explaining Emacs. The only drawback is that it is limited to OS X. Someone should write equivalent Windows and Linux applications. Then perhaps proof assistants will have a chance of being more widely adopted.

→ continue reading (5 comments)### TEDx “Zeroes”

- 16 October 2014
- Programming, Software, Talks

I spoke at TEDx University of Ljubljana. The topic was how programming influences various aspects of life. I showed the audence how a bit of simple programming can reveal the beauty of mathematics. Taking John Baez’s The Bauty of Roots as an inspiration, I drew a very large image (20000 by 17500 pixels) of all roots of all polynomials of degree at most 26 whose coefficients are $-1$ or $1$. That’s 268.435.452 polynomials and 6.979.321.752 roots. It is two degrees more than Sam Derbyshire’s image, so consider the race to be on! Who can give me 30 degrees?

→ continue reading (6 comments)### Costa’s minimal surface with PovRay

- 30 December 2013
- Software

A student of mine worked on a project to produce beautiful pictures of Costa’s minimal surface with the PovRay ray tracer. For this purpose she needed to triangulate the and compute normals to it at the vertices. It is not too hard to do the latter part, and the Internet offers several ways of doing it, but the normals are a bit tricky. If anyone can calculate them with paper and pencil I’d like to hear about it.

I went back to my undergraduate days when I actually did differential geometry and churned out the normals with Mathematica. It took a bit of work, kind advice from my colleague Pavle Saksida, and a pinch of black magic (to extract the Delaunay triangulation from Mathematica), so I thought I might as well publish the result at my GitHub costa-surface repository. The code is released into public domain. Have fun making pictures of Costa’s surface! Here is mine (deliberately non-fancy):

→ continue reading### How to implement dependent type theory III

- 29 November 2012
- Homotopy type theory, Programming, Software, Tutorial

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).

### How to implement dependent type theory II

- 11 November 2012
- Homotopy type theory, Programming, Software, Tutorial

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.

### How to implement dependent type theory I

- 08 November 2012
- Homotopy type theory, Programming, Software, Tutorial

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 (6 comments)### Alg

- 22 January 2011
- Computation, Software

**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.

### Programming with effects II: Introducing eff

- 27 September 2010
- Computation, Eff, Guest post, Programming, Software, Tutorial

**[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 (7 comments)### Programming with effects I: Theory

- 27 September 2010
- Computation, Eff, Programming, Software, Talks, Tutorial

**[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.

→ continue reading (18 comments)### Random art in Python

- 21 April 2010
- Programming, Software, Tutorial

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

### Remote Backup with Secure Shell and Rsync

- 16 September 2008
- Software

Back in 2000 John Langford of the Machine Learning (Theory) blog and I wrote a backup script which I am still using today. A number of other people have found it useful so I decided to release it under an open source license. The script is easy to use under Linux. I am told it also backs up Windows with a bit of tweaking.

→ continue reading### Sub and Poly, two new additions to the PL Zoo

- 14 September 2008
- Programming languages, Software

I have added two new languages to the Programming Languages Zoo which demonstrate polymorphic type inference and type checking with subtypes.

→ continue reading (1 comment)### Exact real arithmetic in Haskell

- 03 September 2008
- Computation, Guest post, News, Software

*HERA* is an implementation of exact real arithmetic in Haskell using the approach by Andrej Bauer and Iztok Kavkler, see these and these slides. It uses the fast multiple precision floating point library MPFR. Download source, and see documentation and examples of usage at my home page.

[*Note by Andrej:* this is a guest post by Aleš Bizjak, a first-year student of mathematics at my department. I am very proud of the excellent work he did on his summer project.]

### An object-oriented language Boa

- 07 May 2008
- Programming languages, Software

I have added another language, called *Boa*, to the Programming Languages Zoo. It is an object-oriented language with the following features:

- integers and booleans as base types,
- first-class functions,
- dynamically typed,
- objects are extensible records with mutable fields,
- there are no classes, instead we can define “prototype” objects and extend them

to create instances.

### The Programming Languages Zoo

- 06 May 2008
- Programming languages, Software

I teach Theory of Programing Languages (page in Slovene). For the course I implemented languages which demonstrate basic concepts such as parsing, type checking, type inference, dynamic types, evaluation strategies, and compilation. My teaching assistant Iztok Kavkler contributed to the source code as well. I decided to publish the source code as a **Programming Language Zoo** for anyone who wants to know more about design and implementation of programming languages.