If you’re wondering what I’ve been up to lately, and type theory doesn’t scare you away: I’ve been working on the homotopy type theory project, which is approximately an attempt to make sense of the higher-dimensional structure latent in Martin-Löf type theory, which is closely connected with ideas from higher category theory and homotopy theory.

In particular, I just posted on the Homotopy Type Theory blog this thing I’ve been working on. I also have some posts (for this site) in the pipeline, so stay tuned.

I’ve been reinstalling Ubuntu (11.04, Natty Narwhal) a lot lately, because my computing environment is in a lot of flux right now. I wiped my desktop computer, have a relatively new laptop, had a laptop at Intel, and now have a desktop at CMU.

As a result, my package installation routine is more or less down to a science right now. Here are the packages I am sure to install–and sure to uninstall–right at the start, along with brief commentary.

apt-get install

• zsh — my shell of choice.
• vim exuberant-ctags — necessary for editing all manner of text file.
• haskell-platform — Haskell, with batteries included.
• texlive-latex-extra (and hence, most of the other LaTeX packages) — I use LaTeX whenever I need to format text.
• subversion git — these come in handy, even if you don’t use one (or both) of these yourself.
• gdebi gparted rar gv — I always find myself using these at random times. (The rar package also enables RAR support in many other programs.)
• compizconfig-settings-manager — to tweak the default Ubuntu settings for window animation, etc.
• gnome-do — like Quicksilver or Spotlight.
• nautilus-open-terminal — adds “Open in Terminal” to your context menu.
• vlc — plays all media files.
• gimp — mostly to convert and resize images. (Alternative: imagemagick.)
• cmus — my favorite library-based music player.
• exfalso eyed3 — edit mp3 tags, before importing into library. I use exfalso for the text fields, and eyed3 to add album art.
• deluge — a good BitTorrent client.
• virtualbox-ose — for virtualization.
• libncurses5-dev — needed for Petite Chez Scheme, below.

Other things to install

• Google Chrome, from official .deb, so it adds the Chrome repository.
• Petite Chez Scheme, for Scheme.

apt-get remove

• unity ^unity-* — I don’t like the new Unity UI.
• shotwell tomboy ubuntuone-client — I don’t want these programs.
• empathy empathy-common — I prefer Pidgin, if I end up using IM.
• gwibber gwibber-service-* — really?
• transmission-common — I prefer Deluge.

If you want exactly the above, you can just run:

sudo apt-get install zsh vim exuberant-ctags haskell-platform texlive-latex-extra subversion git gdebi gparted rar gv compizconfig-settings-manager gnome-do nautilus-open-terminal vlc gimp cmus exfalso eyed3 deluge virtualbox-ose libncurses5-dev

sudo apt-get remove unity ^unity-* shotwell tomboy ubuntuone-client empathy empathy-common gwibber gwibber-service-* transmission-common

Back when I started this website (in 2006!) it was essentially a social outlet with relatively little substance, except for occasional meaningless blatherings about math. Since then, things have changed–WordPress became a legitimate platform, Facebook took over the world, Twitter took over meaningless blathering–and my blog, for better or for worse, lay wasting away.

Perhaps it’s time for an online reinvention. (I know I say that about my blog every six months, but I mean it this time…?) My offhand personal comments have indeed migrated to Facebook and Twitter, but I feel that I should accelerate production of public, long-form, intellectual remarks.

As a heads-up, these will largely focus on math and/or programming language theory, a field I will be studying for the next n years as I pursue a Ph.D. in Computer Science at Carnegie Mellon University. I have a number of ideas in my idea bag, but I’ll try to queue some up so that once I start blogging again, I’ll really blog like I mean it.

In preparation, I have made some behind-the-scenes changes to this blog recently. I went through my entire catalog of posts, most of which were sadly from 2006 and 2007, and reorganized them in an Academic/Personal dichotomy and added relevant tags. I then went ahead and hid all of my pre-2008 posts, because they didn’t really do much besides dramatically skew my tag cloud. Lastly, I added plugins for LaTeX and syntax highlighting (SyntaxHighlighter Evolved), and stole Adam Foltzer’s useful Scheme brush for the latter.

Now all I need is content!

This one really confused me for a bit, and then it all made sense. See if you can figure it out. Remember that, for cons pairs, eq? tests pointer equality. (I’m using Chez Scheme 8.0, but that shouldn’t matter.)

