I have been somewhat silent for all kinds of boring reasons, but also quite so because I am terribly slow in grasping even basic category theory. (You don’t need to have any such knowledge to enjoy this post – just a bit of time because I guess this is going to be the longest blog post ever.) Still all the categorical pain was worth it, and here is why … The Expression Lemma captures a fundamental correspondence between Functional and OO Programming. In this blog post, let me try to explain the lemma in an easygoing manner. I will cut off all mentioning of the Expression Problem which constitutes arguably a motivation for this research. Let me focus on a very obvious and compelling motivation: the lemma provides a foundation for refactoring OO programs of a certain scheme to functional programs of a certain, associated scheme (and vice versa; in case, the latter is really found useful and not considered a criminal offense). BTW, the proof of the lemma will not be discussed below. Also, I should emphasize that only the simple expression lemma will be covered here. So let me refer to the paper for all such elaborations. Before I get started I want to acknowledge that I report about joined work with Ondrej Rypacek who is currently presenting our results at the Mathematics of Program Construction conference in Marseille. In fact, Ondrej deserves most if not all credit. Ondrej also blogged about the lemma some time back, and LTU had linked to the post.
Recursive operations on a recursive data structure
Consider a recursive data structure; let’s use the abstract syntax of a tiny expression language in the running example. For simplicity, let’s limit ourselves to two expression forms: numeric literals, and binary expressions for addition. Consider some recursive operations that are defined on the data structure. Let’s use “expression evaluation” and some sort of “expression transformation” in the running example. In Java, we can use an abstract class, Expr, to model the data structure with abstract methods, eval and modn, to model the operations. (We could also use interface polymorphism.)
public abstract class Expr {
public abstract int eval(); // Evaluate expressions
public abstract void modn(int n); // Transform modulo a constant
}
The two expression forms give rise to two subclasses that encapsulate data and operations.
public class Num extends Expr {
private int value; // State
public Num(int value) { this.value = value; } // Constructor
public int eval() { return value; }
public void modn(int n) { this.value = this.value % n; }
}
public class Add extends Expr {
private Expr left, right; // State
public Add(Expr left, Expr right) { // Constructor
this.left = left;
this.right = right;
}
public int eval() { return left.eval() + right.eval(); }
public void modn(int n) { left.modn(n); right.modn(n); }
}
Contrasting styles of decomposition
The OO style of decomposition can be contrasted with the functional style (or the style of constructive, algebraic specification, if you prefer). The data variants are defined independently of any operation; operations are defined separately as functions that case-discriminate on the data variants. In Haskell:
-- Expression forms
data Expr = Num Int | Add Expr Expr
-- Evaluate expressions
eval :: Expr -> Int
eval (Num i) = i
eval (Add l r) = eval l + eval r
-- Transform all literals modulo a constant
modn :: Expr -> Int -> Expr
modn (Num i) n = Num (i `mod` n)
modn (Add l r) n = Add (modn l n) (modn r n)
Semantic equivalence of OO and functional models
Now the 1 Million $ question is this: Are the two shown programs semantically equivalent, and, if so, how could one possibly prove the equivalence? The expression lemma will arise as an important tool in establishing that semantic equivalence. It is desirable to know of such equivalence because, for example, it would formally justify a refactoring from the OO style of decomposition to the functional one, and vice versa. Some might say that the semantic equivalence is reasonably obvious, but then again, how to formally establish this fact? Also, we are presumably looking for a general class of equivalent program couples (rather than the specific exemplars at hand), but at this stage, it is not obvious how this class would be characterized.
After 2-3 semesters of computer science, you may launch the following attempt.
Suppose:
· j refers to the above Java program
· h refers to the above Haskell program
· [| . |]Java assigns semantic meanings to (the relevant subset of) Java
· [| . |]Haskell assigns semantic meanings to (the relevant subset of) Haskell
Then our educated but inexperienced CS student could hope to be able to show that:
[| j |]Java ≡ [|h |]Haskell.
Or perhaps I just skipped too many classes and had too much wine over the years, and this could work. Anyway, I reckon that this approach would require “semantic voodoo” because the established semantic domains for the two abstraction mechanisms (i.e., classes vs. recursive functions on algebraic data types) are so radically different. In fact, the above equivalence claim does not make much sense, in its current form, because the I/O behaviors do not even match at the type level.
Matching up the input type
The functions of h take term-like data via an argument, while the objects of j readily encapsulate data (state) on which to invoke methods. We can match up the input type by building the objects of the OO program from the same representation that is fed into the functions. That is, expression objects would be constructed from expression terms. Let’s call this step recursive object construction, and designate a static method fromData in the class Expr. Now, if we assume that Java’s and Haskell’s integers can be compared, a “well-typed” proposition about the semantic equivalence of the eval method vs. the eval function can be stated as follows:
For all expression terms t:
Expr.fromData(t).eval()
= eval t
(Java goes left, Haskell goes right.)
We cannot cover modn in this manner, as will be clear shortly.
Matching up the output type by serialization
That is, the function modn returns public data – expression terms, while the method modn returns opaque data – expression objects. So how can we possibly compare the results returned by the function and the method? An apparently symmetric choice would be to introduce the presumable “inverse” of fromData; say an instance method toData which, in the case of Expr, extracts expression terms from expression objects. In fact, some of you may notice that such a couple fromData/toData would be possibly related to what’s called (de-) serialization in distributed programming or object persistency. So let’s try to match up the output type of methods and functions as follows: once a method has been performed such that a new object is returned (or an existing object is mutated), we would extract the state by serialization, hoping to use the data types of the functional program again for the representation of the externalized state, so that comparisons between functional and OO world make sense. If this all works, a “well-typed” proposition about the semantic equivalence of the modn method vs. the modn function could be stated as follows. (For simplicity of chaining, we assume that modn returns the result of the transformation; hence, it is no longer a void method – something that is, btw, for deep reasons, even more evil for a Smalltalk programmer than a Haskell programmer.)
For all expression terms t, for all n:
Expr.fromData(t).modn(n).toData()
= modn n t
(Again, Java goes left, Haskell goes right.)
Let’s scrutinize this use of de-/serialization. Here we note that serialization is “normally” meant to externalize an object’s state for the sake of being able to rematerialize (de-serialize) the object later or elsewhere. Not every object is serializable (in wild life). When an object ends up being serializable, then the serialization format is still effectively private to the corresponding object type, perhaps even to a specific implementation of the type – ask your local OO expert. Do we really want to define semantic equivalence with reference to serialization (or reflection and RTTI), i.e., systematically look into the objects at hand, and patently break encapsulation?
Matching up the output type by observation
I contend that semantic equivalence should instead be defined in reference to object interfaces and behavior (rather than “core dumps” extracted from the objects). So let’s try to limit the statement of equivalence to “observations” that are readily admitted by the OO interface. When these observations return “pure data”, e.g., integers, we can easily compare the results from the functional and OO world. For instance, the semantic equivalence of the modn function vs. the modn method could be approximated by using eval to perform observations. Thus:
For all integers n, for all expression terms t:
Expr.fromData(t).modn(n).eval()
= (eval . modn n) t
(Again, Java goes left, Haskell goes right.)
This option is in peace with encapsulation, and therefore is to be favored. However, the generality of the option is still to be established. In particular, we need to find a way to universally quantify over all possible observations, and to compare the observations with the results from the functional world. To be continued.
Functional object encoding
At this point, we are still struggling with two different host languages in our equations (c.f.: “Java goes left, Haskell goes right”). A formal model is in closer reach if we first eliminated one language. It’s hard to be fair every day. Let’s say goodbye to the OO language; let’s encode OO programs functionally (aka non-dysfunctionally), i.e., by using a functional object encoding. Not much is changed though: the encoding preserves the decomposition style of the OO program, and the use of objects including encapsulation. We use Haskell to encode the encoding. There are the following steps:
1. Declare an interface functor: this is a type constructor that defines the product of all method signatures for the interface of interest in terms of the state type of an object. The state type is abstracted as a type parameter; see x below. In the running example, the eval method returns an Int; the modn methods takes an Int and returns a transformed copy of “self” (aka “this”). Thus:
type IExprF x = (Int, Int -> x)
2. Declare the type of opaque objects: we take the recursive closure of the interface functor. In this manner, the state type is effectively hidden from the observable interface. For convenience’s sake, we also define projections that allow us to invoke the different methods on a capsule. Thus:
newtype IExpr = InIExpr { outIExpr :: IExprF IExpr }
callEval = fst . outIExpr
callModn = snd . outIExpr
3. Declare the type of interface implementations: This is just a trivial application of the interface functor. The idea is that an interface implementation observes the state and populates the type for the method signatures as prescribed by the interface functor. In the co-algebraic discipline of functional object encoding, the resulting type is called the co-algebra type for the functor at hand. Thus:
type IExprCoAlg x = x -> IExprF x
4. Provide interface implementations: Remember, the Java blueprint contains one concrete class for numeric literals, and another concrete class for binary expressions for addition. In the former case, the state type is Int; in the latter case, the state type is a pair of IExpr objects. These are the corresponding interface implementations:
numCoAlg :: IExprCoAlg Int
numCoAlg :: IExprCoAlg Int
numCoAlg = numEval /\ numModn
where
numEval = id
numModn = mod
… or in non-pointfree style:
numCoAlg :: IExprCoAlg Int
numCoAlg i = (numEval, numModn)
where
numEval = i
numModn n = i `mod` n
addCoAlg :: IExprCoAlg (IExpr, IExpr)
addCoAlg = addEval /\ addModn
where
addEval = uncurry (+) . (callEval <*> callEval)
addModn = uncurry (/\) . (callModn <*> callModn)
… or in non-pointfree style:
addCoAlg (l,r) = (addEval, addModn)
where
addEval = callEval l + callEval r
addModn n = (callModn l n, callModn r n)
5. Provide object constructors: The Java blueprint had constructors. More generally, any class needs a protocol for populating object state. In a functional object encoding, a constructor can be modeled as a function that takes the initial state of an object, and encapsulates it with the method implementations. To this end, the fundamental operation of unfolding comes to rescue; unfold “builds” (or “constructs”) values of a functor’s recursive closure (here: IExpr) from values of some other type (here: integers or subobjects):
newNum :: Int -> IExpr
newNum = unfoldIExpr numCoAlg
newAdd :: (IExpr, IExpr) -> IExpr
newAdd = unfoldIExpr addCoAlg
Conceptually, the unfold operation is defined generically for any functor: (i) apply the argument – a co-algebra (c.f. c below), (ii) map the unfold operation recursively over the positions of the functor’s type parameter (here: the occurrence of self’s type in the arguments and results of methods, c.f. fmapIExprF below), (iii) tie the recursive knot of the functor (c.f. InIExpr below). Thus:
unfoldIExpr :: IExprCoAlg x -> x -> IExpr
unfoldIExpr c = InIExpr . fmapIExprF (unfoldIExpr c) . c
The definition of the functorial map is induced by the structure of the functor at hand. The IExprF functor comprises one using occurrence of the type parameter in the second component of the pair, specifically in the result-type position of the function type (i.e., in the return-type of the signature of the modn method). The argument of the functorial map is applied to that occurrence:
fmapIExprF :: (x -> y) -> IExprF x -> IExprF y
fmapIExprF f (e,m) = (e, f . m)
This completes our transcription of the Java code to Haskell.
Reality check: computing 42 in different ways
As a simple illustration and clarification of the development so far, let us do some expression evaluation in different settings. In the OO setting, we construct objects by nested object construction on which we invoke the method for expression evaluation. Thus:
public class Demo {
public static void main(String[] args) {
Expr x = new Add(
new Num(39),
new Add(
new Num(1),
new Num(2)));
System.out.println(x.eval());
}
}
Likewise, in the setting of the original functional program, we construct a nested term to which we apply the function for expression evaluation. While visually similar, it is important to notice that term construction results in plain, public data whereas object construction results in objects that encapsulate private data and behavior.
main = do
let x = Add (Num 39) (Add (Num 1) (Num 2))
print $ eval x
Here is also a demo for the functionally encoded OO program:
main = do
let x = newAdd (newNum 39, newAdd (newNum 1, newNum 2))
print $ callEval x
All programs agree on the result of evaluation: 42.
Gory details of recursive object construction
We are now in the position to actually define fromData – as needed for matching up the input type of the two programs. Thanks to the functional object encoding it is now easier to see that it really makes sense to construct expression objects from expression trees. We exploit the fact that the recursive data structure of the functional program coincides with the recursive closure of the union of the OO state types. Here is the type of fromData:
fromData :: Expr -> IExpr
Our development relies on “Squiggol power” and the entire backlog of functorially parameterized morphisms. Hence, we must redefine the recursive data structure as the recursive closure of its non-recursive functorial shape. (Compare this with the non-recursive interface functor and the separate definition of its recursive closure.) Thus:
type ExprF x = Either Int (x,x)
newtype Expr = InExpr { outExpr :: ExprF Expr }
num = InExpr . Left -- serves as constructor
add = InExpr . Right -- serves as constructor
The type constructor ExprF captures the functorial shape of the expression forms. That is, it is a sum over Int (corresponding to the case of numeric literals) and (x,x) (corresponding to the case of binary addition) where x is ultimately to be instantiated to the recursive closure of the functor. That closure is taken by Expr. Indeed, the newly defined Expr is isomorphic to the algebraic data type Expr – as it was defined earlier. We can now combine the constructors for the two kinds of IExpr objects into a single function that dispatches on the functorial structure; here we apply ExprF to the opaque object type:
newEither :: ExprF IExpr -> IExpr
newEither = newNum \/ newAdd
… or more verbosely, by expansion of “\/”:
newEither :: ExprF IExpr -> IExpr
newEither (Left i) = newNum i
newEither (Right lr) = newAdd lr
It remains to apply newEither in a recursive manner. The fundamental operation of folding comes to rescue. A fold traverses over a recursive data structure while it is parameterized by a fold algebra, i.e., operations to apply to intermediate results as well as leafs. The “one-layer” constructor newEither serves as the fold algebra in our case. In different words, recursive object construction is defined as a fold over expression terms while the constructor newEither dispatches on expression forms and invokes data variant-specific constructors at each level:
fromData :: Expr -> IExpr
fromData = foldExpr newEither
Conceptually, the fold operation is defined generically for any functor: (i) reveal one layer of functorial shape from the recursive closure (c.f. outExpr below); (ii) map the fold operation recursively over the positions of the functor’s type parameter (here: over the positions for subobjects, c.f. fmapExprF below), (iii) combine intermediate results (or process leafs) by applying the fold algebra (c.f. a below). Thus:
type ExprAlg x = ExprF x -> x
foldExpr :: ExprAlg x -> Expr -> x
foldExpr a = a . fmapExprF (foldExpr a) . outExpr
The functor implies the following functorial map:
fmapExprF :: (x -> y) -> ExprF x -> ExprF y
fmapExprF f (Left i) = Left i
fmapExprF f (Right (x,x')) = Right (f x, f x')
Arriving at behavioral equivalence
We are still in need of a general method for comparing the results returned by the functions vs. the methods. We already alluded to the use of observations for that purpose. There is one trick we did not yet mention. That is, we can we construct objects (an ADT) from the functional program such that the functional program’s “public” data is encapsulated with the functions to be applied to that data. As a result, we will have objects on both sides of the equation, and hence, can perform observations on both sides, which makes it easier to set up a comparison. The ADT is constructed as follows:
newBoth :: Expr -> IExpr
newBoth = unfoldIExpr both
both :: IExprCoAlg Expr
both = eval /\ modn
… or more verbosely, by expansion of “/\”:
both :: IExprCoAlg Expr
both e = (eval e, modn e)
It’s time for a bold claim:
fromData = newBoth
That is, the objects obtained by recursive construction are equivalent to the objects obtained by the ADT construction. Let’s clarify the kind of equivalence at hand. Here we note that the terms on both sides of the equation are functions, and the equality sign is meant here as extensional equality, i.e., these functions always return the same result when applied to the same argument. Now, we also need to understand that the functions return objects which are in turn tuples of functions (methods). Further, each such method can be invoked again to return new objects (i.e., yet other tuples of functions). That is, method invocation can be arranged in arbitrarily long chains. Extensional equality of fromData and newBoth implies that all these possible chains also lead to observationally equivalent results. To summarize, the objects constructed by fromData and newBoth are indistinguishable by the observations (including chains of any length) admitted by the interface. This is really as much as we could hope for within the bounds of encapsulation. Hence, from here on, we replace the vague term of semantic equivalence by the more rigorous term of observational equivalence.
Making explicit more structure
We are not yet ready for a proof of the above claim. Intuitively, we need to get to a point where we can show that the functional program and the OO program are based on the same problem-specific ingredients (having to do with data variants for expressions and operations thereupon) which are only composed in different manners. At this point, the functional program is particularly monolithic: two functions written in the style of general recursion. Contrast this status with the functional object encoding of the OO program, where the co-algebra identifies all problem-specific ingredients in a structured manner. It is easy enough to achieve a similar degree of modularity for the eval and modn functions by defining them in terms of fold; it is “well-known” that these forms can actually be derived automatically:
eval :: Expr -> Int
eval = foldExpr evalAlg
evalAlg = evalNum \/ evalAdd
where
evalNum :: Int -> Int
evalNum = id
evalAdd :: (Int, Int) -> Int
evalAdd = uncurry (+)
modn :: Expr -> Int -> Expr
modn = foldExpr modnAlg
modnAlg = modnNum \/ modnAdd
where
modnNum :: Int -> Int -> Expr
modnNum = ((.) num . mod)
modnAdd :: (Int -> Expr, Int -> Expr) -> Int -> Expr
modnAdd = ((.) add . uncurry (/\))
Getting a sense for duality
The ingredients evalNum, evalAdd, modnNum and modnNum are really like the equations in the style of general recursion except that recursive components of the left-hand side are already replaced by the recursively computed results, and hence, the ingredients do not involve any recursive function applications of their own. (This is just a trivial and general consequence of committing to bananas.) The OO program is broken down into problem-specific ingredients quite similarly. Let’s compare. The functional program is structured as follows:
newBoth
= uI both
= uI (eval /\ modn)
= uI (fE (evalNum \/ evalAdd) /\ fE (modnNum \/ modnAdd))
Here, we abbreviate as follows:
- fE = foldExpr
- uI = unfoldIExpr
The OO program is structured as follows:
fromData
= fE newEither
= fE (newNum \/ newAdd)
= fE (uI (numEval /\ numModn) \/ uI (addEval /\ addModn))
In both cases, recursion is under the regime of the composition scheme. You don’t have to be a rocket scientist in category theory to smell the duality here. Subject to several conditions on the problem-specific ingredients, we may be able, eventually, to prove that both compositions are observationally equivalent.
Matching up problem-specific ingredients
Get a coffee first; this is going to be the hard part of the post.
Playing stupid, one could hope that:
evalNum = numEval
evalAdd = addEval
modnNum = numModn
modnAdd = addModn
Quite obviously, this is not the case. (Not even the types fit.) A more complex correspondence has to be established. Let us do some factoring. To this end, we observe again that the functional style of decomposition results in as many “disjunctions” as there are operations; each such disjunction is processed by a fold; these folds are then combined in a conjunction. Dually, the OO style of decomposition results in as many “conjunctions” as there are data variants; each such conjunction is processed by an unfold; these unfolds are then combined in a disjunction. Let us factor out the inner uses of fold and unfold so that the problem-specific ingredients are solely composed by “/\” and “\/”. For any functor F, the following “well-known” laws allow us to replace conjunctions of folds and disjunctions of unfolds by a single (co-) recursion:
The tupling law:
fF a /\ fF b = fF ((a . F fst) /\ (b . F snd))
The co-tupling law:
uF a \/ uF b = uF ((F Left . a) \/ (F Right . b))
(For the sake of a dense notation, we use a functor in an expression position to refer to the functorial map for that functor.) The tupling law happens to be the foundation of a powerful, optimizing transformation: if we wish to pair the results of two folds applied to the same argument (based on a split, c.f., “/\”), we can combine their fold algebras in one, and thereby do the work of both folds in one pass of recursion. That is, rather than pairing the final results of two folds, we perform pairing (and projection) at each level of recursion, and thereby suffice with one traversal. We do not care for optimization here, only for factoring. The co-tupling law is the dual of the first one. In OO terms, it tells us how to use a single interface implementation as a surrogate for two implementations of the same interface while taking the union of the state types. Regardless of any intuitions, the laws allow us to factor the functional vs. OO style of decomposition as follows:
Functional:
uI (fE fp)
where
fp = ((evalNum \/ evalAdd) . E fst)
/\ ((modnNum \/ modnAdd) . E snd)))
OO:
fE (uI oop)
where
oop = (I Left . (numEval /\ numModn))
\/ (I Right . (addEval /\ addModn))
Let’s distribute projections and injections so that we get conjunctions of disjunctions, or vice versa. Thus:
fp = (evalNum \/ (evalAdd . (fst <*> fst)))
/\ (modnNum \/ (modnAdd . (snd <*> snd)))
oop = (numEval /\ ((.) Left . numModn))
\/ (addEval /\ ((.) Right . addModn))
The roles of “\/” and “/\” are flipped in fp and oop. The “well-known” abide law can be used:
(f /\ g) \/ (h /\ i) = (f \/ h) /\ (g \/ i)
Let’s apply the abide law to oop:
oop = (numEval \/ addEval)
/\ (((.) Left . numModn) \/ ((.) Right . addModn))
Now let’s match up the operands of “\/” in fp and oop.
We highlight the differences in bold face.
evalNum
= id
vs.
numEval
= id
evalAdd . (fst <*> fst)
= uncurry (+) . (fst <*> fst)
vs.
addEval
= uncurry (+) . ((fst . outIExpr) <*> (fst . outIExpr))
modnNum
= (.) (InExpr . Left) . mod
vs.
(.) Left . numModn
= (.) Left . mod
modnAdd . (snd <*> snd)
= (.) (InExpr . Right) . uncurry (/\) . (snd <*> snd)
vs.
(.) Right . addModn
= (.) Right . uncurry (/\) . ((snd . outIExpr) <*> (snd . outIExpr))
The differences can be understood as follows. The functional program has an extra step of committing results to the recursive closure of the data functor; c.f. InExpr. The OO program has an extra step of retrieving arguments from the recursive closure of the interface functor; c.f. outIExpr. These are really just “leftovers” from the particular decomposition styles. A “common denominator” of fp and oop (referred to as lambda from here on) can be obtained by factoring out (left or right) the extra steps:
oop :: IExprCoAlg (ExprF IExpr)
oop = lambda . fmapExprF outIExpr
fp :: ExprAlg (IExprF Expr)
fp = fmapIExprF InExpr . lambda
lambda = ( a \/ b ) /\ ( c \/ d )
Where
a = id
b = uncurry (+) . (fst <*> fst)
c = (.) Left . mod
d = (.) Right . uncurry (/\) . (snd <*> snd)
Here is the executive summary of the steps:
- (1.a) Apply the tupling law to the separate folds of the functional program.
- (1.b) Apply the co-tupling law to the separate unfolds of the OO program.
- (2.a) Distribute projections into the disjunctions of the functional program.
- (2.b) Distribute injections into the conjunctions of the OO program.
- (3.) Apply the abide law to one of the intermediate results (say, to the OO program).
- (4.) Factor the programs to appeal to the following shapes:
oop = lambda1 . fmapExprF outIExpr
fp = fmapIExprF InExpr . lambda2
- (5.) Show (perhaps just “notice”) that lambda1 and lambda2 are equivalent.
Step (5.) may fail for one of two reasons:
- We are not clever enough.
- The lambdas are different.
The type of the common denominator
What would be the type of lambda? As a Haskell programmer, you get used to all kinds of advanced cheating – one is type inference. However, let’s fight like real men, and figure out the type ourselves because this might actually help with understanding the magic at hand. We start from the types of oop and fp:
oop :: IExprCoAlg (ExprF IExpr)
fp :: ExprAlg (IExprF Expr)
Let’s expand the type synonyms for (co-) algebras:
oop :: ExprF IExpr -> IExprF (ExprF IExpr)
fp :: ExprF (IExprF Expr) -> IExprF Expr
Let’s do step (4.) at the type level:
lambda1 :: ExprF (IExprF IExpr) -> IExprF (ExprF IExpr)
lambda2 :: ExprF (IExprF Expr) -> IExprF (ExprF Expr)
This does not leave much space for a type of the common denominator:
lambda :: ExprF (IExprF x) -> IExprF (ExprF x)
The two disagreeing positions of lambda1 and lambda2’s types (highlighted by bold face above) were generalized to the same type variable x. The type of any actual lambda must be at least as polymorphic as shown. We note that lambda‘s type is strictly more polymorphic than the explicit type signatures that we calculated for lambda1 and lambda2. If the factored definitions lambda1 and lambda2 (obtained by steps (1.)-(4.)) fail to type-check against the more polymorphic type, then our method fails to find observational equivalence. In categorical terms, the required polymorphism is what lambda makes a natural transformation, which is essentially a mapping from one functor to another. In fact, lambda is a special kind of natural transformation, i.e., a distributive law. That is, functors of source and target are actually compositions of two functors, and the composition is carried out in flipped order when comparing source and target; c.f. ExprF . IExprF vs. IExprF . ExprF.
Unnatural or non-dualizable programs
It’s pretty easy to end up outside the required polymorphism. There is actually a systematic way of discussing such causes of unnaturality. We simply look at the computed types of lambda1 and lambda2 and discuss all the differences one by one:
- (Compare the argument position of lambda1 and lambda.)
The OO program is not allowed to invoke method chains on the subobjects. The result of invoking a subobject (by a single method call) cannot be further observed. (This follows from the fact that the general type IExpr in oop (which is isomorphic to IExprF IExpr in lambda1) is restricted to IExprF x in lambda.) This limitation may come over as odd, and a generalized expression lemma is appreciated; see our lovely paper.
- (Compare the result position of lambda1 and lambda.)
The OO program is not allowed to arbitrarily construct and replace subobjects. A method implementation is bound (by the type) to use the objects returned by the observations of the subobjects to fill in the slots for the subobjects in the result. This is arguably not a bad limitation as it rules out OO programs that sort of arbitrarily rewrite the object graph. That is, the methods are enforced to be compositional in a certain way.
- (Compare the argument position of lambda2 and lambda.)
The functional program is not allowed to examine the precise expression structure of the intermediate results obtained by recursion. The less polymorphic type of lambda2 exposes the precise expression structure; the extra polymorphism of lambda hides the expression structure. Imposing such a ban on functional programmers resembles the notion of opaque data on the OO side, where one is not allowed to examine state (except when backdoors lack reflection and serialization are leveraged).
- (Compare the result position of lambda2 and lambda.)
The functional program is not allowed to construct deep terms while combining intermediate results obtained by recursion. The type of lambda only admits one layer of functorial shape in the result; it does not even allow leaving out that single layer of functorial shape. This limitation may come over as odd, and a generalized expression lemma is appreciated; again, see our lovely paper.
The Expression Lemma, finally
If we are able to match up the ingredients of a functional program and an OO program using the above steps (1.)-(5.), then the Expression Lemma promises observational equivalence for the different styles of composing the ingredients. The following version of the lemma glances over some technical details; please look at the paper, if you need to know more, and want to scrutinize the lemma or its proof. Given are two functors, T and I, think of T as the data functor (like ExprF in the example), think of I as the interface functor (like IExprF in the example). We assume generic definitions of fold and unfold for any functor. For clarity, we continue to attach the functor in question to any use of fold and unfold. Let’s stop using problem-specific recursive data types, and use the following generic type constructor for taking the recursive closure of any functor:
newtype Mu f = In { out :: f (Mu f) }
Then, for any lambda :: T (I x) -> I (T x), the following identity holds:
unfoldI (foldT ((I In) . lambda) = foldT (unfoldI (lambda . (T out))
(Read as: “Functional and OO programming is not too much different!”)
Towards refactoring
We can also use the developed machinery to refactor an OO program into a functional program (or vice versa). For instance, in the direction of OO to functional programming, we first factor the OO program according to the steps (1.)—(4.), if possible. Then we set lambda = lambda1 and lambda2 = lambda. Now, we attempt the steps (1.)—(4.) in inverse order so that the functional program is calculated. Likewise, the other direction can be accommodated. The refactoring fails if we hit a “case without counterpart”:
- The occurrence of the data functor in the result position of lambda seems to suggest that the implementation of any given operation for any given data variant can freely choose the data variant in the result of the operation. This is true for folds (read: constructor x can be rewritten to constructor y), but imposes a slight challenge on OO programming. That is, an OO method with “self’s” type in the result position of the interface functor must return an object of the same state type. The problem shows up when we attempted the inverse application of the co-tupling law (as part of deriving an OO program from a functional one), which may just fail when lambda was too liberal. We may overhaul the interface functor to use the recursive closure in place of “self”, but the expression lemma will no longer apply. Alternatively, we could stop refactoring before the application of the co-tupling law, but the resulting OO program would now designate one “class” to all data variants, which may count as failed decomposition.
- The occurrence of the interface functor in the argument position of lambda seems to suggest that the implementation of any given operation for any given data variant can freely refer to the results of applying any operations recursively on components of the data. This is true for functional objects (read as: method x can call method y), but imposes a slight challenge on functional programming. That is, if we start with the assumption that all functions should be separate folds, then they cannot cross-reference each other. However, if we start from (or stop at) a tupled fold, the problem goes away. The problem shows up when we attempted the inverse application of the tupling law (as part of deriving a functional program from an OO one). If we assume that programmers can use the notation of general recursion, it is fair to further assume that the translation into folds directly returns a tupled fold. Hence, we do not face any proper limitation here.
Wrap-up
I hope some of you actually managed to get to the end of this text. I also hope that the text helps with improving the understanding of the fundamental correspondence between functional and OO programming. Of course, there are many loose ends that need more work. For instance, how do we deal with hard-core non-functional objects (when mutation and aliasing cannot be ignored)? Also, what are the exact mechanics of a refactoring transformation? Further, how does the state of the art in fold mining relate to the needs of our method? Yet further, what other ideas for refactoring OO to functional programs must be critically integrated to make a contribution to real-world scenarios such as multi-core parallelization? Finally, I realize that despite this long text, the presentation is still somewhat dense for someone not trained in Squiggol power and Haskell magic; so I hope that Ondrej and me end up writing a comprehensive tutorial on the full subject some day.
Have a great summer!
Let me go back to the beach now that I have finished this quick post.
Ralf Lämmel
