Renaissance Grrrl

Over the last few weeks I was interviewed for the Identity Function. The process was quite nice and got me thinking on a number of things. Some of them I may well flesh out into blog posts once I get the time. Of course, that likely won't be until the autumn given everything else going on the next couple months.

I'll be in New York from 28 June through 10 July. The first couple days are for a PI meeting, then I'll get a four-day weekend before LICS, NLCS, and LOLA. Originally the plan was to take a quick trip to Sacramento that weekend for a friend's wedding. (The wedding's still on, but plans changed.) At least this way I'll get a chance to relax, rather than running all over the place. Of course this also means I'll be spending the 4th in NYC. Historically the 4th has been one of my favorite holidays, because it was one I've always spent with friends. I don't know that any of my readers are in NYC, but if you'll be around drop me a line. Or if you used to live there and know fun things to do that weekend, let me know! (Especially any quiet end-of-Pride things.)

Me and L set the date for our final move to the Bay Area: 20 July. And then I start at Google on the 25th. Between now and then: dissertating!!

It's official, I'm heading to Google at the end of July to work with Mark Larson on the Chrome OS security team (of all things!). Seems an unlikely match, but Mark was pretty keen on my background (including the gender stuff!) and wasn't put off by my fusion of linguistics, type-theory, constructive logic/maths, et al. I guess the security team is more concerned with semantic models and constructive correctness than the other teams I talked with. Makes sense, I suppose, but it's sad that these are still thought of as "security" concerns rather than "everything in programming" concerns.

I'm totally looking forward to it, but I am still thinking of it as a bit of an experiment. I'm an academic at heart, so I could see myself heading back to academia in a few years. (Wanting to be a professor is, afterall, what motivated me to start gradschool in the first place.) Then again, I've never really thought of industry as being interested in the sorts of theory I work on. In any case, I'll still be around at the various conferences I've been frequenting; I won't just disappear into industry.

I know a bunch of y'all are in the bay area. I'd love to hear any pointers you have on apartment hunting or on what neighborhoods (nearish Mt View) are nice— i.e., places an artistic disabled radical queer woman might like. Feel free to comment below or get in touch by email, twitter, etc.

In the spirit of Brent's post, I figure I'll make a public announcement that I'm in Vancouver all week attending HOPE, ICFP, and the Haskell Symposium. I love reconnecting with old friends, as well as meeting new folks. Even if I've met you at past ICFPs, feel free to re-introduce yourself as ...things have changed over the past few years. I know I've been pretty quiet of late on Haskell cafe as well as here, but word on the street is folks still recognize my name around places. So if you want to meet up, leave a comment with when/where to find you, or just look for the tall gal with the blue streak in her hair.

Unlike Brent, and unlike in years past, I might should note that I am looking to "advance my career". As of this fall, I am officially on the market for research and professorship positions. So if you're interested in having a linguistically-minded constructive mathematician help work on your problems, come say hi. For those not attending ICFP, you can check out my professional site; I need to fix my script for generating the publications page, but you can find a brief background/research statement there along with the other usuals like CV, recent projects, and classes taught.

The past couple weeks I've been teaching about recursive types and their encodings in B522. Here's a short annotated bibliography for followup reading:

• For a basic intro to recursive types, and for the set-theoretic metatheory: see section IV, chapters 20 and 21.
  • Benjamin C. Pierce (2002) Types and Programming Languages. MIT Press.
• The proof of logical inconsistency and non-termination is "well-known". For every type τ we can define a fixed-point combinator and use that to exhibit an inhabitant of the type:
  • fixτ = λf:(τ→τ). let e = λx:(μα.α→τ). f (x (unroll x)) in e (roll(μα.α→τ) e)
  • ⊥τ = fixτ (λx:τ. x)
• A category-theoretic proof that having fixed-points causes inconsistency
  • Hagen Huwig and Axel Poigné (1990) A note on inconsistencies caused by fixpoints in a Cartesian Closed Category. Theoretical Computer Science, 73:101–112.
• The proof of Turing-completeness is "well-known". Here's a translation from the untyped λ-calculus to STLC with fixed-points:
  • (x)* = x
  • (λx. e)* = roll(μα.α→α) (λx:(μα.α→α). e*)
  • (f e)* = unroll (f*) (e*)
• Knaster–Tarski (1955): For any monotone function, f, (a) the least fixed-point of f is the intersection of all f-closed sets, and (b) the greatest fixed-point of f is the union of all f-consistent sets.
  • Alfred Tarski (1955) A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2):285–309.
  • Bronisław Knaster (1928) Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématique, 6:133–134.
