My superpower is synchronicity

Only recently, thanks to the computer, has it become feasible to solve real, nontrivial problems of reasoning from incomplete information, in which we use probability theory as a form of logic in situations where both intuition and "random variable" probability theory would be helpless. This has brought out the facts in a way that can no longer be obscured by arguments over philosophy. One can always argue with a philosophy; it is not so easy to argue with a computer printout, which says to us: "Independently of all your philosophy, here are the facts about what this method actually gives when applied."

Daaamn. That's some gettin' told right there.

The above quote (emphasis added) is from the eminently readable Probability in Quantum Theory by E.T. Jaynes, which presents a critique and alternative perspective on the role of probability within quantum mechanics. If you've any interest in philosophy of science or the philosophical disputes between frequentism and Bayesianism, even if you've no real knowledge of physics, then I highly recommend reading it. While the frequentist vs Bayesianist argument is well-known of, the details of what is actually at stake are less well-known and often quite subtle. I think the author does a good job of bringing out and highlighting what the argument is about, and why it is relevant to the future of science (especially physics).

For my part, I've been well indoctrinated into the Bayesian philosophy. This semester I'm taking a course on frequentism, or rather on "experimental methods" as they call it. A professor here has been pushing hard for Bayesian methods in behavioral sciences, and the professor of my class delights in teasing him about it (though he admits to no investment in the philosophical debate). It's been a very long time since I've seen the frequentist perspective, and I'm always of the opinion that it's good to keep an eye on one's philosophical enemies. I've known that frequentism has long dominated the behavioral sciences, but I must shamefully admit that I've attributed this to them being "soft" (even for as much as I identify with my undergrad training in anthropology and humanities). However, coming from machine learning where Bayesianism is de rigueur, one thing I found startling about the article is that, apparently, in physics too it's the frequentists who've dominated the conversation for decades. Indeed, as Jaynes portrays it, it's the frequentists who ousted Laplace, rather than the other way around as is portrayed in AI/ML circles.

I finally got around to posting the slides for a talk I gave twice this summer: Probability Smoothing for NLP: A case study for functional programming and little languages. The first version of the talk was presented at the McMaster Workshop on Domain Specific Lanaguages (and Ed Kmett has posted a video of that version on YouTube) with the presentation focused on EDSLs, with smoothing given as an example. The second version was presented at the AMMCS minisymposium on Progress and Prospects in Model-Based Scientific Software Development, where the focus was more on the domain itself and how the use of a DSL allows ensuring correctness, modularity, and maintainability of code for developing probability models. The slides are essentially the same for both talks, with the benchmarks updated a bit in the latter.

As you may have surmised, this is but a small facet of the Posta project I was working on last year. I had meant to submit it as a functional pearl for ICFP, but the timing didn't work out for that. After giving the McMaster version of the talk, Ed convinced me that I should publish the code for the smoothing DSL separately from the rest of Posta. So he's the one to blame about my being so slow in releasing the Posta code I promised this summer. Though seriously, I'd been considering breaking up and reorganizing the code anyways. Now that I'm back from ICFP and all my traveling over the summer, I hope to get that code pushed out soon. Sorry for the delay y'all.

Via silmaril: If you're a dancer, you've heard about isolation. If you're a belly dancer, you've heard a lot about isolation. Well.... Watch this, and weep. In envy, I won't lie.

Oh yes, weeping shall commence.

Last week was a whirlwind. It was the first week of classes, which normally wouldn't be a big thing, except this semester I'm teaching a course. The first couple months of summer were pretty sedate up in Canada. But the last month, leading into the start of fall term, was full of traveling. I came back from Canada for a couple weeks, then left for a week with Licia, came back for a couple days (literally) and then flew off to California for Lindsey and Alex's wedding, arriving home the night before I needed to teach my first 9:30am class. Things've settled down now, though I'm heading off to ICFP next friday.

One thing traveling is good for is getting caught up on pleasure reading. In addition to the Vinge mentioned last time, I also got to read some new C.S. Friedman. After returning from Canada I got a bunch of new games for the PS3 too. Portal 2 is good fun, though the atmosphere feels like a bizarre hybrid between the first Portal and the Fallout franchise; fitting in its way, but very strange. I've also been playing through El Shaddai and reveling in the beauty of Amaros. Unlike a lot of Japanese games, the US version lets you keep the original voice acting, which is fabulous. Dunno how good the English voices are actually; maybe next time I play through it I'll find out. And then there's Catherine: an adult romantic horror by the team who did the Persona series. It's actually a puzzle game, where you're trying to climb a tower that crumbles beneath you. Both the puzzling and the plot are top rate, as to be expected from Atlus and SMT. There are other books and other games, but I'm not feeling like doing any proper reviews just yet.

