ezyang's blog

Metro Maps of the News

Metro maps are a visual metaphor for complex, interdependent story lines developed by Dafna Shahaf. Dafna’s thesis involved techniques for automatically taking a corpus of news articles and extracting a coherent narratives that covered the overall space. For our final CS448b project, we took one of the narratives Dafna had generated and created a system for displaying the maps. (The demo is best viewed on a large monitor.)

We only had enough time to get the viewer aspect polished, but we think that it would not be too difficult to extend this framework for the construction of metro maps (in case you don’t have access to Dafna’s algorithm).

This is joint work with Russell Chou and Jacob Jensen.

Maildir synchronizing Sup

On the prompting of Steven Hum, I’ve put some finishing touches on my Sup patchset and am “releasing” it to the world (more on what I mean by “release” shortly.) The overall theme of this patchset is that it integrates as much Sup metadata it can with Maildir data. In particular:

• It merges Damien Leone’s sync-back patchset with the latest Sup mainline. The sync-back patchset synchronizes flags such as “Read” or “Trashed” to the Maildir, which can then be propagated back to your IMAP server using OfflineIMAP.
• Furthermore, this patchset has the ability to synchronize arbitrary labels, with a simple set of rules of what folder a message should be moved to depending on what labels it has. For example, inbox and archived messages can be kept in separate folders, so that non-Sup clients can usefully access mail you care about. (Trust me: this is really awesome.) This is coupled with a bonus OfflineIMAP patch which implements fast remote message moving.
• It implements inotify on Maildir, so a full directory scan is no longer necessary to retrieve new messages. The bottleneck for polling is now strictly OfflineIMAP.
• It implements the ability to save sent and draft messages to Maildir, so they show up in third-party clients.
• Finally, it has a number of miscellaneous bugfixes and extra hooks which I have personally found useful.

There is at least a high probability the patchset will work for you, since I’ve been using it actively for a while. Sup will sometimes crash; if it doesn’t happen reproduceably or cause data loss, I probably won’t investigate too hard. Some of my patches are a bit sketchy (especially those labeled HACK: I’ve attempted to document all the skeevy bits in commit messages and code comments.) So, how supported is this version of Sup? Well:

1. I am using this patchset, therefore, for all use-cases and environments I care about, it will stay working;
2. I will probably not fix problems I am not affected by, and definitely not problems I cannot reproduce;
3. I do not promise a stable commit history: I’ve rebased the patchset multiple times and will continue to do so.

Some of the early patches are pretty uncontroversial though, and I’d like to see them get into mainline eventually. You can get the code here: http://gitorious.org/~ezyang/sup/ezyang/commits/maildir-sync/

New hooks

