My friend Juan Paucar directed me to a paper from the magnificent Programming Languages and Systems 28th European Symposium on Programming, ESOP 2019, related to Codata. I have been very interested in codata, mainly because it relates to data in a category-theory way, but, as usual, I didn't understand many of the words involved. This paper helped me understand a lot, and also helped me understand and shape my mind on how to connect the worlds of FP and OOP. But, before that, we must go on tour over a bit of theory.
Data
Data, better understood as Haskell's data
declaration, is nothing more than a type and a bunch of ways (functions) to create values of that type. I'm going to use the GADT syntax just because it makes the functions visible. Here is an example:
data Foo where
Foo1 :: Int -> String -> Foo
Foo2 :: Bool -> Foo
For the folks that don't grasp GADTs yet, the above is equivalent to:
data Foo
= Foo1 Int String
| Foo2 Bool
But with the GADT syntax we can see the functions. Foo1
is a constructor, but also a function. Foo1
receives an Int and a String, and constructs a value of type Foo
. Exactly the same happens with Foo2
.
We just talked about constructors: a constructor is nothing more than a function that manufactures a value out of other values. But that pretty much defines every function as a constructor, which isn't helpful. We'll go a bit further: a constructor is a "primitive" function that makes a value of type T, and is not build out of other functions that make a value of type T. Also, a constructor is the function you define when you write a data
declaration.
If there are constructors, there should be something that dismantles data, because data seems to be constructed by aggregating values. This thing that deconstructs data is called "eliminators". The universal eliminator in Haskell is the case
statement:
case myfoo of
Foo1 i s -> ...
Foo2 b -> ...
The case
statement accepts a parameter (what you put between the case
and the of
) and returns a value of some type. That's why all the branches in a case
statement must have the same type, because when you write a case
statement, you are writing a function like mycase :: Foo -> X
, but with a nicer syntax.
This means eliminators are not always in the shape of case
statements. In reality, eliminators are just functions, and Haskell provides special syntax for these functions to be written in a better way. But, if we go to Lisp, for example, we also have constructors and eliminators.
In Lisp you can manufacture a list with a new head by using the constructor cons
(this is why these data structure is called a cons-cell
). cons
is just another function with two parameters: the head and the tail of the list to be constructed, and returns the list. To destructure a cons-list, you have two eliminators: car
and cdr
. car
takes a list and returns the head, cdr
takes the list and returns the tail.
Haskell also offers eliminators, but everyone frowns at you if you use them too much: when you declare a record datatype, Haskell helpfully creates functions to access each of the fields:
data FooRecord = FooRecord {
fooField1 :: Int,
fooField2 :: String
}
-- Both
-- fooField1 :: FooRecord -> Int
-- fooField2 :: FooRecord -> String
-- now exist
Everyone frowns at you when you use these accessors because if FooRecord
has more than a single constructor, and you use an eliminator for the other constructor, your program blows up in flames. This is no different to how car
and cdr
blow up in flames when you pass as parameter an empty list.
The point of all of this is that data
is a declaration that offers a bunch of different ways to create a value, and your program chooses which one interests you for the current case.
Category Theory
Category Theory is a branch of Mathematics mainly used by haskellers to annoy everyone else. But, believe it or not, it's also useful to reason about programs. In Category Theory we have objects and we have arrows that interconnect the objects. For something to be a Category, its objects and arrows have to obey some rules.
One of the constructs of Category Theory is the co-category. A co-category is a category where the arrows have been reversed. If in category X, an arrow goes from A to B, in the category co-X, the arrow goes from B to A.
At this point, "codata" should be suspicious to you. It totally looks like "co-data", the co-category of "data". But, how does it actually look the category of "data"?
The Category of data
The "data" category is revealed to us as the data
declaration. Let's have another look at the Foo
example:
data Foo where
Foo1 :: Int -> String -> Foo
Foo2 :: Bool -> Foo
In this case (but not in all categories) the types are the objects and the functions are the arrows. If we massage a little bit the code above, by using uncurrying, we can get to a data format that is a bit less arrow-ish and easier for our purposes:
data Foo where
Foo1 :: (Int, String) -> Foo
Foo2 :: Bool -> Foo
Now Foo1
takes a pair of Int and String and returns a Foo
, and Foo2
takes a Bool
and returns a Foo
. This is pretty much what every haskeller already knows: you don't have a Foo
via Foo1
until you provide both the Int
and the String
, no matter how many arrows are in the middle.
And now, the case statement:
case myfoo of
Foo1 (i, s) -> what_to_do_if_Foo1 i s
Foo2 b -> what_to_do_if_Foo2 b
Let's massage it a little bit to turn it into a function:
fooEliminator :: (Foo, ((Int, String) -> a), (Bool -> a)) -> a
fooEliminator (myfoo, what_to_do_if_Foo1, what_to_do_if_Foo2) =
case myfoo of
Foo1 (i, s) -> what_to_do_if_Foo1 (i, s)
Foo2 b -> what_to_do_if_Foo2 b
Now that we have converted case
into a plain old function, we don't need to do hand-waiving and magic because everything is now plain old function composition and application. Also, all the uncurrying that all the haskellers are about to complain is just going to help us.
The co-Category of data: co-data
I massaged all these expressions and uncurried them because, otherwise it is confusing. I mean, a co-category is a category with the arrows flipped. Which poses the question: which arrows? All of them? Some of them? Everything is easier if there is a single arrow: it means we don't have to go figuring out which one.
So let's flip the arrow of the Foo
data declaration, and let's see what comes out.
-- This is not real Haskell, `codata` doesn't exist (yet) in Haskell
codata Foo where
Foo1 :: (Int, String) <- Foo
Foo2 :: Bool <- Foo
I happily renamed data
to codata
, and flipped the single arrow in each line. Let's massage it a little bit more by flipping the order of the arguments so that the arrow points to the right, because we are accustomed to see the arrow functions that way:
codata Foo where
Foo1 :: Foo -> (Int, String)
Foo2 :: Foo -> Bool
What does this mean? Well, a lot of things at the same time, but let's go one by one.
We have two functions related to the codata Foo
. The first, called Foo1
takes a Foo
and manufactures a pair of Int and String. The second, called Foo2
takes a Foo
and manufactures a Bool
. We have two functions that take what seems to be a composite value Foo
and extract simple values from it of types Int
, String
and Bool
.
The same way that we could call any of the two functions in the data Foo
declaration, we can call any of the two functions in the codata Foo
, and get an (Int, String)
for the first case, and a Bool
for the second. Nothing forces us to call both, and we can just call any one of them.
If we have a Foo
, and by calling Foo1
we get simple values from it, this looks a lot like a eliminator. But we can also call Foo2
, which looks like another eliminator.
Trying to make sense of all of this, we reach a deep insight:
data
is about how we can call any of the many different constructors of a composite value.codata
is about how we can call any of the many different eliminators of a composite value.
From it, we can derive further insights:
- Codata looks a lot like objects and methods, where the codata value is the object, and the eliminators are the methods. There is probably some theorem out there that maps codata as a category to objects in OO programs.
- It's not that Functional Programming is superior to Object Oriented Programming. But, the usual Functional Programmer has been an Object Oriented Programmer before. Because of this, he is likely to know
codata
from OO, and now is starting to understanddata
from FP. As a result of this, he is better armed than an Object Oriented Programmer because an Object Oriented Programmer only knowscodata
.
Further philosophical details can be extracted from the duality data-codata:
- If we were to find a pure FP programmer, and a pure OO programmer, they would probably have a similar level of skill, but in totally different dimensions. This would make very hard to actually figure out who is the most skilled, because their skill-sets wouldn't be comparable! How do you compare skill-set in
data
with skill-set incodata
? - Data (and Functional Programming) deals on how we can construct complex datatypes from simple ones by using constructors. Codata (and Object Oriented Programming) deals on how we can extract the components from an object by calling its methods.
-
The Expression Problem states that you should be able to add new cases and new functions to a datatype without losing type safety and without having to recompile.
- In an OO language, you can add a new case by creating another subclass and implementing the methods. But, if you want to add a new function to a datatype, you have to add it to the superclass and implement it on all the existing subclasses, which means modifying a lot of files and recompiling most of the program.
- In a FP language you can add a new function to an existing datatype just by adding a function. But, if you want to add a new case, you have to add the constructor and modify all the functions that use the datatype, which means modifying a lot of files and recompiling most of the program.
Turns out, with our new data-codata knowledge, that we have a deeper insight into the Expression Problem, and why most solutions feel half-assed. Typeclasses in Haskell feel like "OO bolted in", the same way that C# extension methods feel like "functions bolted in". In a world where data is king, codata stuff feels bolted in; the same way than in a world where codata is king, data stuff feels bolted in. The categories are opposite, and that means the underlying math is fighting with what we want to add. Without cooperation from the math side, the best we can hope is getting a half-assed result.
Conversions
All this theory would be useless (as well as the paper) if we couldn't do something with it. Turns out the paper shows something very interesting: a way to implement data
in the codata
world, and a way to implement codata
in the data
world. This is something great, as it means we may have programming languages in the future that support both data
and codata
!
Codata in data: implementing objects in Functional Programming
The first conversion that we can implement is creating Objects in Functional Programming. Haskell already shines a way to implement them: typeclasses. When you read about typeclasses, the literature starts throwing around dictionary of functions passed implicitly. This shines a way to implement objects: as a product of the eliminators (methods) of the object. Thus:
class Foo {
int fooInt;
String fooString;
public Foo(int x, String y) {
fooInt = x;
fooString = y;
}
public int getTheInt() {
return fooInt;
}
public String doSomething(String extra) {
return fooString
.concat(fooInt.toString())
.concat(extra);
}
}
Becomes:
data Foo = Foo {
getTheInt :: Int,
doSomething :: String -> String
}
-- constructor
mkFoo :: Int -> String -> Foo
mkFoo fooInt fooString = Foo {
getTheInt = fooInt,
doSomething = \extra -> fooString <> show fooInt <> extra
}
And now we can do some OOP:
let myFoo = mkFoo 3 5 in
doSomething myFoo "blah" -- this is like myFoo.doSomething("blah")
All the OO folks will complain if this doesn't work with inheritance, and they are right, because otherwise this fails to do its part on the Expression problem. So let's extend both examples:
class ModifiedFoo extends Foo {
bool mfooBool;
public ModifiedFoo(int x, String y, bool z) {
super(x, y);
mfooBool = z;
}
public String doSomething(String extra) {
if(mfooBool) {
return "Nope";
} else {
return super.doSomething(extra);
}
}
}
And now in Haskell:
mkModifiedFoo :: Int -> String -> Bool -> Foo
mkModifiedFoo fooInt fooString mfooBool = Foo {
getTheInt = getTheInt super,
doSomething = \extra -> if mfooBool
then "Nope"
else doSomething super extra
}
where
super = mkFoo fooInt fooString
The Haskell approach stores attributes in a closure, instead of declaring them. I could create a specific object to store them, but I consider the closures good enough.
Curiously, the translation between the two is mostly mechanical, which is what the authors of the paper use to mechanically convert one into the other.
Data in codata: implementing Algebraic Data Types in Object Oriented Languages
Curiously, implementing ADTs in OOP languages is something that goes with many names, but seems to be hideous, at least initially. It has a very fancy name: Church Encoding, and a less fancy name: the Visitor Pattern, but they are pretty much the same thing. This technique is based on converting the case
statement into an object, and the different constructors into instances of an Acceptor
class. Let's see an example:
data Foo where
Foo1 :: (Int, String) -> Foo
Foo2 :: Bool -> Foo
fooEliminator :: (Foo, ((Int, String) -> a), (Bool -> a)) -> a
fooEliminator (myfoo, what_to_do_if_Foo1, what_to_do_if_Foo2) =
case myfoo of
Foo1 (i, s) -> what_to_do_if_Foo1 (i, s)
Foo2 b -> what_to_do_if_Foo2 b
In Java, the datatype declaration becomes:
abstract class Foo {
public A eliminate(FooEliminator<A> fooEliminator);
}
// Class to represent Foo1
final class Foo1 extends Foo {
int i;
String s;
public A eliminate(FooEliminator<A> fooEliminator) {
return fooEliminator.what_to_do_if_Foo1(i, s);
}
}
// Class to represent Foo2
final class Foo2 extends Foo {
bool b;
public A eliminate(FooEliminator<A> fooEliminator) {
return fooEliminator.what_to_do_if_Foo2(b);
}
}
abstract class FooEliminator<A> {
public A what_to_do_if_Foo1(int i, String s);
public A what_to_do_if_Foo2(bool b);
}
In the Haskell example, the what_to_do_if_FooX
were two functions that we need to pass in together, as they become parts of the same case
statement. In the Java version we decide to pass them together as an instance of FooEliminator
, thus going together because they are methods of the same object.
Adding new operations to Foo
, as the Expression Problem demands, is quite easy in both implementations. In Haskell we just call fooEliminator
with different parameters:
fooEliminator myFoo (\(i, s) -> something_different_1 i s) (\b -> something_different_2 b)
For the Java implementation is also easy. We derive a new type of FooEliminator
, and we call Foo.eliminate
with it:
class SomethingDifferentFooEliminator extends FooEliminator<String> {
public String what_to_do_if_Foo1(int i, String s) {
return "something different".concat(i.toString()).concat(s);
}
public String what_to_do_if_Foo2(bool b) {
return "something different".concat(b.toString());
}
}
Foo myFoo = new Foo1(3, "asdf");
FooEliminator<String> eliminator = new SomethingDifferentFooEliminator();
System.out.println(myFoo.eliminate(eliminator));
Effectively, the values we needed to construct the variants of our Algebraic Data Type become the parameters of the eliminator methods.
With similar situation to the previous conversion, this one is pretty much mechanical, which means we will probably see it in the future done automatically in programming languages.
Further reading and conclusion
As usual, the paper goes a lot more into type theory, category theory and lots of mathematical notation, which makes it much more precise to what I have written here. Unfortunately, all this precision and mathematical notation may make it a bit less understandable for beginners. I hope this article is a bit more beginner friendly, while still conveying the major points.
Finally, I want to thank Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones for the insightfully great paper they have written, and my good friend Juan Paucar for finding and telling me that the paper exists, as well as for proofreading the article.