# Planet

PLT, n-Categorical, and Constructive Mathematics blogs.

Generated with org-webring -- v1.8.3

##### Syndicates

#### Compiling a Lisp: Reader

first – previous Welcome back to the “Compiling a Lisp” series. This time I want to take a break from compiling and finally add a reader. I’m finally getting frustrated manually entering increasinly complicated ASTs, so I figure it is time. After this post, we’ll be able to type in programs like: (< (+ 1 2) (- 4 3)) and have our compiler make ASTs for us! Magic. This will also add some nice debugging tools for us. For example, imagine an interactive command line utility in which we can enter Lisp expre…

Max Bernstein's Blog#### Compiling a Lisp: Primitive binary functions

first – previous Welcome back to the “Compiling a Lisp” series. Last time, we added some primitive unary instructions like add1 and integer->char. This time, we’re going to add some primitive binary functions like + and <. After this post, we’ll be able to compile programs like: (< (+ 1 2) (- 4 3)) Note that these expressions may look like function calls but, like last chapter, they are not opening new stack frames (which I’ll explain more about later). Instead, the compiler will recognize that the pro…

Max Bernstein's Blog#### A general definition of dependent type theories

The preprint version of the paper A general definition of dependent type theories has finally appeared on the arXiv! Over three years ago Peter Lumsdaine invited me to work on the topic, which I gladly accepted, and dragged my student Philipp Haselwarter into it. We set out to give an answer to the queation: What is type theory, precisely? At least for me the motivation to work on such a thankless topic came from Vladimir Voevodsky, who would ask the question to type-theoretic audiences. Some took hi…

Mathematics and Computation#### Racist Bullshit in Mathematics

Robin Gandy’s “On the Axiom of Extensionality–Part 1”, Journal of Symbolic Logic, Vol. 21, No. 1 (Mar., 1956) quotes Alan Turing using a racist phrase. Yikes. Those unfamiliar with this particular racist phrase will be disappointed to learn that it’s still current enough in the UK to be used “totally unintentional[ly]”… whatever that means. Gandy’s […]

weaselhat#### Every proof assistant: Cubical Agda – A Dependently Typed Programming Language with Univalence and Higher Inductive Types

I am happy to announce that we are restarting the "Every proof assistants" series of talks with Anders Mörtberg who will talk about Cubical Agda. Note that we are moving the seminar time to a more reasonable hour, at least as far as the working people in Europe are concerned. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types Time: Thursday, September 17, 2020 from 15:00 to 16:00 (Central European Summer Time, UTC+2)Location: online at Zoom ID 989 0478 …

Mathematics and Computation#### The Fall of the SKI Civilization

Abstract: The recent breakthroughs in deciphering the language and the literature left behind by the now extinct Twinklean civilization provides valuable insights into their history, science, and philosophy. The oldest documents discovered on the third planet of the star Lambda Combinatoris (also known as the Twinkle star) talk about the prehistory of the Twinklean thought. […]

Bartosz Milewski's Programming Cafe#### Compiling a Lisp: Primitive unary functions

first – previous Welcome back to the “Compiling a Lisp” series. Last time, we finished adding the rest of the constants as tagged pointer immediates. Since it’s not very useful to have only values (no way to operate on them), we’re going to add some primitive unary functions. “Primitive” means here that they are built into the compiler, so we won’t actually compile the call to an assembly procedure call. This is also called a compiler intrinsic. “Unary” means the functions will take only one argument. “F…

Max Bernstein's Blog#### Announcing the Johns Hopkins (Virtual) Category Theory Seminar

*No summary available.*

#### Compiling a Lisp: Booleans, characters, nil

first – previous Welcome back to the “Compiling a Lisp” series. Last time, we compiled integer literals. In today’s relatively short post, we’ll add the rest of the immediate types. Our programs will look like this: 'a' true false nil or () In addition, since we’re not adding too much exciting stuff today, I made writing tests a little bit easier by adding fixtures. Now, if we want, we can get a pre-made Buffer object passed into the test, and then have it destroyed afterward. Encoding Since we’r…

Max Bernstein's Blog#### Compiling a Lisp: Integers

first – previous Welcome back to the “Compiling a Lisp” series. Last time we made a small code execution demo. Today we’re going to add the first part of our language: integer literals. Our programs will look like this: 123 -10 0 But we’re not going to put a parser in. That can come later when it gets harder to manually construct syntax trees. Also, since implementing full big number support is pretty tricky, we’re only going to support fixed-width numbers. It’s entirely possible to then implement b…