sent-save-to
  Configures where to save sent mail to. If this hook doesn't exist,
  the global sent setting will be used (possibly defaulting to sup://sent)
  Variables:
      message: RMail::Message instance of the mail to send.
      account: Account instance matching the From address
  Return value:
       Source to save mail to, nil to use default

compose-from
  Selects a default address for the From: header of a new message
  being composed.
  Variables:
    opts: a dictionary of ComposeMode options, including :from, :to,
      :cc, :bcc, :subject, :refs and :replytos
  Return value:
    A Person to be used as the default for the From: header

draft-save-to
  Selects a source to save a draft to.
  Variables:
    from_email: the email part of the From: line, or nil if empty
  Return value:
    A source to save the draft to.

Label synchronization

To use this functionality, in config.yaml, you need a new option :maildir_labels:

:maildir_labels:
  :stanford: [[:inbox, 4], [null, 6]]

The value of this option is a dictionary of “accounts” to lists of precedences. (The account label stanford doesn’t actually mean anything; it’s just for documentation.) Read it as follows:

For messages belonging in source 4 or source 6 (consult sources.yaml), if the message has the :inbox tag, move it to source 4, otherwise move it to source 6.

This will automatically start working for any new mail you change the labels of. In order to apply this to old mail, you need to run sup-sync-back-maildir. If you’re going to move a lot of mail, you probably want to run this version of OfflineIMAP: https://github.com/ezyang/offlineimap

Why can't I just be a little lazy?

You can. Imagine a version of Haskell where every constructor was strict, e.g. every field had a ! prefix. The semantics of this language are well defined; and in fact, the fine folks at CMU have known about this for some time:

Up to this point we have frequently encountered arbitrary choices in the dynamics of various language constructs. For example, when specifying the dynamics of pairs, we must choose, rather arbitrarily, between the lazy dynamics, in which all pairs are values regardless of the value status of their components, and the eager dynamics, in which a pair is a value only if its components are both values. We could even consider a half-eager (or, equivalently, half-lazy) dynamics, in which a pair is a value only if, say, the first component is a value, but without regard to the second.

Similar questions arise with sums (all injections are values, or only injections of values are values), recursive types (all folds are values, or only folds of values are values), and function types (functions should be called by-name or by-value). Whole languages are built around adherence to one policy or another. For example, Haskell decrees that products, sums, and recursive types are to be lazy, and functions are to be called by name, whereas ML decrees the exact opposite policy. Not only are these choices arbitrary, but it is also unclear why they should be linked. For example, we could very sensibly decree that products, sums, and recursive types are lazy, yet impose a call-by-value discipline on functions. Or we could have eager products, sums, and recursive types, yet insist on call-by-name. It is not at all clear which of these points in the space of choices is right; each has its adherents, and each has its detractors.

Are we therefore stuck in a tarpit of subjectivity? No! The way out is to recognize that these distinctions should not be imposed by the language designer, but rather are choices that are to be made by the programmer. This may be achieved by recognizing that differences in dynamics reflect fundamental type distinctions that are being obscured by languages that impose one policy or another. We can have both eager and lazy pairs in the same language by simply distinguishing them as two distinct types, and similarly we can have both eager and lazy sums in the same language, and both by-name and by-value function spaces, by providing sufficient type distinctions as to make the choice available to the programmer.

This is from the Polarization chapter of Harper’s Practical Foundations for Programming Languages. Personally, I think call-by-name with (by default) eager data types by default is an under-appreciated point in the design space: with this combination, you still get the ability to implement your own control-flow structures like if (just not on data structures) and have lazy bindings, but you no longer have to worry about a large class of space leak. Of course, this regime doesn’t eliminate all problems: for example, if you foldl instead of foldl', you will still end up with a long line of function applications and stack overflow. It’s not clear to me if there is an alternative form of fix which dodges this bullet.

Functional Encryption

Joe Zimmerman recently shared with me a cool new way of thinking about various encryption schemes called functional encryption. It’s expounded upon in more depth in a very accessible recent paper by Dan Boneh et al.. I’ve reproduced the first paragraph of the abstract below:

We initiate the formal study of functional encryption by giving precise definitions of the concept and its security. Roughly speaking, functional encryption supports restricted secret keys that enable a key holder to learn a specific function of encrypted data, but learn nothing else about the data. For example, given an encrypted program the secret key may enable the key holder to learn the output of the program on a specific input without learning anything else about the program.

Quite notably, functional encryption generalizes many existing encryption schemes, including public-key encryption, identity-based encryption and homomorphic encryption. Unfortunately, there are some impossibility results for functional encryption in general in certain models of security (the linked paper has an impossibility result for the simulation model.) There’s no Wikipedia page for functional encryption yet; maybe you could write it!

Apropos of nothing, a math PhD friend of mine recently asked me, “So, do you think RSA works?” I said, “No, but probably no one knows how to break it at the moment.” I then asked him why the question, and he mentioned he was taking a class on cryptography, and given all of the assumptions, he was surprised any of it worked at all. To which I replied, “Yep, that sounds about right.”

Extremist Programming

Extremist programming (no relation to extreme programming) is the act of taking some principle, elevating it above everything else and applying it everywhere. After the dust settles, people often look at this extremism and think, “Well, that was kind of interesting, but using X in Y was clearly inappropriate. You need to use the right tool for the job!”

Here’s the catch: sometimes you should use the wrong tool for the job—because it might be the right tool, and you just don’t know it yet. If you aren’t trying to use functions everywhere, you might not realize the utility of functions that take functions as arguments [1] or cheap lambdas [2]. If you aren’t trying to use objects everywhere, you might not realize that both integers [3] and the class of an object [4] are also objects. If you aren’t trying to use laziness everywhere, you might not realize that purity is an even more important language feature [5].

This leads to two recommendations:

1. When learning a new principle, try to apply it everywhere. That way, you’ll learn more quickly where it does and doesn’t work well, even if your initial intuitions about it are wrong. (The right tool for the job, on the other hand, will lead you to missed opportunities, if you don’t realize that the principle is applicable in some situation).
2. When trying to articulate the essence of some principle, an extremist system is clearest. If you want to know what it is like to program with lazy evaluation, you want to use Haskell, not a language with optional laziness. Even if the extremist system is less practical, it really gets to the core of the issue much more quickly.

There are a lot of situations where extremism is inappropriate, but for fun projects, small projects and research, it can really teach you a lot. One of the most memorable interactions I had in the last year was while working with Adam Chlipala. We were working on some proofs in Coq, and I had been taking the moderate route of doing proofs step-by-step first, and then with Ltac automation once I knew the shape of the proof. Adam told me: “You should automate the proofs from the very beginning, don’t bother with the manual exploration.” [6] It was sage advice that made my life a lot better: I guess I just wasn’t extremist enough!

[1] Higher-order functions and combinators: these tend to not see very much airplay because they might be very verbose to write, or because the language doesn’t have a very good vocabulary for saying what the interface of a higher-order function is. (Types help a bit here.)

[2] Cheap lambdas are necessary for the convenient use of many features, including: monads, scoped allocation (and contexts in general), callbacks, higher-order functions.

[3] Consider early versions of Java prior to the autoboxing of integer and other primitive types.

[4] Smalltalk used this to good effect, as does JavaScript.

[5] This is one of my favorite narratives about Haskell, it comes from Simon Peyton Jones’ presentation Wearing the hair shirt (in this case, laziness).

[6] This is the essence of the Chlipala school of Coq proving, in recognition of how astonishingly easy it is to trick experienced computer scientists into writing the equivalents of straight-line programs by hand, without any abstractions.

Plan 9 mounts and dependency injection

“Everything is a file.” [1] This was the design philosophy taken to its logical extreme in Plan 9. Any interface you could imagine was represented as a file. Network port, pixel buffers, kernel interfaces—all were unified under a common API: the file operations (open, read, write…) Plan 9 used this to eliminate most of its system calls: it had only thirty-nine, in contrast to modern Linux’s sprawling three hundred and twenty-six.

When I first heard of Plan 9, my first thought was, “But that’s cheating, right?” After all, they had reduced the number of syscalls but increased the number of custom files: complexity had merely been shifted around. But one of my labmates gave me a reason why this was still useful: per-process mountpoints. These mountpoints meant that I could give each process their own view of the filesystem—usually the same, but sometimes with some vital differences. Suppose that I wanted to tunnel the network connection of one of my applications: this application would be accessing the network through some file, so I instead could mount a network filesystem to the network files of another system, and transparently achieve proxying without any cooperation from my application. [2]

Let’s step back for a moment and put on our programming language hats. Suppose that a file is an abstract data type, and the syscall interface for manipulating files is the interface for this data type. What are mounts, in this universe? Another friend of mine pointed out the perfectly obvious analogy:

Files : Mounts :: Abstract Data Types : Dependency Injection

In particular, the mount is a mechanism for modifying some local namespace, so that when a file is requested, it may be provided by some file system completely different to what the process might have expected. Similarly, dependency injection specifies a namespace, such that when an object is requested, the concrete implementation may be completely different to what the caller may have expected.

The overall conclusion is that when developers implemented dependency injection, they were reimplementing Plan 9’s local mounts. Is your dependency injection hierarchical? Can you replace a hierarchy (MREPL), or mount your files before (MBEFORE) or after (MAFTER) an existing file system? Support runtime changes in the mount? Support lexical references (e.g. dot-dot ..) between entities in the hierarchy? I suspect that existing dependency injection frameworks could learn a bit from the design of Plan 9. And in Haskell, where it seems that people are able to get much further without having to create a dependency injection framework, do these lessons map back to the design of a mountable file system? I wonder.

[1] Functional programmers might be reminded of a similar mantra, “Everything is a function.”

[2] For the longest time, Linux did not provide per-process mount namespaces, and even today this feature is not available to unprivileged users—Plan 9, in contrast, had this feature available from the very beginning to all users. There is also the minor issue where per-process mounts are actually a big pain to work with in Linux, primarily, I dare say, due to the lack of appropriate tools to assist system administrators attempting to understand their applications.

hp/D3.js: an interactive heap profile viewer

I’m taking a Data Visualization course this fall, and one of our assignments was to create an interactive visualization. So I thought about the problem for a little bit, and realized, “Hey, wouldn’t it be nice if we had a version of hp2ps that was both interactive and accessible from your browser?” (hp2any fulfills this niche partially, but as a GTK application).

A week of hacking later: hp/D3.js, the interactive heap profile viewer for GHC heaps. Upload your hp files, share them with friends! Our hope is that the next time you need to share a heap profile with someone, instead of running hp2ps on it and sending your colleague the ps file, you’ll just upload the hp file here and send a colleague your link. We’ve tested it on recent Firefox and Chrome, it probably will work on any sufficiently modern browser, it definitely won’t work with Internet Explorer.

Some features:

• You can annotate data points by clicking on the graph and filling in the text box that appears. These annotations are saved and will appear for anyone viewing the graph.
• You can filter heap elements based on substring match by typing in the “filter” field.
• You can drill down into more detail by clicking on one of the legend elements. If you click OTHER, it will expand to show you more information about the heap elements in that band. You can then revert your view by pressing the Back button.

Give it a spin, and let me know about any bugs or feature suggestions! (Some known bugs: sometimes Yesod 500s, just refresh until it comes up. Also, we lack backwards animations, axis changing is a little choppy and you can’t save annotations on the OTHER band.)

Ubuntu Quantal upgrade (Thinkpad/Xmonad)

October has come, and with it, another Ubuntu release (12.10). I finally gave in and reinstalled my system as 64-bit land (so long 32-bit), mostly because graphics were broken on my upgraded system. As far as I could tell, lightdm was dying immediately after starting up, and I couldn’t tell where in my copious configuration I had messed it up. I also started encrypting my home directory.

• All fstab mount entries now show up in Nautilus. The correct fix appears to be not putting these mounts in /media, /mnt or /home/, and then they won’t be picked up.
• Fonts continue to be an exquisite pain in rxvt-unicode. I had to switch from URxvt.letterSpace: -1 to URxvt.letterSpace: -2 to keep things working, and the fonts still look inexplicably different. (I haven’t figured out why, but the new world order isn’t a complete eyesore so I’ve given up for now.) There’s also a patch which fixes this problem (hat tip this libxft2 bug bug) but I found that at least for DejaVu the letterSpace hack was equivalent.
• When you manually suspend your laptop and close the lid too rapidly, Ubuntu also registers the close laptop event, so when you resume, it will re-suspend! Fortunately, this is pretty harmless; if you press the power-button again, it will resume properly. You can also work around this by turning off resume on close lid in your power settings.
• On resume, the network manager applet no longer accurately reflects what network you are connected to (it thinks you’re connected, but doesn’t know to what, or what signal strength it is). It’s mostly harmless but kind of annoying; if anyone’s figured this one out please let me know!
• Hibernate continues not to work, though I haven’t tried too hard to get it working.
• Firefox was being really slow, so I reset it. And then it was fast again. Holy smoke! Worth a try if you’ve found Firefox to be really slow.
• GHC is now 7.4.2, so you’ll need to rebuild. “When do we get our 7.6 shinies!”

My labmates continue to tease me for not switching to Arch. We’ll see…

ACM XRDS: Jeff Dean profile

I was wandering through the Gates building when the latest issue of the ACM XRDS, a student written magazine, caught my eye.

“Oh, didn’t I write an article for this issue?” Yes, I had!

The online version is here, though I hear it’s behind a paywall, so I’ve copypasted a draft version of the article below. Fun fact: The first version of this article had a Jeff Dean fact, but we got rid of it because we weren’t sure if everyone knew what Jeff Dean facts were…

True fact: as a high school student, Jeff Dean wrote a statistics package that, on certain functions, was twenty-six times faster than equivalent commercial packages. These days, Jeff Dean works at Google, helping architect and optimize some of the biggest data-crunching systems Google employs on a day-to-day basis. These include the well known MapReduce (a programming model for parallelizing large computations) and BigTable (a system which stores almost all of Google’s data). Jeff’s current project is infrastructure for deep learning via neural networks, a system with applications for speech/image recognition and natural language processing.

While Jeff has become a public face attached to much of Google’s internal infrastructure projects, Jeff stresses the fact that these projects require a mix of areas of expertise from people. Any given project might have people with backgrounds in networking, machine learning and distributed systems. Collectively, a project can achieve more than any person individually. The downsides? With all of the different backgrounds, you really need to know when to say: “Hold on, I don’t understand this machine learning term.” Jeff adds, however, that working on these teams is lots of fun: you get to learn about a sub-domain you might not have known very much about.

Along with a different style of solving problems, Google also has different research goals than academia. Jeff gave a particular example of this: when an academic is working on a system, they don’t have to worry about what happens if some really rare hardware failure occurs: they simply have to demo the idea. But Google has to worry about these corner cases; it is just what happens when one of your priorities is building a production system. There is also a tension with releasing results to the general public. Before the publication of the MapReduce paper, there was an internal discussion about whether or not to publish. Some were concerned that the paper could benefit Google’s competitors. In the end, though, Google decided to release the paper, and you can now get any number of open source implementations of MapReduce.

While Jeff has been at Google for over a decade, the start of his career looked rather different. He recounts how he ended up getting his first job. “I moved around a lot as a kid: I went to eleven schools in twelve years in lots of different places in the world… We moved to Atlanta after my sophomore year in high school, and in this school, I had to do an internship before we could graduate… I knew I was interested in developing software. So the guidance counselor of the school said, ‘Oh, great, I’ll set up something’, and she set up this boring sounding internship. I went to meet with them before I was going to start, and they essentially wanted me to load tapes into tape drives at this insurance company. I thought, ‘That doesn’t sound much like developing software to me.’ So, I scrambled around a bit, and ended up getting an internship at the Center for Disease Control instead.”

This “scrambled” together internship marked the beginning of many years of work for the CDC and the World Health Organization. First working at Atlanta, and then at Geneva, Jeff spent a lot of time working on what progressively grew into a larger and larger system for tracking the spread of infectious disease. These experiences, including a year working full-time between his graduation from undergraduate and his arrival at graduate school, helped fuel is eventual choice of a thesis topic: when Jeff took an optimizing compilers course, he wondered if he could teach compilers to do the optimizations he had done at the WHO. He ended up working with Craig Chambers, a new faculty member who had started the same year he started as a grad student. “It was great, a small research group of three or four students and him. We wrote this optimizing compiler from scratch, and had fun and interesting optimization work.” When he finished his PhD thesis, he went to work at Digital Equipment Corporation and worked on low-level profiling tools for applications.

Jeff likes doing something different every few years. After working on something for a while, he’ll pick an adjacent field and then learn about that next. But Jeff was careful to emphasize the fact that while this strategy worked for him, he also thought it was important to have different types of researchers, to have people who were willing to work on the same problem for decades, or the entire career—these people have a lot of in depth knowledge in this area. “There’s room in the world for both kinds of people.” But, as he has moved from topic to topic, it turns out that Jeff has come back around again: his current project at Google on parallel training of neural networks was the topic of Jeff’s undergraduate senior thesis. “Ironic,” says Jeff.

Duality for Haskellers

This post is the spiritual predecessor to Flipping Burgers in coBurger King.

What does it mean for something to be dual? A category theorist would say, “It’s the same thing, but with all the arrows flipped around.” This answer seems frustratingly vague, but actually it’s quite precise. The only thing missing is knowing what arrows flip around! If you know the arrows, then you know how to dualize. In this post, I’d like to take a few structures that are well known to Haskellers, describe what the arrows for this structure look like, and then show that when we flip the arrows, we get a dual concept.

Products and sums

Suppose you have some data of the type Either a b. With all data, there are two fundamental operations we would like to perform on them: we’d like to be able to construct it and destruct it. The constructors of Either are the Left :: a -> Either a b and Right :: b -> Either a b, while a reasonable choice of destructor might be either :: (a -> r) -> (b -> r) -> Either a b -> r (case analysis, where the first argument is the Left case, and the second argument is the Right case). Let’s draw a diagram:

I’ve added in two extra arrows: the represent the fact that either f g . Left == f and either f g . Right == g; these equations in some sense characterize the relationship between the constructor and destructor.

OK, so what happens when we flip these arrows around? The title of this section has given it away, but let’s look at it:

Some of these arrows are pretty easy to explain. What used to be our constructors (Left and Right) are now our destructors (fst and snd). But what of f and g and our new constructor? In fact, \x -> (f x, g x) is in some sense a generalized constructor for pairs, since if we set f = const a and g = const b we can easily get a traditional constructor for a pair (where the specification of the pair itself is the arrow—a little surprising, when you first see it):

So, sums and products are dual to each other. For this reason, sums are often called coproducts.

(Keen readers may have noticed that this presentation is backwards. This is mostly to avoid introducing \x -> (f x, g x), which seemingly comes out of nowhere.)

Top and bottom

The unit type (referred to as top) and the bottom type (with no inhabitants) exhibit a duality between one another. We can see this as follows: for any Haskell type, I can trivially construct a function which takes a value of that type and produces unit; it’s const ():

Furthermore, ignoring laziness, this is the only function which does this trick: it’s unique. Let’s flip these arrows around: does there exist a type A for which for any type B, there exists a function A -> B? At first glance, this would seem impossible. B could be anything, including an uninhabited type, in which case we’d be hard pressed to produce anything of the appropriate value. But wait: if A is uninhabited, then I don’t have to do anything: it’s impossible for the function to be invoked!

Thus, top and bottom are dual to one another. In fact, they correspond to the concepts of a terminal object and an initial object (respectively) in the category Hask.

One important note about terminal objects: is Int a terminal object? It is certainly true that there are functions which have the type forall a. a -> Int (e.g. const 2). However, this function is not unique: there’s const 0, const 1, etc. So Int is not terminal. For good reason too: there is an easy to prove theorem that states that all terminal objects are isomorphic to one another (dualized: all initial objects are isomorphic to one another), and Int and () are very obviously not isomorphic!

Folds and unfolds

One of the most important components of a functional programming language is the recursive data structure (also known as the inductive data structure). There are many ways to operate on this data, but one of the simplest and most well studied is the fold, possibly the simplest form a recursion one can use.

The diagram for a fold is a bit involved, so we’ll derive it from scratch by thinking about the most common fold known to functional programmers, the fold on lists:

data List a = Cons a (List a) | Nil
foldr :: (a -> r -> r) -> r -> List a -> r

The first two arguments “define” the fold, while the third argument simply provides the list to actually fold over. We could try to draw a diagram immediately:

But we run into a little bit of trouble: our diagram is a bit boring, mostly because the pair (a -> r -> r, r) doesn’t really have any good interpretation as an arrow. So what are we to do? What we’d really like is a single function which encodes all of the information that our pair originally encoded.

Well, here’s one: g :: Maybe (a, r) -> r. Supposing we originally had the pair (f, z), then define g to be the following:

g (Just (x, xs)) = f x xs
g Nothing = z

Intuitively, we’ve jammed the folding function and the initial value into one function by replacing the input argument with a sum type. To run f, we pass a Just; to get z, we pass a Nothing. Generalizing a bit, any fold function can be specified with a function g :: F a r -> r, where F a is a functor suitable for the data type in question (in the case of lists, type F a r = Maybe (a, r).) We reused Maybe so that we didn’t have to define a new data type, but we can rename Just and Nothing a little more suggestively, as data ListF a r = ConsF a r | NilF. Compared to our original List definition (Cons a (List a) | Nil), it’s identical, but with all the recursive occurrences of List a replaced with r.

With this definition in hand, we can build out our diagram a bit more:

The last step is to somehow relate List a and ListF a r. Remember how ListF looks a lot like List, just with r replacing List a. So what if we had ListF a (List a)—literally substituting List a back into the functor. We’d expect this to be related to List a, and indeed there’s a simple, unique function which converts one to the other:

in :: ListF a (List a) -> List a
in (ConsF x xs) = Cons x xs
in NilF = Nil

There’s one last piece to the puzzle: how do we convert from ListF a (List a) to ListF a r? Well, we already have a function fold g :: List a -> r, so all we need to do is lift it up with fmap.

We have a commuting diagram, and require that g . fmap (fold g) = fold g . in.

All that’s left now is to generalize. In general, ListF and List are related using little trick called the Mu operator, defined data Mu f = Mu (f (Mu f)). Mu (ListF a) is isomorphic to List a; intuitively, it replaces all instances of r with the data structure you are defining. So in general, the diagram looks like this:

Now that all of these preliminaries are out of the way, let’s dualize!

If we take a peek at the definition of unfold in Prelude: unfold :: (b -> Maybe (a, b)) -> b -> [a]; the Maybe (a, b) is exactly our ListF!

The story here is quite similar to the story of sums and products: in the recursive world, we were primarily concerned with how to destruct data. In the corecursive world, we are primarily concerned with how to construct data: g :: r -> F r, which now tells us how to go from r into a larger Mu F.

Conclusion

Dualization is an elegant mathematical concept which shows up everywhere, once you know where to look for it! Furthermore, it is quite nice from the perspective of a category theorist, because when you know two concepts are dual, all the theorems you have on one side flip over to the other side, for free! (This is because all of the fundamental concepts in category theory can be dualized.) If you’re interested in finding out more, I recommend Dan Piponi’s article on data and codata.