• For a quick introduction to category theory, a good place to start is:
  • Benjamin C. Pierce (1991) Basic Category Theory for Computer Scientists. MIT Press.
• For a more thorough introduction to category theory, consider:
  • Jiří Adámek, Horst Herrlich, and George Strecker (1990) Abstract and Concrete Categories: The Joy of Cats. John Wiley and Sons.
• The Boehm–Berarducci encoding
  • Oleg Kiselyov (2012) Beyond Church encoding: Boehm–Berarducci isomorphism of algebraic data types and polymorphic lambda-terms
  • Corrado Boehm and Alessandro Berarducci (1985) Automatic Synthesis of Typed Lambda-Programs on Term Algebras. Theoretical Computer Science, v39:135–154
• Under βη-equivalence, Church/Boehm–Berarducci encodings are only weakly initial (hence, can define functions by recursion but can't prove properties by induction)
  • Herman Geuvers (1992) Inductive and Coinductive types with Iteration and Recursion. Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 193–217
• However, using contextual equivalence, Church/Boehm–Berarducci encodings are (strongly) initial
  • Neel Krishnaswami (2009) mentions in passing [Better citation needed]
• Surjective pairing cannot be encoded in STLC (i.e., the implicational fragment of intuitionistic propositional logic): see p.155
  • Morten H. Sørensen and Paweł Urzyczyn (2006) Lectures on the Curry–Howard isomorphism. Studies in Logic and the Foundations of Mathematics, v.149.
• However, adding it is a conservative extension
  • Roel de Vrijer (1987) Surjective Pairing and Strong Normalization: Two themes in lambda calculus. dissertation, University of Amsterdam.
  • Roel de Vrijer (1989) Extending the lambda calculus with surjective pairing is conservative. 4th LICS, pp.204–215.
  • Kristian Støvring (2005) Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. BRICS.
• Boehm–Berarducci encoded pairs is not surjective pairing: the η-rule for Boehm–Berarducci encoding of pairs cannot be derived in System F. (The instances for closed terms can be, just not the general rule.)
  • Peter Selinger mentions in passing (p.77) [Better citation needed]
• Compiling data types with Scott encodings
  • Jan Martin Jansen, Pieter Koopman, and Rinus Plasmeijer (200X) Data Types and Pattern Matching by Function Application.
  • Jan Martin Jansen, Pieter Koopman, and Rinus Plasmeijer (2006) Efficient Interpretation by Transforming Data Types and Patterns to Functions. Trends in Functional Programming.
  • Jan Martin Jansen, Rinus Plasmeijer, and Pieter Koopman (2010) Comprehensive Encoding of Data Types and Algorithms in the λ-Calculus. J. Functional Programming.
  • Pieter Koopman, Rinus Plasmeijer, and Jan Martin Jansen (2014) Church encoding of data types considered harmful for implementations. IFL submission
• For more on the difference between Scott and Mogensten–Scott encodings:
  • Aaron Stump (2009) Directly Reflective Meta-Programming. J. Higher Order and Symbolic Computation, 22(2):115–144.
• Parigot encodings
  • M. Parigot (1988) Programming with proofs: A second-order type theory. ESOP, LNCS 300, pp.145–159. Springer.
• Parigot encoding of natural numbers is not canonical (i.e., there exist terms of the correct type which do not represent numbers); though both Church/Boehm–Berarducci and Scott encoded natural numbers are.
  • Herman Geuvers (2014) mentions in passing [Better citation needed]
• For more on catamorphisms, anamorphisms, paramorphisms, and apomorphisms
  • Varmo Vene and Tarmo Uustalu (1998) Functional programming with apomorphisms (corecursion). In Proc. Estonian Acad. Sci. Phys. Math., 47:147–161
  • Erik Meijer, Maarten Fokkinga, and Ross Paterson (1991) Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire. In Proc. 5th ACM conference on Functional programming languages and computer architecture, pp.124–144
    • A translation of Squiggol into Haskell by Edward Yang.
• build/foldr list fusion
  • Andy Gill, John Launchbury, and Simon Peyton Jones (1993) A short cut to deforestation. In Proc. Functional Programming Languages and Computer Architecture, pp.223–232.
  • Many more links at the bottom of this page
• For another general introduction along the lines of what we covered in class
  • Philip Wadler (1990) Recursive types for free!
• "Iterators" vs "recursors" in Heyting arithmetic and Gödel's System T: see ch.10:
  • Morten H. Sørensen and Paweł Urzyczyn (2006) Lectures on the Curry–Howard isomorphism Studies in Logic and the Foundations of Mathematics, v.149.
• There are a great many more papers by Tarmo Uustalu, Varmo Vene, Ralf Hinze, and Jeremy Gibbons on all this stuff; just google for it.

For all you local folks, I'll be giving a talk about my dissertation on November 5th at 4:00–5:00 in Ballantine Hall 011. For those who've heard me give talks about it before, not much has changed since NLCS 2013. But the majority of current CL/NLP, PL, and logic folks haven't seen the talk, so do feel free to stop by.

Abstract: Many natural languages allow scrambling of constituents, or so-called "free word order". However, most syntactic formalisms are designed for English first and foremost. They assume that word order is rigidly fixed, and consequently these formalisms cannot handle languages like Latin, German, Russian, or Japanese. In this talk I introduce a new calculus —the chiastic lambda-calculus— which allows us to capture both the freedoms and the restrictions of constituent scrambling in Japanese. In addition to capturing these syntactic facts about free word order, the chiastic lambda-calculus also captures semantic issues that arise in Japanese verbal morphology. Moreover, chiastic lambda-calculus can be used to capture numerous non-linguistic phenomena, such as: justifying notational shorthands in category theory, providing a strong type theory for programming languages with keyword-arguments, and exploring metatheoretical issues around the duality between procedures and values.

Edit 2014.11.05: The slides from the talk are now up.

Last friday I passed my qualifying examinations! So now, all I have left is a bunch of paperwork about that and then proposing, writing, and defending the dissertation itself. So, in about a year or so I'll be on the job market. And, much as I despise job hunting, I can't wait!

Since defending the quals I've been spending far too much time playing Persona 3 Portable. I've played P3FES, but P3P adds a female protagonist option which changes a bunch of the social interactions, so I've been playing through that side of things. Other than the heterosexual assumptions about the relationships, I've been loving it. More rpgs should have female protagonists. That's one of the reasons I've always loved FF6. Also a big part of why I found FF13 compelling. (Though, tbh: while Lightning is awesome as a protagonist, Vanille is definitely my favorite character :) And a big part of the powerfulness of Kreia as a character in KotOR2 stems from her interactions with the canonically-female protagonist.

Speaking of women. I've been presenting as female for a couple months now, and since I have no intention of stopping nor hiding that fact, I've decided to move T-Day forward. Basically, for those who haven't already switched over to the right pronouns etc: T-Day is today. I've sent emails to the department heads in order to get them to send out the "official" memo; so if you haven't gotten it yet, that should show up on monday or tuesday.

The next couple months are going to be hectic with paper writing. I'm hoping to get a paper on syntax-based sentiment-analysis using matrix-space semantics into one of the CL conferences with deadlines this March. No Haskell involved in that one, though I'll probably spend a few posts discussing the semantic model, which may be of interest to y'all. I'm also planning on getting the work from my first qual paper published; that paper was about Posta, a functional library for interactive/online/incremental tagging with HMMs. Here I'm planning to target journals rather than conferences, and it'll spread out over a few papers: one on the overall system (which I need to actually push up to Hackage), one on the higher-order anytime n-best extraction algorithm, and one on reformulating HMM algorithms in terms of foldl and scanl (this may be combined with the HO-AnB paper, length permitting). All of these would be targeting the linguistics audience. Using folds and scans is old-hat in functional programming; my particular goal with that paper is exposing linguists to the tools of FP and how they can be used to greatly simplify how we describe our algorithms. Once those are out of the way I might also see about writing up a functional pearl on the smoothing library I presented at AMMCS a few years back.

Just got back from MFPS-LICS-CSF saturday night. T'was the first LICS I've been to, and my first time in the deep south. I had fun overall. Definitely enjoyed the French Quarter with its narrower streets, delightful architecture, and other non-American features. And I ran into the Pride parade the day after arriving; I seem to have a knack for that ;) The humidity was killer though.

