I found a javac bug

JDK-8178701: Compile error with switch statement on protected enum defined in parent inner class

I discovered this bug when I wrote some code that compiled in Eclipse, committed it, and then got an email a few minutes later from our Jenkins continuous integration server saying that the build failed. From the error message, I managed to track it down to a specific section of code that compiled in Eclipse but gave a compile error in javac.

This isn’t the first time I’ve ran into a Java compiler or standard library bug while developing CertSAFE, nor is it the first time that I’ve submitted a bug report via the Oracle web form. However, it is the first time that I’ve had a report accepted and published as a verified OpenJDK bug.

I’m always happy when I find a compiler bug, because it makes me feel better about bugs in my code to know that the platform developers screw up too.

A plausible-sounding data structure that probably doesn’t exist

Here is a description of an abstract data type: a confluently persistent set data type containing a subset of the integers in a range \([1..n]\) and supporting \(O(\log(n)^c)\) time creation, \(O(\log(n)^c)\) time size query, \(O(n \log(n)^c)\) time conversion to a duplicate-free list, and \(O(\log(n)^c)\) time merging, for some constant \(c\). Here, “creation” takes as arguments the range of the element domain \([1..n]\) and an optional single element in this range, and “merging” takes two sets with the same domain and returns a new set representing the union of the two input sets. In Haskell, the type signatures for these operations might look like this:

Seems fairly reasonable, right? I’m going to show that it is likely that no such data structure exists.

Continue reading A plausible-sounding data structure that probably doesn’t exist

Making ByteString and Text instances of Foldable… almost

I just noticed you can do this:

And then use it like this:

Notice that those are the polymorphic Foldable functions maximum and mapM_, not Text-specific functions. I don’t know if this has any real-world applications, but it’s kind of neat…

Update: As pointed out by lfairy on Reddit, the FMList type works kind of like this.

Exact (integer arithmetic only) capsule intersection test

The capsule (also called a “pill”) is one of a few common types of shape used for collision detection in games and other applications. A 3-D capsule is a cylinder capped by hemispheres. The 2-D equivalent, a rectangle capped by semicircles, is technically called a stadium, but they are commonly just called capsules as well.

Capsules used for collision detection in Super Smash Bros. Melee.
Capsules used for collision detection in Super Smash Bros. Melee. From here.

Capsules are nice because they can form both spherical and elongated shapes in any direction. The animation above shows how Super Smash Bros. Melee uses spherical hitboxes that are “stretched” across frames into capsules to prevent fast-moving attacks from going through opponents without hitting them. (Marvel vs. Capcom 3 uses the same trick.) What really makes capsules useful is that they have a very simple mathematical description: a capsule is the set of all points less than a certain radius from a line segment. This means you can check whether two capsules intersect each other by just finding the shortest distance between the two line segments and checking whether it is less than the sum of the radii.

Calculating the distance between two line segments is a well-known problem. This StackOverflow answer gives the code to do that with floating-point arithmetic. Sometimes, though, approximating the correct answer with floating-point isn’t good enough. What if we want an exact intersection test for capsules using only integer arithmetic?
Continue reading Exact (integer arithmetic only) capsule intersection test

Interactive WebGL Demo: Screen-Space Subsurface Scattering

Screen-space subsurface scattering (also known by the amusing acronym SSSSS) refers to a class of techniques for approximating subsurface scattering effects in 3D graphics as a fast postprocessing pass, rather than attempting to accurately model light passing through a translucent material. The original article on screen-space subsurface scattering used a series of blur passes modulated by the depth buffer to fake the detail-blurring effects of subsurface scattering in real time. The diffuse and specular components of reflection in the scene are rendered out to separate textures; only the diffuse layer is blurred, and then the sharp specular shading is composited in afterwards. This is designed to model the multi-layered behavior of many materials, like human skin in the original paper, where light rays either reflect off the surface immediately on contact or penetrate into the material and bounce around before exiting.