Max Bernstein's Blog#### Compiling a Lisp: The smallest program

previous Welcome to the first post in the “Compiling a Lisp” series. We’re going to write a small program today. Before we actually compile anything, though, let’s build up a bit of a foundation for code execution. That way, we can see the code compile and run and be satisfied with the results of both. Instead of compiling to disk, like most compilers you may be familiar with (GCC, Clang, DMD, Python, etc), we’re going to compile in memory. This means that every time we run the program we have to compile…

Max Bernstein's Blog#### Compiling a Lisp: Overture

In my last series, I wrote about building a Lisp interpreter. This time, we’re going to write a Lisp compiler. This series is an adaptation of Abdulaziz Ghuloum’s excellent paper An Incremental Approach to Compiler Construction, with several key differences: Our implementation is in C, instead of Scheme Our implementation generates machine code directly, instead of generating text assembly Our implementation may omit some runtime data structures See my implementation for reference, but note that it m…

Max Bernstein's Blog#### Come One, Come All! The AU CS Colloquium Series is Open to All

This semester I’m the faculty chair of the AU CS Colloquium, and due to it being completely online this semester I decided to open it up to the wider community. So I’ll be doing some advertising here to get y’all to come and attend some great presentations. The complete schedule can be found here: The Colloquium Schedule Topics will vary and will include PL, category theory, security, and diversity in CS this semester. If you would like to attend please RSVP to me. The first presentation is by a NEW …

Metatheorem#### Haskell mini-patterns handbook

Collection of small Haskell patterns with detailed description, examples and exercises

Kowainik Blog#### Idris 2 version 0.2.1 Released

A new version (0.2.1) of Idris 2 has been released. You can download the source (including generated Scheme and Racket files for bootstrapping) from the download page. To build it, you can either use a bootstrapping version built in Idris 1, or (the simplest way), run make bootstrap to build from the generated Scheme. Full instructions are in INSTALL.md in the distribution. Documentation is available here. To get started, you can see: Installation instructions and how to get started Changes since Idris 1 T…

Idris#### What to Define When You’re Defining Gradual Type Systems

What do you have to do to define a gradual type system? You have to come up with a type system that has a question mark in it, of course. But what else?

weaselhat#### Benign Data Races Considered Harmful

The series of posts about so called benign data races stirred a lot of controversy and led to numerous discussions at the startup I was working at called Corensic. Two bastions formed, one claiming that no data race was benign, and the other claiming that data races were essential for performance. Then it turned out […]

Bartosz Milewski's Programming Cafe#### Formulog: ML + Datalog + SMT

If you read a description of a static analysis in a paper, what might you find? There’ll be some cute model of a language. Maybe some inference rules describing the analysis itself, but those rules probably rely on a variety of helper functions. These days, the analysis likely involves some logical reasoning: about the terms […]

weaselhat#### Categories for the Working C++ Programmer

This post is based on the talk I gave in Moscow, Russia, in February 2015 to an audience of C++ programmers. Let’s agree on some preliminaries. C++ is a low level programming language. It’s very close to the machine. C++ is engineering at its grittiest. Category theory is the most abstract branch of mathematics. It’s […]

Bartosz Milewski's Programming Cafe#### Defunctionalization and Freyd’s Theorem

The main idea of functional programming is to treat functions like any other data types. In particular, we want to be able to pass functions as arguments to other functions, return them as values, and store them in data structures. But what kind of data type is a function? It’s a type that, when paired […]

Bartosz Milewski's Programming Cafe#### Freyd’s Adjoint Functor Theorem

One of the tropes of detective movies is the almost miraculous ability to reconstruct an image from a blurry photograph. You just scan the picture, say “enhance!”, and voila, the face of the suspect or the registration number of their car appear on your computer screen. With constant improvements in deep learning, we might eventually […]

Bartosz Milewski's Programming Cafe#### Weighted Colimits

It’s funny how similar ideas pop up in different branches of mathematics. Calculus, for instance, is built around metric spaces (or, more generally, Banach spaces) and measures. A limit of a sequence is defined by points getting closer and closer together. An integral is an area under a curve. In category theory, though, we don’t […]

Bartosz Milewski's Programming Cafe#### Every proof assistant: Cur - Designing a less devious proof assistant

We shall finish the semester with a "Every proof assistant" talk by William Bowman. Note that we start an hour later than usual, at 17:00 UTC+2. Cur: Designing a less devious proof assistant Time: Thursday, June 25, 2020 from 17:00 to 18:00 (Central European Summer Time, UTC+2)Location: online at Zoom ID 989 0478 8985Speaker: William J. Bowman (University of British Columbia)Proof assistant: Cur Abstract: Dijkstra said that our tools can have a profound and devious influence on our thinking. I…

