I’ve started using lenses for my projects, and am climbing the learning curve of the new idioms. The forward chaining `&` operator (`|>` in F#) is particularly important to grasp, as without it the infix operators of the library are extremely awkward.

Here’s a simple example of `&` chaining together several updates:

```{-# LANGUAGE TemplateHaskell #-}
import Control.Applicative
import Control.Lens

data Foo = Foo { _bar :: Int, _baz :: Bool, _quux :: String }
deriving Show

makeLenses ''Foo

testFoo :: Foo
testFoo = Foo { _bar = 5, _baz = False, _quux = "Hello" }

mungedFoo :: Foo
mungedFoo = testFoo & bar  .~ 6
& quux .~ "Goodbye"
```

But what if we want to do the same thing with monadic (or applicative) values? Without lenses, we might use an awkward anonymous function:

```mayMungeFoo' :: Maybe Foo
mayMungeFoo' = (\b q -> testFoo { _bar = b, _quux = q})
<\$> return 6
<*> return "Goodbye"
```

But with lenses, we can use our old familiar `>>=` along with `%%~` from the lens library to get something nice back:

```mayMungeFoo :: Maybe Foo
mayMungeFoo = testFoo & bar  %%~ const (return 6)
>>= quux %%~ const (return "Goodbye")
```

I can’t find a way to make this work with just an `Applicative` constraint, but the pattern is useful enough that I might have to think up a new operator name for composition of a lens with `const`.

December 7, 2012 at 2:45 pm

Posted in Code

Tagged with ,

A Meta-Scheduler for the Par-Monad will appear in ICFP 2012!

I’ve just received the happy word that my paper on heterogeneous parallelism in Haskell with Abhishek Kulkarni, Rebecca Swords, Sajith Sasidharan, Eric Jiang, and Ryan Newton will be appearing in ICFP 2012! Here’s a draft pdf, and Ryan’s blog post with an example of CPU+GPU computation.

I’m quite excited; this paper closed out my Master’s studies, and was the first I submitted to a conference. The anonymous reviewers were extremely generous with their time, and we have a good deal of strong feedback to work into the camera-ready version.

Of course, we’re also moving to Portland next month, so this promises to be a busy time!

May 28, 2012 at 11:03 pm

Moving to Portland and joining Galois

with one comment

I’m excited to announce that after Bethany and I finish our degrees in May, we’ll be heading back to Portland where I’ve accepted an engineering position at Galois, Inc. I’m thrilled to be headed back after such a great experience as an intern there last summer.

It’s bittersweet to be moving on from IU, where I’ve been privileged to be friends and learn with the outstanding Programming Languages Group and be mentored by superstars like Dan Friedman, Amr Sabry, Will Byrd, and Ryan Newton. Without their friendship, support, and wisdom, there’s no chance I’d now be looking forward to such unique and rewarding work.

I hope the switch from academia will leave more cycles available for this sorely neglected space. I’ve had some exciting projects on the back burner for a while now that deserve some more of my attention. For now, though, one more semester to go, and then on to adventure (and food carts)!

February 10, 2012 at 7:08 pm

Posted in FYI, Portland

A lot of IU course work is making the leap to git, so it’s worth quickly pointing out this great resource: git ready » learn git one commit at a time.

It splits out guides by skill level, and makes them focused enough that it’s more of a cookbook than a tutorial. As you’re working, just keep it open in a tab for call-by-need reference.

September 15, 2011 at 2:01 pm

Posted in Code, FYI

Tagged with

Tech talk: Combining Denotational and Operational Semantics for Scalable Proof Development

A few weeks ago, I had the opportunity to give a tech talk at Galois derived from one of the most memorable lectures at the Oregon Programming Languages Summer School. Here’s the abstract, the video of my talk, and the Coq developments I adapted from Greg Morrisett’s materials:

Interpreters offer a convenient and intuitive way for programmers to reason about language behavior through denotational semantics. However in a setting like Coq, where all recursive functions must provably terminate, it is impossible to write interpreters for non-terminating languages. The standard alternative is to inductively define operational semantics, but this can yield proofs that are difficult to automate, particularly in the presence of changing language features.

This talk presents a combined approach, where an interpreter is used in combination with operational semantics to prove type preservation of a small functional language. To demonstrate the scalability of the Coq development, let expressions and a pair types will be added and preservation will be proved again with only one extra line of proof script.

Coq development sources

August 10, 2011 at 1:25 pm

with one comment

For years I had no idea that Scott Adams was a horrible human being, and enjoyed his bad jokes through the comic’s RSS feed. Lately his blog writing as gotten a bit more attention.

A couple months ago, he posted and then later deleted a blog post with such gems as:

The reality is that women are treated differently by society for exactly the same reason that children and the mentally handicapped are treated differently. It’s just easier this way for everyone. You don’t argue with a four-year old about why he shouldn’t eat candy for dinner. You don’t punch a mentally handicapped guy even if he punches you first. And you don’t argue when a women tells you she’s only making 80 cents to your dollar. It’s the path of least resistance. You save your energy for more important battles.

Even though he has a slavering horde of followers ready to explain how his critics lack reading comprehension skills, he still felt the need to engage in sock-puppetry to prop up his awful views. Upon being discovered:

I’m sorry I peed in your cesspool. For what it’s worth, the smart people were on to me after the first post. That made it funnier.

His latest intellectual treatise concerns the plight of males, doomed by nature to be unhappy because society suppresses our natural rapin’ instinct:

Powerful men have been behaving badly, e.g. tweeting, raping, cheating, and being offensive to just about everyone in the entire world. The current view of such things is that the men are to blame for their own bad behavior. That seems right. Obviously we shouldn’t blame the victims. I think we all agree on that point. Blame and shame are society’s tools for keeping things under control.

The part that interests me is that society is organized in such a way that the natural instincts of men are shameful and criminal while the natural instincts of women are mostly legal and acceptable. In other words, men are born as round pegs in a society full of square holes. Whose fault is that? Do you blame the baby who didn’t ask to be born male? Or do you blame the society that brought him into the world, all round-pegged and turgid, and said, “Here’s your square hole”?

The post continues into a strangely wistful longing for a day when all men will be chemically castrated and we’ll finally be free of our round-pegged burdens. I guess this is supposed to be satire, since his usual political philosophy is second-rate technocratic libertarianism tempered by a deep regret of women’s suffrage. Thankfully, some smart writers accepted this churlish invitation:

I’d like to offer an opportunity to one of the writers at Salon, Huffington Post, Jezebel, Mediate, or Mediabistro. Allow me to interview you, by email, for this blog, on the topic of why you so vehemently disagree with your hallucination of my opinion. (Fair warning: It won’t work out well for you.)

Salon’s Mary Elizabeth Williams is one who took him up on it. The exchange is embarrassing to read, and not for the reason Adams hoped; there’s too much there to quote at length, but I want to call out one quote in particular:

My next question: Do you support the death penalty for rape, as I do, or are you relatively pro-rape compared to me?

Move over, Robert Stacy McCain. That’s the ugliest thing I’ve read in a long time.

June 30, 2011 at 3:37 pm

Posted in FYI

Tagged with , ,

Arrived in Portland

After a cramped four days of driving, Bethany and I arrived today in Portland! This morning we painstakingly navigated the Old Oregon Trail Highway, setting Lindsey up for the inevitable, perfect punchline.

We unpacked the car, and spent a good while gawking at the fact that we can see a mountain from our house.

Amazed by this and wondering what else the town has in store for us, we found a six-pack of Widmer Brothers X-114 for a jaw-dropping \$7. This proved easily as good as Bell’s \$16 per 6 Hop Slam.

Finally, we walked a couple of blocks to the Broadway Grill & Brewery, where the shoestring fries and beer sampler cannot be recommended highly enough.

More to come.

June 3, 2011 at 10:35 pm

Posted in Portland

Tagged with , ,

And then out of nowhere, a monad appears!

In this post, I walk through two typical Scheme programming challenges, and then show how they naturally give rise to a monad. Really, they’re not so scary. As Simon Peyton Jones said of designing Haskell:

Our biggest mistake: using the scary term “monad” rather than “warm fuzzy thing”.

Here’s the first part of the challenge: can you recreate the behavior of Scheme’s `begin` using only `lambda` and procedure application? Let’s start with a simple example:

```> (begin (printf "One\n") (printf "Two\n"))
One
Two
```

In this example, `begin` enforces the order in which the two `printf` expressions are evaluated. To get the same behavior just from `lambda` and application, we need to take advantage of the fact that Scheme is a call-by-value language. This is, the arguments to any function are always applied before the body of the function is evaluated.

So, we need to arrange our expression so that `(printf "One\n")` is an argument to a procedure that contains `(printf "Two\n")`:

```> ((lambda (_) (printf "Two\n")) (printf "One\n"))
One
Two
```

Success! Note that there’s nothing special about the underscore; it simply means that we do not care about the value of `(printf "One\n")`. We only care that it gets evaluated for its printing effect.

This would be nicer to read if the evaluation order of our statements read from left-to-right, as with `begin`. The only reason our example reads backwards is the order of procedure application: `(function argument)`. To get the order we want, we define a backwards procedure application:

```> (define mybegin
(lambda (x f)
(f x)))
> (mybegin (printf "One\n") (lambda (_) (printf "Two\n")))
One
Two
```

```> (mybegin (printf "One\n")
(lambda (_) (mybegin (printf "Two\n")
(lambda (_) (printf "Three\n")))))
One
Two
Three
```

Now for the second part of the challenge: recreate the behavior of Scheme’s `let` using the same toolbox of `lambda` and procedure application. Here’s our example:

```> (let ([x 5])
(+ x 3))
8
```

Nesting `let` in this way enforces the order of evaluation similarly to `begin`. In this example, `5` must be evaluated before `(+ x 3)`. So, we can start with the same basic structure as our `begin` example.

```((lambda (_) (+ x 3)) 5)
```

This isn’t quite right, though, since `let` does more than `begin`. Rather than throwing away the value of, say, `(printf "One\n")` by binding it to an unused underscore, we need to evaluate `5` and then bind it to `x`:

```> ((lambda (x) (+ x 3)) 5)
8
```

Let’s use the same trick we used for `mybegin` to make this nicer to read:

```> (define mylet
(lambda (x f)
(f x)))
> (mylet 5 (lambda (x) (+ x 3)))
8
```

It also works nicely with larger examples:

```> (mylet 5 (lambda (x) (mylet x (lambda (y) (+ x y)))))
10
```

Why, then, bother with two names for the same thing? After all, the definitions of `mybegin` and `mylet` are the same. Let’s call it what it is, which is `bind` (Haskell: `>>=`).

```> (define bind
(lambda (x f)
(f x)))
```

With a definition for `bind`, we nearly have a monad. We also need a function `return` in order to really say we have a monad. Loosely speaking, `return` is a function that brings a value into a monad’s world in the most trivial way possible. Our monad’s world is simply the world of Scheme values, so what could be more trivial than the identity function?

```> (define return
(lambda (a) a))
```

Here are our examples, happily living in the identity monad:

```> (bind (printf "One\n")
(lambda (_) (bind (printf "Two\n")
(lambda (_) (return (printf "Three\n"))))))
One
Two
Three
> (bind 5 (lambda (x) (return (+ x 3))))
8
> (bind 5 (lambda (x) (bind x (lambda (y) (return (+ x y))))))
10
```

The identity monad by itself isn’t terribly useful. After all, we already have `begin` and `let`! What we’ve done, though, is provide a hook into how we evaluate expressions in sequence. In “Real World Haskell”, Bryan O’Sullivan, Don Stewart, and John Goerzen describe monads as the “programmable semicolon”, and it’s easy to see why. We’ve taken the most basic notion of sequencing, “do this, then do that”, and encoded it with a handful of functions. The upshot is that more complex notions of sequencing are nearly as easy and follow the same structure, but that’s for a future post.

April 4, 2011 at 7:16 pm

Posted in Code

Tagged with , , ,

Jetpack, or: LaTeX for WordPress!

Automattic just released Jetpack, which allows features from wordpress.com to be used on self-hosted blogs like this one. The exciting part? $\LaTeX$ right there in a blog post! Once this semester lets go of my time, I’ll be sure to use it and make this space even nerdier.

March 9, 2011 at 5:59 pm

Posted in Code

Tagged with , ,