In addition to teaching, I'm taking two courses this term. Advanced Phonetics, continuing from the Phonetics course I took last spring. Back at Reed for my undergrad we didn't have any phonetics courses, only phonology; so I've been getting caught up on that, as well as filling out the requirements for the Linguistics half of my dual PhD. The other course (Q551) is an intro to cognitive neuropsychology. It's something of a psychology methods course, with a bit of neuroanatomy and the briefest mention of how the imaging technology works. Last spring I took a course on neuroscience for speech and hearing, and up in Canada I spent the summer with a bunch of computer scientists who work on optimizing the algorithms behind the imaging technology; so I'm not sure how much I'll get out of Q551, but it's a requirement for the CogSci half of the dual PhD. As a (meta)theoretical computational linguist, neuroimaging isn't really my area; but as it turns out there are some interesting problems there and plenty of room for theoretical mathematics. Even after the imaging is done, interpreting the images runs into a lot of the same statistical problems that you get in NLP. Both fields are in need of a new statistics, one which doesn't break down when you have enormous data sets. Maybe one day I'll try working on that.

An Atlanta area mother was recently convicted of vehicular homicide. Convicted for the crime of being a pedestrian hit by a drunken driver, a driver who was also on painkillers, also half blind, also convicted of two previous hit-and-runs. Her child was also hit, and killed, which is why she's now a criminal. In truth, she was convicted for the crime of being black and poor in America. I haven't been in the country six hours and this is the news story that greets me. Racism, the othering of people who take public transit, and the deadly violent car culture that dominates the US.

A (white) friend of mine was killed in a crosswalk in Portland years ago. The SUV driver couldn't be bothered to check if it was safe when making a left-hand turn across a busy street, at full speed without slowing at all. There were witnesses. He also fled the scene. She was headed to the corner to next to her apartment to buy a mop.

I've been hit three times in crosswalks, all three with the walk sign on and a red light for the cars. Only one of those times was it serious. But I was saved by the fact that the rich white man was driving a sporty little thing so I went over the hood instead of under.

What a welcome home.

unification-fd 0.5.0

The unification-fd package offers generic functions for first-order structural unification (think Prolog programming or Hindley–Milner type inference). I've had this laying around for a few years, so I figured I might as well publish it.

An effort has been made to try to make this package as portable as possible. However, because it uses the ST monad and the mtl-2 package it can't be H98 nor H2010. However, it only uses the following common extensions which should be well supported[1]:

Rank2Types
MultiParamTypeClasses
FunctionalDependencies
FlexibleContexts
FlexibleInstances
UndecidableInstances

[1] With the exception of fundeps which are notoriously difficult to implement. However, they are supported by Hugs and GHC 6.6, so I don't feel bad about requiring it. Once the API stabilizes a bit more I plan to release a unification-tf package which uses type families instead, for those who feel type families are easier to implement or use.

Description

The unification API is generic in the type of the structures being unified and in the implementation of unification variables, following the two-level types pearl of Sheard (2001). This style mixes well with Swierstra (2008), though an implementation of the latter is not included in this package.

That is, all you have to do is define the functor whose fixed-point is the recursive type you're interested in:

    -- The non-recursive structure of terms
    data S a = ...
    
    -- The recursive term type
    type PureTerm = Fix S