Mathematics and Computation#### Monoidal Catamorphisms

I have recently watched a talk by Gabriel Gonzalez about folds, which caught my attention because of my interest in both recursion schemes and optics. A Fold is an interesting abstraction. It encapsulates the idea of focusing on a monoidal contents of some data structure. Let me explain. Suppose you have a data structure that […]

Bartosz Milewski's Programming Cafe#### Guitar Decomposed: 9. Extension Chords

Previously we discussed ninth chords, which are the first in a series of extension chords. Extensions are the notes that go beyond the first octave. Since we build chords by stacking thirds on top of each other, the next logical step, after the ninth chord, is the eleventh and the thirteenth chords. And that’s it: […]

Bartosz Milewski's Programming Cafe#### Every proof assistant: Epigram 2 - Autopsy, Obituary, Apology

This week shall witness a performance by Conor McBride. Epigram 2: Autopsy, Obituary, Apology Time: Thursday, June 11, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)Location: online at Zoom ID 989 0478 8985Speaker: Conor McBride (University of Strathclyde)Proof assistant: Epigram 2 Abstract: "A good pilot is one with the same number of take-offs and landings." runs the old joke, which makes me a very bad pilot indeed. The Epigram 2 project was repeatedly restarted several times in…

Mathematics and Computation#### a baseline compiler for guile

Greets, my peeps! Today's article is on a new compiler for Guile. I made things better by making things worse!The new compiler is a "baseline compiler", in the spirit of what modern web browsers use to get things running quickly. It is a very simple compiler whose goal is speed of compilation, not speed of generated code.Honestly I didn't think Guile needed such a thing. Guile's distribution model isn't like the web, where every page you visit requires the browser to compile fresh hot mess; in Guile I …

wingolog#### Guitar Decomposed: 8. Ninth Chords

We have already discussed several kinds of seventh chords. But if you can extend the chord by adding a third above it, why not top it with yet another third? This way we arrive at the ninth chord. But a ninth is one whole step above the octave. So far we’ve been identifying notes that […]

Bartosz Milewski's Programming Cafe#### Every proof assistant: redtt

This week the speaker will be Jon Sterling, and we are getting two proof assistants for the price of one! redtt and the future of Cartesian cubical type theory Time: Thursday, June 4, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)Location: online at Zoom ID 989 0478 8985Speaker: Jon Sterling (Carnegie Mellon University)Proof assistant: redtt and cooltt Abstract: redtt is an interactive proof assistant for Cartesian cubical type theory, a version of Martin-Löf type theory featuring…

Mathematics and Computation#### Guitar Decomposed: 7. Major Seventh Chords

Previously we talked about dominant seventh chords, which are constructed by adding a minor seventh to a chord. Adding a major seventh instead is a very “jazzy” thing. With it, you can jazz up any chord, not just the dominant. A major seventh is one semitone below the octave, so it forms a highly dissonant […]

Bartosz Milewski's Programming Cafe#### Idris 2 version 0.2.0 Released

A new version (0.2.0) of Idris 2 has been released. You can download the source (including generated Scheme and Racket files for bootstrapping) from the download page. The significance of this release is that it is the first release which can compile itself - that is, it is written in Idris 2. To build it, you can either use a bootstrapping version built in Idris 1, or (the simplest way), run make bootstrap to build from the generated Scheme. Full instructions are in INSTALL.md in the distribution. Documen…

Idris#### Every proof assistant: Beluga

We are marching on with the Every proof assistant series! Mechanizing Meta-Theory in Beluga Time: Thursday, May 28, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)Location: online at Zoom ID 989 0478 8985Speaker: Brigitte Pientka (McGill University)Proof assistant: Beluga Abstract: Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the pro…

Mathematics and Computation#### Every proof assistant: MMT

I am happy to announce the next seminar in the "Every proof assistant" series. MMT: A Foundation-Independent Logical System Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)Location: online at Zoom ID 989 0478 8985Speaker: Florian Rabe (University of Erlangen)Proof assistant: The MMT Language and System Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committing to any found…

Mathematics and Computation#### The Big Brzozowski

When I mentioned how important smart constructors are for Brzozowski derivatives on Twitter, when Prabhakar Ragde raised an interesting question: I saw Brzozowski in the hall once and asked him if there was any bound on the growth of regex size. He didn’t know of any work on the subject! — Prabhakar Ragde (@plragde) May […]

weaselhat