I took the sample shader code from that page and translated it into a simple WebGL demo. You need to have a browser that supports WebGL and the WEBGL_depth_texture extension. (Chrome should work, at least.) There are two sliders that let you control the subsurface scattering effect:

  • One slider controls that simulated scattering radius by adjusting the distance between samples for the blur operation. If you turn this parameter up very high, you can get wave-like artifacts near sharp transitions in depth due to the way the depth buffer is factored into the blur operation. Increasing the number of Gaussian blur samples would reduce this effect at the cost of performance.
  • The other slider controls how sharp a depth difference has to be before the shader will stop blurring across that area. If you turn this up to a large value, disconnected areas of the mesh will start blurring into each other, but if you turn it down too low the scattering effect will disappear completely.

Propositional logic proofs are awful

In my last post, I gave an implementation for a program that searches through every proof in a particular proof notation for propositional logic, and collects all the theorems that it finds. The proof formalism used was Hindley–Milner, with types being the formulas of the theory and well-typed lambda terms the valid proofs (per the Curry–Howard correspondence).

The program’s output looked like this: \a. DoubleNegElim (\b. a) : forall a. False -> a. On the right side of the colon, we have our type/theorem: for every proposition \(a\), \(\bot \rightarrow a\). The notation there is about as good as you’re going to get in ASCII text. But then we have the proof, on the left side of the colon. It’s an inscrutable lambda term encoding a natural deduction proof. The type inference engine is filling in the steps in the proof based only on which deductive rules were used, with the result that, even if you know how to read the notation, you really have to stare at it for a while to figure out why the proof works. While this admittedly lends an aura of elegance and mystery to the proceedings, I think I’d prefer a proof that is comprehensible by a human without significant head-scratching.
Continue reading Propositional logic proofs are awful

The shortest proof for every theorem

Suppose we want to show that there is a number \(n\) such that no upper bound on the busy beaver number \(\Sigma(n)\) is provable from, say, the axioms of ZFC. One possible proof is as follows: Assume that no such \(n\) exists. That is, assume that for every \(n\), there is a proof in first-order logic that uses only the axioms of ZFC and derives a sentence \(\Sigma(n) \leq m\) for some \(m\). Then we could compute an upper bound for \(\Sigma(n)\) by exhaustively searching all of the possible valid ZFC proofs until we found one that deduced a theorem of the form \(\Sigma(n) \leq m\); by assumption, we must eventually find such a proof. But we know that we cannot compute an upper bound on \(\Sigma(n)\) for arbitrary \(n\); thus, we have derived a contradiction, and the original assumption must be false.

Enumerating proofs until you find one with the desired properties is one of those grand CS traditions that, like calling an \(O(n^{12})\) algorithm “efficient” while dismissing an \(O(1.001^n)\) algorithm as “intractable”, is handy for theoretical purposes but has essentially no bearing on the real world whatsoever. After all, no one would really write a program that loops through all possible proofs and tests each one.

Continue reading The shortest proof for every theorem

Google Guava makes Java… usable

Hello World! I’m planning to use this blog to collect the various discoveries I make about software development in my day-to-day job as a software engineer at CERTON, Inc. The perhaps-vain hope is that I will help some other poor soul who stumbles across my posts and finds the solution to the exact problem they were encountering at that instant. I’ll also probably post mathematical curiosities and software engineering commentary. The ultimate goal is to keep the quality level high enough that I feel less guilty of time-wasting writing here than if I were participating in the standard social grooming networks.

But, of course, you’re not here for me, you’re here for you. So let’s talk about Google Guava. For the unfamiliar, Guava is a collection of utilities for performing common tasks in Java, similar in spirit to Apache Commons or C++’s Boost. I was introduced to Guava by a fellow CERTON developer for the purpose of performing some set operations more easily in the selection logic in CertSAFE Modeler. Since then, the use of Guava in our codebase has expanded greatly, making it far and away the library we get the most use out of.

Even if you’re already using Guava, there’s most likely parts of it that you’re not using currently only because you don’t know they exist. I know I find myself saying “Wow! I didn’t know Guava had that!” on a regular basis. Here’s a quick list of the most common uses of Guava in the code I write. Undoubtedly there’s things I haven’t listed here because I haven’t discovered them yet—and you might just find something in this list that you wish you had known about a year ago.
Continue reading Google Guava makes Java… usable