The slides from my NLCS talk are available here. I've been having some issues with my bibtex2html script, so they're not linked to on the publications page yet; but they will be once I get that issue fixed.

In less happy news, I got some bloodwork back today. Cholesterol is far far too high, and I'm getting into the pre-diabetic range for bloodsugar levels. So, I'm starting a major diet change in hopes of getting those under control. Apparently lack of protein is a big part of the problem (for me), which is ironic since most americans get far too much. Damn midwestern genes. Went grocery shopping today; it's profoundly difficult to get a 1::1 carbs-to-protein ratio as a vegetarian.

Hmm, so I was hoping to get back into blogging over the summer. Y'know, a sort of liveblogging on quals, like how people blog about their Google Summer of Code projects these days. Turns out, some part of my brain is all, "oh noes! blogging is a waste of time! You could be working or, y'know, playing videogames or something!" So that sucks. In part because my brain is stupid, in part because I've been reading so many awesome blogs by people at least as busy as I am and now I feed bad for not measuring up to some impossible standard I made up out of thin air.

So the summer was fun, albeit not relaxing in the slightest. I really need to work on that whole Day of Rest idea. Things that happened this summer:

• Grace and Jason got married! So that's the second California wedding I've been to in as many years. Now I can quit complaining about never having gone to a wedding. It was great to see friends from college again. Of the ones I lost touch with over the years, one works in the game industry (both indie and corporate), and another works for Wolfram Alpha (indeed, with Mr. Wolfram himself). So that's pretty cool.
• Went to NASSLLI in Austin. There were some awesome classes there. Craige Roberts is fabulous; definitely someone to keep an eye on. Got to meet Adam Lopez, who was recently working on stuff related to one of my quals. Adam was part of the Edinburgh SMT crew, who came to JHU shortly after I left so I hadn't met him before. And, of course, got to hang out with Ken and Oleg again. Also, awesome, someone there remembered my talk from NASSLLI 2010 and asked about followup work on it.
• Read a bunch of fun books, or rather had them read to me. Licia got a kindle and loves reading aloud; she's the best ever. Fun books include: Pride and Prejudice and Jane Eyre. Seriously, they are both delightful and if you haven't read them you should. Competent women are the best. Also, Look Me in the Eye: My Life with Asperger's (dude, what a life!), and most of God, No! and Drop Dead Healthy.
• Bought Tales of Graces F on a whim and loved every minute of it. It starts off as your very standard JRPG about childhood friends, but then jumps ahead a few years after everyone has separated and grown up. The prologue is, as the reviews say, the least entertaining part; but it does a good job of setting the background for making the main plot poignant. Just saying people were childhood friends pales in comparison to seeing it and then seeing how they've grown apart. I haven't played any of the other Tales games, but the system is pretty similar to the Star Ocean system. Better done though, IMO. You have the fusion/cooking thing, but it's done in a way that's both extremely helpful and not obnoxious, so you use it regularly and actually care. The combat system is vibrant and engaging, and the system of badges is really cool. Overall the system has a lot of depth but doesn't get in the way of just playing. Some of the reviews complained about uneven difficulty, but I have no idea what they're on about. 10/10
• And in a few weeks I'll be heading off to ICFP again. It'll be the first time I've been to Europe, can't wait.

