Two weeks ago, I attended the first Programming Language Implementation Summer School, held in beautiful Bertinoro, Italy.
The goal of PLISS was “to prepare early graduate students and advanced undergraduates for research in the field,” and I think it successfully accomplished that. There were many talks in a variety of areas, such as just-in-time compilers, garbage collection, static analysis, and distributed systems. But PLISS was more than just a series of talks: PLISS provided an environment for interacting with other students as well as senior researchers.
In this blog post, reporting on a collaboration with Li-Yao Xia, I will show an example of how some results that we traditionally think of as arising from free theorems / parametricity can be established in a purely “syntactic” way, by looking at the structure of canonical derivations. More precisely, I prove that \(
\newcommand{\List}[1]{\mathsf{List}~#1}
\newcommand{\Fin}[1]{\mathsf{Fin}~#1}
\newcommand{\Nat}[1]{\mathbb{N}}
\newcommand{\rule}[2]{\frac{\displaystyle \array{#1}}{\displaystyle #2}}
\newcommand{\judge}[2]{{#1} \vdash {#2}}
\newcommand{\emptyrule}[1]{\begin{array}{c}\\[-1em] #1 \end{array}}
∀α. \List α → \List \alpha
\) is isomorphic to \(
Π(n:\Nat{}). \List{(\Fin{n})}
\) where \(\Fin{n}\) is the type of integers smaller than \(n\), corresponding to the set \(\{0, 1, \dots, n-1\}\).
Racket 6.9 was released in April and it has been smooth sailing for many people. However, some people using the Windows 10 Creators Update have been experiencing crashes, not just for Racket, but for the whole operating system. This is due to a bug in Windows. We have contacted Microsoft; they have classified the bug as (1) a stack overflow and (2) not a security hazard, and intend to add a fix in a future version of Windows.
The next version of Racket will include a patch to help avoid triggering the bug. Until then, one work-around is to run Racket in a virtual machine (VM). This blog post is a step-by-step guide on how to install a VM for Racket.
A VirtualBox image with Racket preinstalled can be downloaded here:
The username and password for this machine are both racket.
In April 3—5 I took part into a Russian conference exclusively devoted to programming languages: Programming Languages and Compilers (Google.Translated version of the site). I was a member of organizing committee and had a paper there.
This is the first conference in Russia highly focused on our area of PL. At least for the last several decades (I believe, there were conferences of the kind back in USSR). The conference was devoted to the memory of prominent Soviet PL-researcher from Rostov-on-Don, Adolf Fuksman who worked on ideas quite similar to what we know as the aspect-oriented programming back in the 70-s.
The source code for the PRL website is written using Scribble, the Racket documentation tool. I am very happy with this choice, and you should be too!
Gabriel Scherer and I recently wrote an artifact for a semantics paper on a typed assembly language interoperating with a high-level functional language.
Rank polymorphism gives you code reuse on arguments of different dimensions. Take a linear interpolation function (let’s just call it lerp) for scalars:
(λ ((lo 0) (hi 0) (α 0)) (+ (* lo (- 1 α)) (* hi α)))
The number marks on each argument indicate the expected “rank” of the argument: how many dimensions it should have. In this case, each one is marked 0, indicating a scalar (i.e., 0-dimensional) argument. The function is usable as-is for
-
α-blending two RGB pixels
-
dimming or brightening an image
-
fade transition between video scenes