And then provide an instance for Unifiable, where zipMatch performs one level of equality testing for terms and returns the one-level spine filled with pairs of subterms to be recursively checked (or Nothing if this level doesn't match).

    class (Traversable t) => Unifiable t where
        zipMatch :: t a -> t b -> Maybe (t (a,b))

The choice of which variable implementation to use is defined by similarly simple classes Variable and BindingMonad. We store the variable bindings in a monad, for obvious reasons. In case it's not obvious, see Dijkstra et al. (2008) for benchmarks demonstrating the cost of naively applying bindings eagerly.

There are currently two implementations of variables provided: one based on STRefs, and another based on a state monad carrying an IntMap. The former has the benefit of O(1) access time, but the latter is plenty fast and has the benefit of supporting backtracking. Backtracking itself is provided by the logict package and is described in Kiselyov et al. (2005).

In addition to this modularity, unification-fd implements a number of optimizations over the algorithm presented in Sheard (2001)— which is also the algorithm presented in Cardelli (1987).

• Their implementation uses path compression, which we retain. Though we modify the compression algorithm in order to make sharing observable.
• In addition, we perform aggressive opportunistic observable sharing, a potentially novel method of introducing even more sharing than is provided by the monadic bindings. Basically, we make it so that we can use the observable sharing provided by the previous optimization as much as possible (without introducing any new variables).
• And we remove the notoriously expensive occurs-check, replacing it with visited-sets (which detect cyclic terms more lazily and without the asymptotic overhead of the occurs-check). A variant of unification which retains the occurs-check is also provided, in case you really need to fail fast for some reason.
• Finally, a highly experimental branch of the API performs weighted path compression, which is asymptotically optimal. Unfortunately, the current implementation is quite a bit uglier than the unweighted version, and I haven't had a chance to perform benchmarks to see how the constant factors compare. Hence moving it to an experimental branch.

I haven't had a chance to fully debug these optimizations, though they pass some of the obvious tests. If you find any bugs, do be sure to let me know. Also, if you happen to have a test suite or benchmark suite for unification on hand, I'd love to get a copy.

References

Luca Cardelli (1987)

Basic polymorphic typechecking. Science of Computer Programming, 8(2): 147–172.

Atze Dijkstra, Arie Middelkoop, S. Doaitse Swierstra (2008)

Efficient Functional Unification and Substitution, Technical Report UU-CS-2008-027, Utrecht University.

Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry (2005)

Backtracking, Interleaving, and Terminating Monad Transformers, ICFP.

Tim Sheard (2001)

Generic Unification via Two-Level Types and Paramterized Modules, Functional Pearl, ICFP.

Tim Sheard and Emir Pasalic (2004)

Two-Level Types and Parameterized Modules. JFP 14(5): 547–587. This is an expanded version of Sheard (2001) with new examples.

Wouter Swierstra (2008)

Data types a la carte, Functional Pearl. JFP 18: 423–436.

Links

• Homepage: http://code.haskell.org/~wren/
• Hackage: http://hackage.haskell.org/package/unification-fd
• Darcs: http://community.haskell.org/~wren/unification-fd
• Haddock: Darcs version

I've mentioned these a few times in different places, most recently on Reddit. So I figured I should repost them here for better googleability for folks just starting to learn about dependent types and type theory.

PSA #1: Beware: "type theory" and "Type Theory" are not the same thing, note the caps. The former describes the entire field of enquiry which explores possible theories about types; the latter is the name of one particular theory/system, namely the one Per Martin-Löf popularized (and others have extended and reinvented since then).

Yes, this is an extremely obnoxious detail, but it's one that often confuses newcomers; e.g., learning MLTT and thinking that applies to all type systems, or learning other type systems and then being confused when people make flagrantly false statements (when interpreted as statements about type theory as a whole, though they're true of MLTT). This is why I prefer to refer to Type Theory as "TT" or "MLTT", to avoid confusion, and because I am interested in the entire field of enquiry and in comparing different systems rather than focusing on just one.

ObTangent: There are similar reasons for why ML is called "ML" instead of "metalanguage".

PSA #2: There are conflicting meanings for the terms "sum" and "product" in dependent type land. Those coming from category theory and functional programming tend to say "sum" to mean tagged unions, "product" to mean pairs (e.g, cartesian products or similar), and "exponentials" to mean functions as objects— all of these exactly as in non-dependent languages. However, those coming more from the set-theory side of things use "product" to mean functions (whence the capital Pi), "sum" to mean pairs (whence the capital Sigma), and have no common term for unions.

Immutability and Blocks, Lambdas and Closures (André Pang): Mr. Python, please call the office. Your abstractions are leaking.

Last week I gave a debugging problem. Well, now it's time for the big reveal. If you'd like to try your hand at it, you should follow that link and stop reading this post. It took me a couple weeks to figure this one out. Given the nature of the symptoms (failure only on messages of lengths 255 and 383) it was pretty clear that this was some obscure and annoying bug, like an off-by-one error. I read through the relevant code for the whole communication stack (Haskell protobufs, Haskell FIFO IO, Java FIFO IO, Java protobufs) with a inkling of what the problem might be, but I still missed it the first time through.

In the hints I suggested that length 511 should also be problematic, and that we were using the length-delimited version of protobufs. For those who aren't familiar with protobufs there are only two relevant details of the encoding. The first is that length-delimited protobufs write the length before the payload (as mentioned in the hint), and the second is how that length is encoded. In order to reduce the message size, protobufs use a variable length encoding for integers. The encoding says that we read a byte at a time (little-endian order), keeping the low-order 7 bits as part of the number. If the 8th bit is unset, then we're done; if it's set, then we continue reading the next byte. Thus, the length 255 is encoded as 0xFF 0x01 ((0xFF .&. 0x7F) .|. (0x01 `shiftL` 7) == 255), 383 is encoded as 0xFF 0x02, and 511 is encoded as 0xFF 0x03. Conversely, the non-problematic 254 is encoded as 0xFE 0x01, and 256 is encoded as 0x80 0x02.