All last week I was in Tokyo to attend ICFP and associated workshops. It was nice to finally meet a bunch of people I've been talking with online for the last few years. And I met up with Ken Shan and Oleg Kiselyov again, which is always a pleasure. Unlike last time I was in Japan, I didn't get too much time to explore and go sightseeing. I got to explore Chiyoda, which I missed last time around, and I made sure to do two of the most important things: (1) eat some okonomiyaki, (2) visit Akihabara to buy some new manga.

My newest acquisition is 銃姫 ("Gun Princess") Phantom Pain, which I'm rather enjoying so far. Anything that starts off with an execution, spell-casting based on Buddhist mantras, and a prolonged diatribe on why one of the characters is a good-for-nothing incompetent layabout, can't be half bad :) Unfortunately, I only got the first two volumes, so I'll finish them all too soon. So far it's proving easier to read than my previous acquisition (Peace Maker 鐵), though I'm not sure if that's due to getting better at Japanese or because 鐵 is written in a particular style. I definitely noticed my deterioration in fluency since five years ago; grammar's fine, but my vocab is abysmal. I need to find a decent way to work on that.

I've been working on a tagging library (and executable) for a bit over a year now. When the project started I had the advantage of being able to choose the language to do it in. Naturally I chose Haskell. There are numerous reasons for this decision, some of which have been derided as "philosophical concerns". Certainly some of the reasons why Haskell is superior to other languages do border on the philosophical. Y'know, silly little things like the belief that type systems should prevent errors rather than encouraging them to proliferate. I'm sure you've heard the arguments before. They're good arguments, and maybe they'll convince you to try out Haskell in your basement. But in many so-called "enterprise" settings, anything that even smells like it might have basis in theoretical fact is automatically wrong or irrelevant; whatever you do in the privacy of your basement is your own business, but heaven forbid it have any influence on how decisions are made in the workplace! So, here is a short list of entirely pragmatic, practical, and non-theoretical reasons why Haskell is superior to Java for implementing enterprise programs. More specifically, these are reasons why Haskell is superior for my project. Perhaps they don't matter for your project, or perhaps they'll be enough to convince your boss to let you give Haskell a try. Because design decisions are often project-specific, each point explains why they matter for Posta in particular.

