Adam Foltzer's Blog

Moving to Portland and joining Galois

leave a 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)!

Written by Adam Foltzer

February 10, 2012 at 7:08 pm

Posted in FYI, Portland

Call-by-need git learning: git ready

leave a comment »

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.

Written by Adam Foltzer

September 15, 2011 at 2:01 pm

Posted in Code, FYI

Tagged with

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

leave a comment »

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:

Combining Denotational and Operational Semantics for Scalable Proof Development from Galois Video on Vimeo.

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

Written by Adam Foltzer

August 10, 2011 at 1:25 pm

Never Read Dilbert

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.

Written by Adam Foltzer

June 30, 2011 at 3:37 pm

Posted in FYI

Tagged with , ,

Arrived in Portland

leave a comment »

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.

Mount Hood from our porch

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.

Beer sampler

More to come.

Written by Adam Foltzer

June 3, 2011 at 10:35 pm

Posted in Portland

Tagged with , ,

And then out of nowhere, a monad appears!

with 3 comments

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

This reads a lot better. How about adding a third expression?

> (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.

Written by Adam Foltzer

April 4, 2011 at 7:16 pm

Posted in Code

Tagged with , , ,

Jetpack, or: LaTeX for WordPress!

with 2 comments

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.

Written by Adam Foltzer

March 9, 2011 at 5:59 pm

Posted in Code

Tagged with , ,

Opt out of creepy behavioral advertising

leave a comment »

You know those ads for sites you’ve visited that show up in the most unexpected places? Opt out at this page from the Network Advertising Initiative.

Written by Adam Foltzer

February 13, 2011 at 9:54 pm

Posted in Privacy

Tagged with , ,

We’re doomed! (IPv4 edition)

leave a comment »

Via Ars Technica, River of IPv4 addresses officially runs dry:

In a ceremony in Miami this morning, the final five blocks of IPv4 addresses were given out to the five Regional Internet Registries that further distribute IP addresses to the far corners of the planet. The five RIRs still have tens of millions of addresses as working inventory, but once those addresses are given out, it’s over. Internet Protocol addresses are a prerequisite for all Internet communication—both the sender and the receiver need one. As such, additional addresses are necessary whenever new users are connected to the Internet.

It won’t quite be a scene from a disaster flick, though. There are technologies in the wings to stretch the current supply of addresses a lot further. However, a lot of them involve multiple end users sharing a single address.

For most purposes, this will be okay. After all, your home router shares your address among all your devices using NAT. Many two-way communications such as videoconferencing and file transfer, though, require a direct path between both devices. Techniques such as Internet Gateway Device Protocol help applications automatically configure routers to avoid problems, but I’m not sure this will hold up once the NAT gateways are in ISPs rather than our homes.

Hopefully, there will be enough commercial pressure soon to truly roll out IPv6 as the solution. After all, it brings us anecdotes like this gem from the Ars comment thread:

Think of it like this. If the ENTIRE IPv4 address space was 1.6 square inches… how big are you envisioning the IPv6 space to be? As big as a desk? No. How about a room? lol. Okay, a house? Not even close. A FOOT BALL STADIUM! Not even gotten started yet. Okay, lets do a crazily large jump, as big as ASIA! You’ve got a long way to go. The entire earth? Hey, finally you’re a spec on the map!

So how big would IPv6 be? It would be _the size of the solar system_! The FREAKING SOLAR SYSTEM vs a 1.6 sq in! IPv6 is absurdly large. Humanity could scale up to a galactic civilization before IPv6 would even be a concern (by that point, IP would likely need to be redesigned anyways to deal with the vastly different requirements).

Written by Adam Foltzer

February 3, 2011 at 9:19 pm

Posted in Gadgets

Tagged with , , , , , ,

HTML5 to lose the 5

leave a comment »

This move reflects how these standards are actually used:

In a blog entry Thursday, HTML specification editor Ian Hickson announced that the HTML specification will no longer have a version number attached. The WHATWG version of the specification will be treated as a “living standard” that will evolve organically as additions are integrated, sort of like a rolling release model.

I’m a big fan of things like <audio> and <canvas>, but it’s been frustrating to deal with inconsistencies in browser support. Setting a clear marker at version 5 was supposed to make this less of a problem, as “HTML5 support” would be a clear marker of a modern browser. Unfortunately, browser vendors decided that phrase means “supports some things from HTML5 and also some new markup we invented that’s probably better.” This decision is just a concession to that reality.

Written by Adam Foltzer

January 21, 2011 at 11:42 am

Posted in Code

Tagged with , , ,