Skip to main content

Some classes of effectful programs

I'm going to do something unusual for this blog and talk about functional programming for a bit.

Jessica Kerr wrote a blog post about the concept of idempotence as it's used in math and programming, and I decided I wanted to lay the ideas out in more familiar terms to me.

So, consider a pure mini-ML with functions, products, numbers, lists, polymorphism, and let-binding, but no references (or other effects -- for the duration of this post I'm going to limit my notion of "effect" to references into a store). This is Language 1 (L1). Now consider adding references and sequencing to this language (i.e. new expressions are ref v, r := v, !r, and (e; e)). This is Language 2 (L2).

The operational semantics of Language 2 includes a store mapping references to values, for which I'll use the metavariable S. In addition to giving types T -> T' to L2 functions, we can give them store specifications S -o S' (using the linear implication symbol -o suggestively but not especially formally) to suggest how they might modify it; e.g. a function f(r) = r := 3 has store spec (arg L * (L |-> V) -o (L |-> 3)) (saying that if the location L referred to by the argument had value V before the function was called, it has value 3 after the function is called).

Here are some classes of Language 2 programs:

1. Effectless. 

This is the subset of Language 2 programs that are also Language 1 programs.

f : 'a -> 'b 
meeting spec S -o S (keeps the store the same)
e.g.: f(x) = x

This is sometimes called "referentially transparent".

2. Observably effectless.

f : 'a -> 'b
meeting spec S -o S' (might change the store)
where f(x) = (f(x); f(x))

but always returns the same output for the same input.

let r = ref nil in 
f(x) = (r := (x::!r); x) 

The function might have some internal effect, but the caller can't observe that based on the returned values. I'd argue this might be a more useful class for the term "referentially transparent", since "effectless" is a much better term for class 1, but honestly I don't find the former term informative at all and would rather do away with it.

3. Effectively idempotent.

f : 'a -> unit
meeting spec S -o S'
where f(x) ~ (f(x); f(x))

...where ~ is a notion of equivalence on the store; i.e., if we were write the store explicitly and label its state transitions with function calls:

S --f(x)--o S' --f(x)--o ... --f(x)--o S'

Calling f(x) once can change the store, but calling it an arbitrary number of subsequent times won't induce subsequent changes.

In this case, we don't care about the return value (made it of unit type to emphasize this point), but rather the effects of calling the function. The example I gave for "observably effectless" is not effectively idempotent.

I believe this is the concept that programmers who work across multiple APIs care about when they talk about "idempotence" -- the side-effects of such functions might be sending an email or posting to a user's timeline, which is definitely an effect on the world, but probably not one that you want to repeat for every impatient click on a "submit" button.

4. Mathematically idempotent

This is a property that doesn't have anything to do with effects -- we can talk about it for L1 programs or L2 programs, it doesn't matter. We don't care whether or not it has an effect on the store.

f : 'a -> 'b
f(x) = f(f(x))
e.g.: f(x) = 3

What class 4 has to do with class 3

We can compile L2 programs to L1 programs by reifying the store and location set in L2's semantics as a value in L1 (anything that can represent a mapping from locations to values). 

If we're interested in the class 3 functions of L2, we just need to consider programs of the form

(f(x); f(x))
f : 'a -> unit.

If st is our distinguished store type,
f becomes f' : 'a * st -> st
and (f(x); f(x)) in a store reified as s becomes
f' (x, f'(x, s))

Now the property defining class 3 can be translated as:
f(x, s) = f(x, f(x, s))

