# neelk

## Mar. 28th, 2007

### 09:34 pm - *MMORPG for learning math*

Hippasus is MMORPG designed to teach players math; the magic system for the game is based on solving mathematical problems.

## Mar. 8th, 2007

### 01:19 pm - *Amazing Historical Narrative*

So, my friend Jonathan Walton pointed me to this amazing book on Google Book Search. I'll quote him about it:

Right after the Taiping Rebellion, a former British officer named Augustus Lindley wrote what is basically a pulp version of his (possibly fictional or exaggerated memoirs) of fighting on the side of the Taiping against the British and French forces. It's called Ti-Ping Tien-Kwoh, The History of the Ti-Ping Revolution, Including a Narrative of the Author's Personal Adventures By Lin-Le [Lindley's Chinese Name], Formerly Honorary Officer, Chung-Wang's Guards; Special Agent of the Ti-Ping General-in-Chief; and Late Commander of the "Loyal and Faithful Auxiliary Legion." While Lindley clearly is a product of his time, and his narrative is far from perfect, he gives an amazingly enlightened account of the situation in China and the people he supposedly met. While also FIGHTING RIVER PIRATES! And RUNNING SUPPLIES INTO BESIEGED NANJING! And WINNING THE LOVE OF A PORTUGUESE LADY!

## Jan. 23rd, 2007

## Jan. 11th, 2007

### 10:23 pm - *Random math burbling*

I talked to John today, and realized that my denotational semantics for my little language makes no sense. I'm only half-annoyed by this, because it means that I'll have to learn domain theory properly in order to fix it, and to learn domain theory I need to get comfortable with category theory, because domain theory is a PITA without the language of categories to keep things well-organized. And category theory is something I've been telling myself I should properly learn for, er, ever since I first started here.

As an additional motivation, I talked with jcreed last night, and he showed me his incredibly cool explanation of all possible logical connectives (except conjunction and disjunction). It is clearly *begging* for a treatment using the language of operads, which means that he is cooking up a way to integrate the judgmental approach to defining logics with the categorical. Since these are the only two methods I know to keep myself from designing broken logics, having some way of sanity checking in both directions would be very keen. It would also mean that I could write a paper that only jcreed, John Baez, and Jean-Yves Girard could understand, which would be awesome (if damaging to future career prospects).

Also, a picture of a smiling baby for that sad and tiny minority of people who don't care about formal logic:

## Jan. 3rd, 2007

## Oct. 27th, 2006

## Oct. 19th, 2006

### 10:11 pm

I think I've written the most polymorphic non-toy two-line ML program ever.

val cross : (('a -> 'b -> 'c) -> 'd -> 'e -> 'f) -> (('g -> 'h -> 'i) -> 'j -> 'b -> 'c) -> ('a -> 'g -> 'h -> 'i) -> 'e -> 'd -> 'j -> 'f

Here's the definition:

let cross outer inner f init xs ys = outer (fun x acc -> inner (fun y acc -> f x y acc) ys acc) xs init

It encapsulates a nested iteration over two arbitrary collections. The first two arguments are folds over two different datatypes, the third and forth arguments are the step function and initial argument, and the last two are the two collections. I am tempted to try and generalize this so it's a combinator that lets you iterate over an arbitrary number of collections, but that seems over the top -- I've already got

**10**polymorphic arguments!

## Aug. 20th, 2006

### 12:20 pm - *Book meme*

Via Jim Henley, a book meme:

## Jul. 21st, 2006

### 03:30 pm - *Best discouragement ever!*

"Those both sound like excellent subjects for postdoctoral research."

-- John

## Jun. 26th, 2006

Navigate: (Previous 10 Entries)