A Correspondence Involving Getters and Setters
One of the reasons that I love Haskell is that it leads you to fascinating thought experiments. Here’s one of mine. The conclusions aren’t particularly earth-shattering, but they are interesting.
One of the most common things to do in an imperative programming language is to build getters and setters for the properties of an object. In Java, they may look like this:
public X getFoo();
public void setFoo(X val);
The obvious mapping from there into a purely functional approach gives you this, for a record type R and a field type F:
getFoo :: R -> F
setFoo :: F -> R -> R
The fact that we have two separate functions here is unpleasing to me, though. Without being quite able to explain why, I’d really like to have just one type that completely describes the property “foo”. A product type is definitely cheating… but this would definitely satisfy me, if it works:
foo :: forall t. (F -> (F,t)) -> (R -> (R,t))
I’m interested in this type for two reasons: first, because it’s fairly easy to embed both a getter and a setter together into such a type. Suppose you give me the functions getFoo and setFoo. Then I can certainly embed them into a foo, in such a way that they can be recovered.
foo g r = let (f,v) = g (getFoo r) in (setFoo f r, v)
getFoo’ = snd . foo (\x -> (x,x))
setFoo’ v = fst . foo (\x -> (v,()))
It’s a straight-forward matter of substitution to see that getFoo’ and setFoo’ are identical to their original counterparts. So one can construct a value of the form of foo given any getter and setter combination, and given any such value of the type of foo, one can extract a getter and a setter. The second reason I care about that type, though, is that has a natural meaning aside from just embedding a getter/setter pair. Recall that the State monad (with state type S, for example) is a newtype wrapper around (forall t. S -> (S,t)). So this can be seen as a state transformer. It takes a stateful transformation, and changes the type of the state.
Now, the rather more involved question is whether there exist state transformers (values of the type of foo) that do not arise in that way as the straightforward embedding of getter and setter functions. In other words, could foo be something more than just the encoding of a getter and a setter into a function?
Alas, the answer is yes. It would be nice if the product type of getters and setters were isomorphic to the type of state transformers, and that is very nearly true… but not quite. To see the reasoning work, first note that the type (a -> (b,c)) is isomorphic to (a -> b, a -> c). (This is the type isomorphism version of distributing an exponent over a product). This lets use split up foo into two parts as follows:
foo1 :: forall t. (F -> F) -> (F -> t) -> R -> R
foo2 :: forall t. (F -> F) -> (F -> t) -> R -> t
We can simplify a little by arguing based on the universal quantification. Note that foo1 is given as a parameter a function of type (F -> t), but it cannot possibly make any use of the value, since it does not know anything about the type t. Furthermore, foo2 must produce a value of type t, and can do so only through its parameter of type (F -> t), which can only be used for that purpose. So these turn out to be equivalent to the following simpler types:
modifyFoo :: (F -> F) -> R -> R
filteredGetFoo :: (F -> F) -> R -> F
I’ve named them suggestively, because I have a bit of intuition for what these things tend to mean. Let’s now look at what happens to the getFoo and setFoo functions that we were able to define from the original foo:
setFoo v = modifyFoo (const v)
getFoo = filteredGetFoo id
This all looks as you might expect… but remember that the question is whether modifyFoo and filteredGetFoo are completely determined by the getter / setter pair arising in that way. Clearly they are not. In particular, note that you can iterate a constant function 1 or more times, and always get the same answer no matter the number of iterations; and the identity function similarly for zero or more times. So some interesting logic can be built into modifyFoo or filteredGetFoo with respect to iterating the function passed as a parameter (a constant number of times, or maybe until some predicate holds, or perhaps something more complex), and though this would change the behavior of the modify and filteredGet operations for some inputs, it would have no effect on the get and put operations.
Still, we’ve got something interesting here. I wonder if there are interesting “non-standard” definitions of modify and filteredGet for some common record type. If so, then they would lead to interesting transformations on values of the State monad, which don’t arise from get and set in the normal way. Makes you wonder, doesn’t it?
Sententia cdsmithus 
The iterability has to do with the fact that you don’t actually have double negation elimination in intuitionistic logic. That is, the type T and the type (forall r. (T -> r) -> r) are not the same; the former can be weakened into the latter, but the latter cannot be strengthened into the former when T doesn’t happen to live in the classical fragment of intuitionistic logic.
So if you take a function argument (T -> T) you are free to apply it as many times as you like before returning. But if you take an argument (T -> r) where r is universally bound, then you can only apply it at most once before returning (meaningfully, that is; if you assume a lazy language and ignore seq when defining “meaningful” application, thereby prohibiting side effects) and must call it at least once if the return type is r.
You forget that even the finest imperative language in the world has not been able to eliminate _|_ from the language. Thus every function has an implicit forall r. r -> prepended to its type; in your case, this only matters for getFoo; its type is actually F -> R -> F.
Thus I’d claim that the actual type of foo is just the State type: F -> R -> (F, R)
I’m not sure exactly what you mean here. Certainly what I’ve written above works with the types I’ve given. If you think a different type is needed, perhaps you can explain how?
Mathnerd:
The problem with that version is that it requires you to supply a _|_ in order to use it as an accessor. The partiality of that approach is somewhat galling, it is used by Henning’s otherwise rather nice Data.Accessor package.
Personally, I find the costate/store coalgebra approach advocated by Russell O’Connor to be more appropriate. A function of the form a -> (b, b -> a) — or equivalently a -> Store b a, subject to the side condition that it forms a comonad coalgebra captures the relationship of get to put.
Another benefit of merging the a -> b, and a -> b -> a functions into one function a -> (b, b -> a) is that they can be composed more efficiently. The result of the function basically provides everything you need to ‘zip back up’ your a with a new b inside, while the two function version has to descend into the structure a second time.
Efficiency aside, both your version and the version stated here miss the get/put laws that such a transformer should satisfy.
You can extract such a State b r -> State a r from such a lens:
http://hackage.haskell.org/packages/archive/comonad-transformers/1.5.2.6/doc/html/Data-Lens-Lazy.html#v:focus
but it strikes me that the use of a lens to transform state is an incidental capacity of a lens, and not its defining property, which seem better expressed in terms of how the primitive operations on a lens interact:
put l (get l a) a = a
stating that the result of putting the value you received from a lens back into the whole is the same as the original
put l b1 (put l b2 a) = put l b1 a
stating that putting is idempotent
get l (put l b a) = b
stating that you get what you put in.
But as Russell noted, and Jeremy Gibbons recently posted
those 3 laws can be replaced with the statement that you want any lens to be a costate coalgebra, which is to say that for a lens f:
extract . f = id
duplicate . f = fmap f . f
On the other hand, the approach here uses a monad homomorphism between two state monads, which isn’t sufficient to capture the side conditions.
Edward Kmett: I’ll agree that lenses could be much nicer. But in Java, State s a is what you’ve got: http://java.sun.com/docs/books/jls/third_edition/html/typesValues.html#4.12.5
How would you use lenses from an imperative viewpoint?
BTW, what happened to category-extras?
Mathnerd: it has been split into about 20 packages. I started working with Brent Yorgey to document the broken out version of things.
As for State ‘being what you have’, yes, you can use a lens to transform onestate monad into another by focusing on part of the state, and that is an important operation to offer via a lens, but that isn’t the most efficient representation, and doesn’t capture the side conditions you want a lens to satisfy.
As for how I use lenses from an imperative standpoint, I have code in scala at work where I’ve replaced imperative methods with lenses focusing on part of the state. Then I just pass a lens to some portion of my state to my object.
Consider the following tuple type describing a bump counter and a map of distinct values to numeric keys.
case class Indexee[K](counter: Int, content: Map[K, Int])
We can build lenses out of getter/setter pairs.
object Indexee {
def counter[K]: Lens[Indexee[K], Int] = Lens ( _.counter, (x,y) => x copy (counter = y))
def content[K]: Lens[Indexee[K], Map[K, Int]] = Lens (_.content, (x,y) => x copy (content = y))
}
Then pass that around
class Memo[S, K](
indexee: Lens[S, Indexee[K]],
…
) {
// composing it with other lenses
val counter: Lens[S, Int] = Indexee.counter compose indexee
// and use it, seemingly, imperatively
def fresh: State[S, Int] = counter += 1
…
}
The lenses used above are the ones I wrote for scalaz
https://github.com/scalaz/scalaz/blob/master/core/src/main/scala/scalaz/Lens.scala
which are based on the separate getter/setter model.