• Haskell has powerful frameworks for defining modular, high-performance, non-trivial parsers (e.g., Attoparsec). In natural language processing (NLP), just like system administration, over half of the work you do involves dealing with a handful of different ad-hoc poorly defined file formats. Reading them; generating them; converting from one format to another; etc. Because every one of these formats grew out of a slow accretion of features for one particular project, they're riddled with inconsistencies, idiosyncratic magic values, corner cases, and non-context-free bits that require special handling. In Java the premiere tool (so far as I know) for defining parsers is JavaCC. (Like the C tools lex and yacc, JavaCC uses its own special syntax and requires a preprocessor, whereas Attoparsec and the like don't. However, this may be a "philosophical" issue.) However, as of last time I used it, JavaCC is designed for dealing with nice clean grammars used by programming languages and it doesn't handle inconsistent and irregular grammars very well.
• Posta uses a system of coroutines (called "iteratees") in order to lazily stream data from disk, through the parsers, and into the core algorithms, all while maintaining guarantees about how long resources (e.g., file handles, memory) are held for. This allows handling large files, because we don't need to keep the whole file in memory at once, either in its raw form or in the AST generated by parsing it. For modern enterprise-scale NLP, dealing with gigabyte-sized files is a requirement; because many NLP projects are not enterprise-scale, you get to spend extra time chopping up and reformatting files to fit their limitations. Last time I used JavaCC it did not support incremental parsing, and according to the advertised features it still doesn't. In addition, implementing coroutines is problematic because Java's security model precludes simple things like tail-call optimization--- meaning that you can only support this kind of streaming when the control flow is simple enough to avoid stack overflows.
• Haskell has awesome support for parallelism. One version, called STM, provides composeable atomic blocks (which matches the way we naturally think about parallelism) combined with lightweight threads (which make it cheap and easy). Java has no support for STM. I am unaware of any support for lightweight threads in Java. The only parallelism I'm aware of in Java is the monitor-style lock-based system with OS threads. As with all lock-based systems, it is non-composeable and difficult to get right; and as with using OS threads anywhere else, there is high overhead which removes the benefits of parallelizing many programs.
• Posta makes extensive use of partial evaluation for improving performance; e.g., lifting computations out of loops. When doing NLP you are often dealing with triply-nested loops, so loop-invariant code motion is essential for performance. In my benchmarks, partial evaluation reduces the total running time by 10%. If raw numbers don't convince you: using partial evaluation allows us to keep the code legible, concise, modular, and maintainable. The primary use of partial evaluation is in a combinator library defining numerous smoothing methods for probability distributions; the results of which are called from within those triply-nested loops. Without partial evaluation, the only way to get performant code is to write a specialized version of the triply-nested loop for every different smoothing method you want to support. That means duplicating the core algorithm and a lot of tricky math, many times over. There's no way to implement this use of partial evaluation in anything resembling idiomatic Java.
• Posta uses an implementation of persistent asymptotically optimal priority queues which come with proofs of correctness. A persistent PQ is necessary for one of the tagger's core algorithms. Since the PQ methods are called from within nested loops, performance is important. Since we're dealing with giga-scale data, asymptotics are important. A log factor here or there means more than a 10% increase in total running time. In Java there's java.util.PriorityQueue but it has inferior asymptotic performance guarantees and is neither persistent nor synchronized. I'm sure there are other PQ libraries out there, but I doubt anyone's implemented the exact version we need and shown their implementation to be correct.

I'll admit I'm not up to date on state-of-the-art Java, and I'd love to be proven wrong about these things being unavailable. But a couple years ago when I returned to Java after a long time away, I learned that all the hype I'd heard about Java improving over the preceding decade was just that: hype. I have been disappointed every time I hoped Java has some trivial thing. The most recent one I've run into is Java's complete refusal to believe in the existence of IPC (no, not RPC), but that's hardly the tip of the iceberg.