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 is isomorphic to where is the type of integers smaller than , corresponding to the set .
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
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!
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
PRL recently produced three papers for the SNAPL conference.
- Linking Types for Multi-Language Software: Have Your Cake and Eat It Too, by Daniel Patterson and Amal Ahmed.
- Search for Program Structure, by Gabriel Scherer
- Migratory Typing: Ten Years Later, by Sam Tobin-Hochstadt, Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland and Asumu Takikawa