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.

e.g.:
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))
for
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.

Comments

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

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

      Delete
    2. This comment has been removed by the author.

      Delete
  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?

    ReplyDelete
    Replies
    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.

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

      Delete
    3. right - that one is non-monospace =

      Delete

Post a Comment

Popular posts from this blog

Reading academic papers while having ADHD

Using Twine for Games Research (Part II)

Using Twine for Games Research (Part III)