...which looks, modulo the extra argument, just like the definition in class 4.


  1. Hmm. A lot of the idea of "mapping out the effects of state" seems strikingly similar to the work that Lindsey is doing. I confess that I have not read her papers yet (I heard of her work somewhat later than when her papers were in the introductory phase, which then resulted in me feeling hopelessly lost trying to understand it...), but your modeling of state transitions as linear implication makes me want to go back and reread that.

    Beyond that, interesting reading. Thanks for the insights!

    (Sigh. I can't comment as my livejournal self, because BlogSpot can't handle my account name having an underscore. Ugh.)

    1. Have you found the blog posts to be any more approachable than the papers? I recommend this one, followed by this one!

    2. This comment has been removed by the author.

  2. Thanks for this post, Chris! I understand the punchline about what class 4 has to do with class 3, but I was confused by some of your notation. In your first example, you write `f(x) = x`. At first I thought that this was supposed to be a single effectless program (the identity function), but now I think that `=` is a meta-level thing and you're instead saying that `f(x)` and `x` are equal in the sense that a store `S` after `f(x)` is evaluated will be the same as store `S` is after `x` is evaluated. Is that right? If so, that definition is interesting because it allows for the possibility that the evaluation of `x` may perform effects, and so calling `f(x)` (which presumably would involve the evaluation of `x`) might too, but at least they are the same effects we'd get from merely evaluating `x`. But you have all this under the heading of "effectless programs", so am I misreading this?

    1. Oooh, that was maybe a bad notational choice on my part -- I was writing code in monospace font, which included some monospace "="s for function definition, and I was writing metalevel equations, in which bits of code were being related to other bits of code by /non/-monospace "=".

      For the specific example you mentioned, I did mean it to be the identity function, but also maybe should have made the point that "f(x) META-EQUALS x" no matter how many times we've called f(x) previously, which is what the term "referentially transparent" seems to emphasize. i didn't mean to suggest anything about the effects of evaluating the argument to the function in this case, though that's also an interesting line of inquiry.

    2. Oh, you _did_ mean `f(x) = x` to be the identity function. OK, I was confused because in the example following, you have `f(x) = (f(x); f(x))`, which looks like a meta-level equation.

    3. right - that one is non-monospace =


Post a Comment

Popular posts from this blog

Using Twine for Games Research (Part II)

This preliminary discussion introduced my thoughts on using Twine as a tool for creating prototypes for games research. I'll start with documenting my first case study: a hack-and-slash RPG-like setting where the player character has a record of attributes ("stats") that evolve through actions that turn certain resources (money, health, items) into others. I've selected this hack-and-slash example because it falls outside the canonical "branching story" domain thought to be Twine's primary use case, but it is not too much trickier to implement. It relies crucially on the management of state in ways that simple branching stories would not, but it does so in a fairly straightforward way.

If all goes well, this post may also serve as a tutorial on the "basics" of Twine (links + variables + expressions). In particular, I'll be using Twine 2/Harlowe, and I haven't seen many tutorials for this new version published yet.

To me, the main "…

Why I don't like the term "AI"

Content note: I replicate some ableist language in this post for the sake of calling it out as ableist.

In games research, some people take pains to distinguish artificial intelligence from computational intelligence (Wikipedia summary), with the primary issue being that AI cares more about replicating human behavior, while CI is "human-behavior-inspired" approaches to solving concrete problems. I don't strongly identify with one of these sub-areas more than the other; the extent to which I hold an opinion is mainly that I find the distinction a bit silly, given that the practical effects seem mainly to be that there are two conferences (CIG and AIIDE) that attract the same people, and a journal (TCIAIG - Transactions on Computational Intelligence and Artificial Intelligence in Games) that seems to resolve the problem by replacing instances of "AI" with "CI/AI."

I have a vague, un-citeable memory of hearing another argument from people who dislike the…

Using Twine for Games Research (Part III)

Where we last left off, I described Twine's basic capabilities and illustrated how to use them in Twine 2 by way of a tiny hack-and-slash RPG mechanic. You can play the result, and you should also be able to download that HTML file and use Twine 2's "import file" mechanism to load the editable source code/passage layout.

Notice that, in terms of game design, it's not much more sophisticated than a slot machine: the only interesting decision we've incorporated is for the player to determine when to stop pushing her luck with repeated adventures and go home with the current spoils.

What makes this type of RPG strategy more interesting to me is the sorts of decisions that can have longer-term effects, the ones where you spend an accumulation of resources on one of several things that might have a substantial payoff down the road. In a more character-based setting, this could be something like increasing skill levels or adding personality traits.

Often, the game-…