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 idempotentThis 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 : '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.