The crucial knowledge, however, is knowing that for some unfathomable reason Java decided to define their byte type as a signed numeric type! On the one hand, this is perverse because bytes are always used when dealing with binary formats and almost never used for actual numerical computation. On the other hand, it is sadistic because every other language in common use (and most of the ones not in common use) have unsigned bytes, so Java's choice to use signed bytes is exquisitely designed to confound any programmer who has ever used another language. More particularly, this means that the implicit conversions between bytes and other numeric types will preserve the signed value, not the representation. Thus, since 0xFF has the signed byte value -1, whenever you use this byte in, say, an int context, it will be silently and implicitly converted into the int -1 as opposed to the int 255 any sane person would expect. Further, since Java comes from the C tradition of languages, it likes to use magical values to indicate errors (e.g., using -1 when only positive values are valid). I'm sure you can see where this is headed.

The InputStream class is one of the plethora of classes for reading from a file. In particular, it's the one used by the CLIPC library for reading from Posix FIFOs. Another awful thing about Java is that it refuses to believe in anything that systems programmers use, because by definition these things aren't portable to every operating system. I believe I've alluded to this before. Among other things it means that Java steadfastly refuses to acknowledge the fact that separate processes can communicate without going through the network stack. If you want RPCs, then there are numerous options available to you. But heaven help you if you want to use IPC in order to avoid that overhead. And don't get me started on signal handling. Luckily for me, CLIPC does the nasty JNI coding necessary to convince Java to believe in FIFOs (and it even works for Windows FIFOs).

Subclasses of InputStream provide a method which allows you to read one byte at a time from wherever it reads from. However, this method has the type int read() where the return value -1 indicates end of file and values 0 through 255 indicate the byte that was read. This is just begging for bugs. You can't just return a byte, since all the bytes from 0x80 to 0xFE (-128 to -2) will be implicitly converted into invalid return values, and the byte 0xFF (-1) will be implicitly converted to EOF.

Using the standard trick for amortizing IO costs, the CLIPC library reads a buffer's worth of data whenever it needs to, and then returns that data as requested. That buffer has the exceptionally reasonable type byte[]. Unfortunately, when reading a single byte it does this innocuous little thing: int returnValue = buffer[i];. Very easy to miss when scanning though hundreds of lines of Java, even when you have an inkling that signed bytes may be at fault. This is why implicit conversion between numeric types is Evil. Haskell does the right thing in requiring all coercions to be explicit. To fix the bug we must do: int returnValue = ((int) buffer[i]) & 0xFF;. Unfortunately, the buffer field is private in FIFOInputStream so I can't make a subclass to fix the bug.

Surprisingly, except for the interpretation of 0xFF as EOF when reading the length header, Google's protobuf code works perfectly fine with all the other errorful byte values since it uses bytewise operations instead of arithmetic. And reads chunks at a time elsewhere, thus avoiding the bug. Good job Google :)

I've sent a bug report to the author of CLIPC, but I've yet to hear back, and cursory googling indicates he may have dropped off the internet a couple years ago. If I haven't heard back by the time I make the first public release of Posta (estimated mid--late May 2011), then I'll have to fork CLIPC since I don't want Posta's license to be dictated by this externality. LGPL 2.1+ is great and all, but this bug is a silly thing to base a license around.

unix-bytestring 0.3.2

The unix-bytestring package offers a full selection of Unix/Posix-specific functions for reading and writing ByteStrings to file descriptors.

The Story Behind It All

A while back I needed a ByteString-based version of the System.Posix.IO String-based API. I coded up the new versions and submitted a patch to the unix package for adding them in. But apparently, noone's much pleased with the System.Posix.IO API! In the ensuing discussion folks brought up their specific complaints and offered suggestions. So now, the couple of functions have become enough to release as its own package— with the hope that one day it'll be rolled into the unix package.

That's where you come in. The current API is more than good enough for anything I've needed, so I need your feedback on what you want from a ByteString-based Unix/Posix I/O library.

I've looked through Roel van Dijk's reverse dependency analysis to find the folks currently using the unix package. The maintainers of the following packages may be particularly interested in unix-bytestring:

• HFuse
• iteratee
• iteratee-mtl
• liboleg

HFuse has complained about the lack of bindings for pread(2) and pwrite(2), which are included in unix-bytestring. The only standing complaint I haven't addressed is one expressed in the iteratee, iteratee-mtl, and liboleg packages which would prefer a return type of (Either Errno _) instead of throwing exceptions.

Links

• Homepage: http://code.haskell.org/~wren/
• Hackage: http://hackage.haskell.org/package/unix-bytestring
• Darcs: http://community.haskell.org/~wren/unix-bytestring
• Haddock: Darcs version