> (define ls (iota 5))
> ls
(0 1 2 3 4)
> (define ls2 (cons -1 ls))
> ls2
(-1 0 1 2 3 4)
> (eq? (cdr ls2) ls)
#t
> (set-cdr! ls '(1))
> ls
(0 1)
> ls2
(-1 0 1)
> (eq? (cdr ls2) ls)
#t


On the other hand,

> (define ls (iota 5))
> ls
(0 1 2 3 4)
> (define ls2 (cons -1 ls))
> ls2
(-1 0 1 2 3 4)
> (eq? (cdr ls2) ls)
#t
> (set-cdr! ls2 '(0))
> ls
(0 1 2 3 4)
> ls2
(-1 0)
> (eq? (cdr ls2) ls)
#f


Why is it that the first example mutates both ls and ls2, and the second example only mutates ls2?

In Compilers this semester, we’re making heavy use of a powerful Scheme match macro which includes a ,[Cata -> Id] syntax for inline calls to helper functions. However, the default vim syntax highlighting for Scheme flags -> as a syntax error, because it is an invalid identifier. It also fails to syntax-highlight match itself, and a number of other helpful macros that we’re using, like define-who.

To get around this problem without write access to the actual syntax file itself (located at /usr/share/vim/vim72/syntax/scheme.vim in the burrow) you can simply create an additional syntax file called ~/.vim/after/syntax/scheme.vim. This file will be automatically loaded after the default Scheme syntax, whenever a Schemely buffer is loaded. I put the following lines in my file:

syn keyword schemeSyntax define-who match ->
syntax region schemeMultilineComment start=/#|/ end=/|#/ contains=schemeMultilineComment

This also fixes the problem that, in the default Scheme mode, #| and |# are not treated as comment delimiters. Of course, you can add any personal macros to the list of syntax keywords.

One last problem: I’m using Aaron Hsu’s ChezWEB framework, and he uses .w as the extension for ChezWEB source files, which ought to be highlighted as Scheme source. Add this line to ~/.vimrc to load Scheme syntax whenever a .w buffer is loaded:

au BufNewFile,BufRead *.w set filetype=scheme

Toward the end of last semester, I was busy sending out transcripts to graduate programs, and noticed some trends in the courses I’ve taken. Unsurprisingly, they have leaned more and more toward computer science, and away from every other field, including math. Upon further inspection, my transcript actually offers an apt perspective of my interests throughout college.

Here’s a graph of credit hours per department, per semester. I think it tells a good story. (Click through for a slightly larger version.)

In the past few weeks, I’ve switched audio players from Songbird to cmus, an ncurses-based console player. I know, it sounds ridiculous, but hear me out:

cmus has vi-style key bindings: j/k are down/up, :q quits, etc. It opens instantly, is very responsive, and has a small footprint. It also has support for remote commands via cmus-remote, and even has a last.fm plugin. If Linux is your primary operating system and you like the terminal, you should give it a try.

It even has a Debian package, but unfortunately, stable is back at version 2.2.0, and the current version (2.3.3) has some significant improvements. I compiled the new version, which links with a lot of codec libraries I had to download (libao2, libflac, libwavpack, libvorbis…).

But I ran into a weird issue where some albums’ artists were showing up as blank or weird garbage strings instead of the correct names; Songbird didn’t have this issue. I’m an obsessive music tagger, so this really upset my sensibilities.

cmus 2.3.3 displays the Album Artist field rather than the Artist, in order to better handle compilations. (This is reasonable, because it sorts by Album second, so it is preferable if each album is only under one artist name.) In the ID3 spec, the TPE1 field represents a “lead artist,” and is typically interpreted as the Artist field; TPE2 is the “band/orchestra/accompaniment” field, but is often interpreted as the Album Artist (most notably, by iTunes).

There is a dearth of good ID3 tag editing software, especially on Linux. I primarily use EasyTAG, but it doesn’t support editing TPE2! When a track doesn’t have a TPE2 field, cmus goes by the TPE1 field, and all is well. However, when a file has weird stuff already in TPE2, I get random garbage in cmus.

I fixed this by using mid3v2, a command-line program that allows editing any ID3v2 frame. I can simply type

mid3v2 –TPE2 “Transatlantic” ~/Music/SMTPe/*.mp3

and it solves my tagging problem! It took me a while to figure out exactly what was going on, but now everything is going smoothly. I might switch from EasyTAG to Ex Falso, a GTK-based tag editor (based, like mid3v2, on the Mutagen library) which looks a lot more featureful.

A while back, on a whim, I asked my tweeps and Facebook friends “What do you call the # symbol?” For some reason, everybody is really excited about #, and all in all, I received 7 responses on Twitter and 24 on Facebook. Some of you are indecisive, so of those 32 responses (counting myself), there were 48 total answers.

I only recently got around to counting up the results, and of those 48, I grouped them into six essentially different responses:

• pound (or pound sign, or “pound that shit bro”),
• hash (or hatch),
• number (or number sign),
• sharp,
• octothorpe,
• and a few other responses (tic-tac-toe board, and 0×23).

Many respondents seemed to have a primary answer, followed by caveats (e.g., “Pound, except in music, where it’s a sharp.”) so I differentiated between the primary and subsequent responses for each person. The following graph shows the results, where dark blue indicates primary responses, and light blue indicates all subsequent responses.

If you want the raw responses for some reason, and you don’t want to cull it yourself from my Twitter and Facebook, I can send you a spreadsheet. Graph is courtesy of the Google Charts API, which is a pretty sweet way to make easily-modified charts. (Check out the image URL if you’re curious how it works. I wrote a trivial Perl script to make it easier to incrementally edit the parameters and view the results.)

There are two schools of thought when it comes to text editing: vim and emacs. Although the “official” text editor of IU’s Computer Science department is emacs, I am a die-hard vim user. (If you have no idea what I’m talking about, this post isn’t for you.)

I think emacs has a perfectly fine control scheme, and is certainly a very powerful program, but I prefer the simplicity of vim’s modal input. Many vim users, however, seem unaware of many things that vim can do. (Many emacs users, similarly, seem to think vim isn’t capable of emacs-like tricks.)

But I am here to dispel these false notions! Here’s a list of many possibly-lesser-known vim tricks, many of which I use on a daily basis. They aren’t complicated, so you don’t need to know much about vim to figure them out. If you have any other tips, leave them in a comment. If you don’t know how to use vim but want to find out, type “vimtutor” at a command line and read the instructions.

Multipliers: Prefixing any command with a number causes that command to occur that many times. If you want to write the character ‘x’ 80 times, just type 80 i x [ESC] and the character x will be inserted 80 times. This works for all sorts of things.

Actions and motions: You might be unaware, but actions like delete (d), change (c), and yank (y) take “motions” as an argument of sorts. Motions include end of file (G), start of line (^), end of line ($), next word (w), and matching brace (%). Executing any of these motions as a command causes the cursor to immediately jump to that location. (If the cursor is on a parenthesis, square bracket, or curly brace, % jumps you to the matching one, whether before or after.) Their true power comes when you combine them with actions, however: d% deletes the matching braces and everything in between; cG deletes the rest of the file and places you into insert mode; yw will copy the next word. In Scheme, I’ve found d% and y% indispensable for moving around S-expressions.

Repeat last command: The . command repeats the last thing you did. If your last action was to delete the current line, . will delete the new current line. That’s all.

Navigating directories/archives: If you open a directory or archive in vim, it will show a file listing. You can move up and down the list as usual, but if you hit Enter, it will open the file/directory that your cursor is on. If you’re in an archive, it extracts a copy into a temporary directory.

Make: The command :mak or :make runs “make” in the current directory, showing you the result. If there are any compile errors, vim will automagically jump your cursor to the first one, even if it’s in a different file. The command :cn gets you to the next error, and :cN to the previous. This drastically reduces the time it takes to compile and fix errors, and is definitely the most useful tip here for any C programmers.

TOhtml: Your files are syntax highlighted when you view them in vim. But what if you want a syntax-highlighted copy of your file to distribute to others? Use the command :TOhtml, which opens a new edit buffer with an HTML syntax-highlighted version of your file, ready to save. If you prefer CSS instead of <font> tags, which you should, then first use the command :let html_use_css=1 or, better yet, put it in your .vimrc file so it’s always set.

Searching: To find a string in a file, use / followed by that string. For instance, /char [Enter] will jump you to the next occurrence of “char.” The setting :set hlsearch (best placed in your .vimrc) causes vim to highlight every matching search occurrence in the file. Simply typing / [Enter] will get you to the next one. :noh turns off the highlighting.

Indentation: If you want to indent with spaces instead of tabs, set expandtab in your .vimrc. Either way, set both shiftwidth and tabstop to the desired size of your tabs. To reindent the current line, use the command ==. A single = is an action, so =G will reindent every line from the current one to the end of the file. gg=G will therefore reindent your entire file. (gg moves to the beginning of the file.)

Splitting: You can edit multiple files side-by-side in a single instance of vim. Type in :sp for a horizontal split, or :vs for a vertical split, followed by the filename you want to open. You can further split either of these new windows. ctrl-W followed by an arrow key (or h, j, k, l) moves your cursor between files. Commands like :e, :w, and :q only affect the active split. (For instance, to close one file and continue editing the others, type in :q while that window is active.

This is just a small subset of vim’s features. I try to learn something new every week. By slowly adding more features to your repertoire, you’ll get increasingly efficient with your editing, without any additional thinking. And after all, that’s the goal with any text editor.

This short excerpt started off an essay which will never see the light of day. I hope to eventually have a suitable way to complete this idea, but until then, maybe somebody will find it good food for thought. (You may also substitute “mathematics” for the theoretical subject of your choice, with varying degrees of success.)

In mathematics, a proof is no more than a convincing argument of a statement’s validity. But as justification for a theorem, a proof alone is wanting. Why state one theorem over another?

The metric of real-world utility seems not to apply. After all, the very objects of study are, in some sense, artificial.

But the allure of mathematics–to me, at least–is how well those objects fit together: the degree to which mathematics unifies apparently different concepts is staggering. Perhaps nobody said it better than G.H. Hardy in A Mathematician’s Apology: “The ‘seriousness’ of a mathematical theorem lies in…the significance of the mathematical ideas it connects.”

If research mathematics is about connecting ideas, surely math education ought to convey that interconnectedness. On the contrary; until reaching senior-level courses, mathematics appears an amalgam of essentially disparate concepts.