Fun with the Value Restriction

This is not a valid OCaml program:

type 'a endo = Endo of int * ('a -> 'a)
let poly = Endo ((succ 23),(fun x -> x))
type thing = { u : unit }
let mono = Endo (0,(fun { u = u } -> { u = u }))
let _ = [mono;poly]

The typechecker rejects it, with this error message:

File "vrmh.ml", line 5, characters 14-18:
This expression has type 'a endo but is here used with type thing endo
The type constructor thing would escape its scope

Removing the last line makes it typecheck. As does exchanging the second and third lines, thusly:

type 'a endo = Endo of int * ('a -> 'a)
type thing = { u : unit }
let poly = Endo ((succ 23),(fun x -> x))
let mono = Endo (0,(fun { u = u } -> { u = u }))
let _ = [mono;poly]

Yes. Notice the mysterious action-at-a-distance. Notice also how the type inferred for poly (see ocamlc -i) is not polymorphic at all, but rather thing endo, the same as mono. Notice further that it would not be possible to define it with an explicit ascription of that type before the definition (i.e., outside the scope) of thing itself. Apparently this is bad.

And then there's the reason why the type of poly didn't have its type variable generalized, thus leaving it with the type '_a endo and subject to unification with the type of mono. This is, of course, the value restriction of ML fame, which I will not explain here; but it's a little more confusing (read: I spent far too much time trying to come up with the mostly minimal test case seen here) (so, yes, this actually is something I ran into in a halfway-real program) in OCaml, where it's been relaxed in certain ways. But not others. For example, this:

type 'a endo = Endo of int * ('a -> 'a)
let poly = Endo (24,(fun x -> x))
type thing = { u : unit }
let mono = Endo (0,(fun { u = u } -> { u = u }))
let _ = [mono;poly]

Is fine.

Wheels Within Wheels

Exhibit A: Hashed and Hierarchical Timing Wheels: Efficient Data Structures for Implementing a Timer Facility, by George Varghese and Tony Lauck, originally in SOSP '87 and later reappeared in 1996 when network protocol research had caught up to it.

Exhibit B: An implementation of hierarchical timing wheels for the fleshy-ape platform, due to David Allen (2002).


(I haven't actually read Getting Things Done, but I have friends who swear by it, some of whom talk to me about it, to which I tend to wind up responding with “oh, that's just locality of reference” or similar.)

Burning Questions Answered

1. The kcore_hdr_t is written by savecore using libkvm.

2. The German owns the zebra.

On the importance of punctuation

Just now I was reading a slashdot article where a bunch of people where whining about some links or other being to some site called “myminicity”. Several mentions of that name later, it finally dawned on me that it was not, in fact, a compound of the usual English state-of-being suffix -ity and some hypothetical trendy nonsense word(s) I hadn't heard of yet (cf. “meme”); but, rather, was to be read as the words “my mini city”.

(I still don't know what the thing actually is, because I don't care.)

If only people had decided to use hyphens when gluing words together for domain names, then I wouldn't have to occasionally waste valuable seconds wondering WTF some string of half-pronounceable letters is supposed to be. (They also wouldn't run the risk of an unfortunate powergenitalia incident, but how often does that happen?) Ah well.

The Sound of Silence

Let's say you have a video file of some sort with no audio stream, and a device that plays video files but can't handle ones with no audio. And you want to use the command-line tool ffmpeg, because you already have a script set up to use it to do whatever transcoding, but for the slight problem of sound.

Maybe you don't, but I did. Know that ffmpeg can take multiple input and/or output files and shuffle them around, in addition to decoding/encoding them. Know also that ffmpeg is documented in a manner both voluminous and not terribly approachable.

The wrong thing to do is to try to figure out how to extract the length of the video track and generate that many audio samples of silence. But, if one hasn't noticed the right part of the man page, this may be what one tries to do. (I did.)

The right thing to do is to use the -shortest flag, which directs ffmpeg to stop whenever any input stream reaches its end, rather than when all inputs are done. Some of you may be (but probably none of you are) thinking of various versions of the Scheme procedure map and their behavior on lists of unequal and/or infinite length, recently a point of contention in the discussion leading up to R6RS. And what is Unix if not a platform for stream processing? (Don't answer that.)

Thus: -f s8 -i /dev/zero -shortest, placed either before or after the regular input file, depending on whether input that does have audio should be silenced or not, respectively.

It's a not entirely inelegant solution to a mildly ridiculous problem.

Quod Erat Covered-In-Bees

Trying to prove something in Coq is like operating a large, fly-by-wire bulldozer. On the one hand, you have to figure out what to shove where, or how to program the machine to do the shoving for you. On the other hand, you can use your superior human pattern-recognition skills to avoid driving into obstacles, and if you do get stuck, you have at least some chance of figuring out how to extricate yourself.

Trying to prove something in ACL2 is like imperiously proclaiming, “Robot servants, hear my command!” and then they run out into the junkyard picking up stuff and moving it around. And if you're lucky, and the task you've given them simple enough, they get the job done for you while you sit back on a lounge chair sipping a strawberry daiquiri. But if that's not the case, they run around doing exactly the wrong thing, until either they explode messily of their own accord or you call in an airstrike. And then you get to examine the flaming wreckage to figure out what went wrong, and what helpful hints you might be able to offer the robots next time.

This Morning's Compiler Meditation:

translating Knuth's “man or boy” test from ALGOL 60 into C, by reifying the activations as structs and closure-converting the call-by-name thunks. Like this.

I considered trying to run it by hand instead, but that would certainly take a lot of paper, and also as Knuth himself apparently failed in that task, I thought perhaps not.