Category Archives: Uncategorized

LogicGrowsOnTrees

From haskell-cafe

Like many other packages on Hackage, LogicGrowsOnTrees provides an implementation of logic programming using MonadPlus;  in this sense it is nothing new.  What sets it apart is that it has been designed from the beginning to work in a distributed environment, allowing it to be parallelized over large numbers of processors with no shared memory.  The benchmarks I have run (using the N-Queens problem with 17-19 queens) showed essentially perfect speed-up all the way up to 256 cores, and the only reason why this number is not larger is because I haven’t had the opportunity to run tests on a larger cluster. 

If the benchmarks are fair, I think this is a big deal.  

I have a couple of projects on the backburner which use combinatorial search.  This is awesome.

Playground Programming

Every now and then, I have a small idea about a development environment feature I’d like to see. At that point, I usually say to myself, “make a prototype to see if I like it and/or show the world by example”, and start putting pressure on myself to make it. But of course, there are so many ideas and so little time, and at the end of the day, instead of producing a prototype, I manage just to produce some guilt.

This time, I’m just going to share my idea without any self-obligation to make it.

I’m working on Chrome’s build system at Google. We are switching the build scripts to a new system which uses an ingenious testing system that I’ve never seen before (though it seems like the kind of thing that would be well-known). For each build script, we have a few test inputs to run it on. The tests run all of our scripts on all of their test inputs, but rather than running the commands, they simply record the commands that would have been run into “test expectation” files, which we then check into source control.

Checking in these auto-generated files is the ingenious part. Now, when we want to change or refactor anything about the system, we simply make the change, regenerate the expectations, and do a git diff. This will tell us what the effects of our change are. If it’s supposed to be a refactor, then there should be no expectation diffs. If it’s supposed to change something, we can look through the diffs and make sure that it changed exactly what it was supposed to. These expectation files are a form of specification, except they live at the opposite end of the development chain.

This fits in nicely with a Haskell development flow that I often use. The way it usually goes: I write a function, get it to compile cleanly, then I go to ghci and try it on a few conspicuous inputs. Does it work with an empty list? What about an infinite list (and I trim the output if the output is also infinite to sanity check). I give it enough examples that I have a pretty high confidence that it’s correct. Then I move on, assuming it’s correct, and do the same with the next function.

I really enjoy this way of working. It’s “hands on”.

What if my environment recorded my playground session, so that whenever I changed a function, I could see its impact? It would mark the specific cases that changed, so that I could make sure I’m not regressing. It’s almost the same as unit tests, but with a friendlier workflow and less overhead (reading rather than writing). Maybe a little less intentional and therefore a little more error-prone, but it would be less error-prone than the regression testing strategy I currently use for my small projects (read: none).

It’s bothersome to me that this is hard to make. It seems like such a simple idea. Maybe it is easy and I’m just missing something.

Algebraic and Analytic Programming

The professor began my undergrad number theory class by drawing a distinction between algebra and analysis, two major themes in mathematics. This distinction has been discussed elsewhere, and seems to be rather slippery (to mathematicians at least, because it evades precise definition).  My professor seemed to approach it from a synesthetic perspective — it’s about the feel of it.  Algebra is rigid, geometric (think polyhedra) , perfect.  The results are beautiful, compact, and eternal.  By contrast, analysis is messy and malleable.  Theorems have lots of assumptions which aren’t always satisfied, but analysts use them anyway and hope (and check later) that the assumptions really do hold up.  Perelman’s famous proof of Poincare’s conjecture, as I understand, is essentially an example of going back and checking analytic assumptions.  Analysis often makes precise and works with the notion of “good enough” — two things don’t have to be equal, they only need to converge toward each other with a sufficiently small error term.

I have been thinking about this distinction in the realm of programming.  As a Haskell programmer, most of my focus is in an algebraic-feeling programming.  I like to perfect my modules, making them beautiful and eternal, built up from definitions that are compact and each obviously correct.  I take care with my modules when I first write them, and then rarely touch them again (except to update them with dependency patches that the community helpfully provides).  This is in harmony with the current practice of denotative programming, which strives to give mathematical meaning to programs and thus make them easy to reason about. This meaning has, so far, always been of an algebraic nature.

What a jolt I felt when I began work at Google.  The programming that happens here feels quite different — much more like the analytic feeling (I presume — I mostly studied algebraic areas of math in school, so I have less experience).  Here the codebase and its dependencies are constantly in motion, gaining requirements, changing direction.  “Good enough” is good enough; we don’t need beautiful, eternal results.  It’s messy, it’s malleable. We use automated tests to keep things within appropriate error bounds — proofs and obviously-correct code would be intractable.  We don’t need perfect abstraction boundaries — we can go dig into a dependency and change its assumptions to fit our needs.

Much of the ideological disagreement within the Haskell community and between nearby communities happens across this line.  Unit tests are not good enough for algebraists; proofs are crazy to an analyst.  QuickCheck strikes a nice balance; it’s fuzzy unit tests for the algebraist.  It gives compact, simple, meaningful specifications for the fuzzy business of testing.  I wonder, can we find a dual middle-ground?  I have never seen an analytic proof of software correctness.  Can we say with mathematical certainty that our software is good enough, and what would such a proof look like?

UPDATE: Here’s a lovely related post via Lu Zeng. Algebra vs. Analysis predicts eating corn?

Great people often seriously experienced their mortality or frailty in some way.  John Coltrane had four family members die in three months; Stephen Hawking contracted that motor thing he has; countless great musicians have lost a sense.  I can see how experiencing something unexpected and tragic would kick you in the pants to go all in on what you love, and do it now! These people understand their power and their freedom through their commitment.  Isn’t it ironic or profound that we can’t or absolutely would not choose to have such an experience, even in exchange for greatness?  In order to do what you love with the passion of greatness, would you choose to have most of your family die?  Could you give up sight, hearing, or movement?  Even if you did, would you not be filled with guilt or regret rather than experiencing the preciousness of life?  In this sense, nature blesses and curses at the same time, seemingly at random; we cannot invoke it or avoid it.  

Polyamory and Respect

I have been in an open, polyamorous relationship with my partner Amanda for about a year and a half. The relationship began as open for somewhat coincidental reasons, but over its course, I have developed a respect for polyamory — an understanding of why it makes sense for me, and why, I suspect, I might want my future relationships to be open as well1. And it is not for the reasons that most people think.

For the first time in the course of the relationship, I’m currently being intimate with someone else. However, I was supportive of polyamory before I had taken advantage of its freedoms, even though Amanda was seeing other people reasonably often. The question is: why? Why would I put myself in such a position? Why would I allow Amanda to sleep with other people while she is with me?

The key lies in a word of that final question — “allow”. To me, a healthy relationship is founded on mutual respect. There are many relationships which are not, but I find the most fulfillment from a relationship which is a coming together of two whole people with respect for each other. Anything else, to me, is just a fling (maybe a long-term one). So, under the supposition that I respect my partner, what does it mean to “allow” something? More pointedly, what does it mean to “disallow” something?

Both allowing and disallowing suppose that I have the power to make decisions for her. It supposes that I am informed enough, without even being present, to make the judgment call about whether her actions were right. In a traditional monogamous setting, I have a wholly un-nuanced view of the situation — if she has slept with someone else, she has made the wrong choice, and I, therefore, have been wronged, and I (with the assistance of social norms) am the one who has decided that.

Let’s imagine a polyamorous situation to help get to the heart of this. Let’s say that she met a new partner, and asked me if it’s okay if she sleeps with them. I will not respond with yes or no. She has offered me the power (and responsibility) to decide the best course of action for her, and I feel it necessary not to accept it. In accordance with my values, I can’t accept that power for anyone but myself: it would be a disservice to us both.

However, I don’t mean to say that there are never any emotions that come with it, or that if there are I have an obligation to bury them. Indeed, I often get jealous and feel hurt when she is with someone else. But as a partner, I want to understand. Why did what she did make sense to her? How did she perceive that would affect me? — knowing that I am considered in her decision-making process is important to me. I will communicate how it actually affected me. Perhaps I spent the night alone feeling shitty — it’s important for her to know that, to take that possibility into account next time she makes a decision, and it’s important for me to understand that I am still alive and that we still love each other. But the key is that, because of respect, I give her the benefit of the doubt that she made the best choice she had — I just want to understand her reasoning, and probably be reassured that she still cares — which she always has.

There are certain “codes” that I see as being very powerful, as leading to a stronger and more aligned internal experience. One of these is honesty — I am committed to always being open & honest (in a more nuanced way than I have been in the past). This is not because honesty in itself is “right”, but because integrity (i.e. always doing what I feel is right) is a quality that is important to me, and I have found that honesty is a code that is easy to verify (i.e. it is easy for me to know if I am abiding by it), which leads to integrity. This is because if I do something which I feel is wrong, I learn that, because of my code of open honesty, I will need to tell someone that I felt what I did was wrong. And that pressure is huge — I can no longer keep it to myself, now I need to show others about my lack of integrity when it happens. This pressure very quickly causes me to start acting with integrity.

In the same way, I see polyamory as a code which is easy to verify, which leads to respect as a consequence, and respect for my partner is something I value. Jealousy happens — when she talks to someone I can tell she thinks is attractive, when she stays out later than I expected her, when she tells me she has or had a crush on someone. But I know that we are in an open relationship — we have agreed that being attracted to others, even to the point of acting on it, is okay, and therefore my feeling of jealousy cannot be instantly transformed into a feeling of righteousness and being wronged. Hence, I have to consider the larger situation — I have to see where she is coming from, I have to understand her and her choices, I have to know her better. And in doing so I understand her values, her wishes, her way of being, her way of relating to others — and such a deep understanding leads me to respect her. I have not felt such a deep respect for anyone else I have ever been in a relationship with, and I think the openness of our relationship has been a major factor in that.

Further, polyamory leads to more communication and strength in our relationship. Consider “cheating” in a monogamous relationship. Let’s say I am in a monogamous relationship with my partner and, in a flush of sexually-excited irrationality I slept with someone else. I still love my partner very much and want to be with her, and we have a good, mutually supportive relationship, but I just made a mistake. (The idea that I could sleep with someone else while still being in love with her may seem impossible to some; that idea is worth examining — consider these prompts: masturbation, past relationships, fantasizing.) The question is, do I share my mistake with her? If I do share, it’s very likely that the relationship will end by social contract — many consider cheating to be an unforgivable offense. I don’t want the relationship to end, because I still love her and want to be with her. If I don’t share, I turn one wrong into two, and eventually many — not only have I wronged her with my actions, I wrong her by lying once about it — and, as lies are, probably many more times to cover up the first one. So not sharing is incompatible with my respect for her, and sharing is incompatible with my love and desire to be with her.

Would it not be easier for everyone if I felt free to share my mistake, if I were not in this terrible bind after making it? With the roles reversed, what would it say about how much I care if I were willing to put my partner in such a bind? Letting go of the moral attachment to fidelity allows this situation easily to be a conversation — she can tell me how it affected her, I can understand that and that may inform my desire not to be so reckless again. Perhaps the conversation will reveal something about our relationship dynamic that needs attention, or perhaps something that is secretly making us both unhappy (one of the possible causes of sleeping with someone else). In that sense we can make a plan to repair it, or possibly we will mutually agree it is in both of our best interests to end the relationship, allowing us to be friends afterward, feeling sadness for our loss but not hurt and anger, because we both know that it was the right decision. In the case that the relationship does not end, the conversation may have revealed a deep problem which we are now on the road to solving, strengthening the relationship and bringing us closer. And maybe it was no big deal, and we understand that as sexual beings sometimes we just need to feel attractive and get our rocks off, and the relationship has not been harmed. All of these are preferable to an abrupt end due to an objective wrong, in which one person feels deeply guilty and the other feels deeply wounded.

There are things which I will only briefly mention: for example, it is freeing to know that a friendship/relationship with someone other than my partner can develop in whatever way seems natural, without worrying if every action has crossed the line. This freedom allows me to get closer to others in my life, even if their gender allows some sexual tension, which brings me more fulfillment and happiness. In my experience, even though I like this other woman a lot, it has not in the least diminished the love I feel for Amanda, and experiencing that helps me see that it is probably the same for her when she is with someone else. In fact, since she has asked me for more reassurance now, I am verbalizing why I love her more, thus reminding myself and strengthening my sense of love for her. Where does the idea that love is a finite resource come from?

These are the reasons why polyamory makes sense to me as a way of conducting myself in relationship. It leads to more honest communication (and therefore more integrity), more mutual understanding and respect, and ultimately a stronger relationship. I see traditional monogamy as a way to defend yourself from scary thoughts of abandonment, but the cost is a dynamic in which it is possible to justify a sense of ownership over your partner, controlling them and taking away their free agency. Is that really worth it?

1One reason is that I get to have future relationships without first ending this wonderful one.

The Plan

Last September, I decided that it was time to get a programming job again. After two months of trying to find paid work (of any kind, $10 would have been great!) as a composer, I realized that it’s really hard. There are a lot of people willing to work for free, and without much of a scoring portfolio (as opposed to the “pure music” I do) I have no way to distinguish myself to the studios that have a budget. Also, a lot of games want orchestral scores, and I don’t have the hardware and software I need to make convincing-sounding synthetic orchestral scores. Also, I’m sure once I get the necessary hardware and software, I will need time to practice with it. In short, I needed money and time. I am extremely fortunate to have, in my free-flowing way, stumbled onto a skill that is valued by the economy, and so I decided it was once again time to utilize that skill to achieve my other goals. I planned to live reasonably cheaply, save up money so that I can buy equipment and support myself for enough time to build up a portfolio by doing free projects.

Now I have been programming for Clozure for almost six months. As far as jobs go, it’s great. I get to work in my favorite language, Haskell, and they give me enough freedom to experiment with designs and come up with solutions that not only work, but that I would even consider good. My fear of programming jobs was based on having jobs where I constantly have to compromise my values, either by working in crappy languages or on startup-style timelines where there is no time to lose. With this job, I feel reunited with my love of software, and my inspirations for developer support tools have been once again ignited.

And so I have amended the plan: after I have saved enough money to support myself for several years, I will not only attempt to bootstrap a career composing, but dedicate my current work week to making a reality the software ideas which have been floating around in my head for half a decade. This prospect really excites me — the reason I have not been able to make my ideas is mostly the time pressure: there’s was always something else I should be doing, and so I always felt guilty working on my pet projects. I wonder, what am I capable of if my pet projects are the main thing?

I want to revive CodeCatalog. Max and I lost steam on that project for a number of reasons.

  1. Due to family pressure, I returned to school.
  2. I fell in love with a girl and got my heart all broken. That can be kind of a downer.
  3. The priorities of the project compromised my vision. We were attempting to use modern wisdom to make the project successful: first impressions and intuitive usability came first. Our focus was on making it pretty and satisfying to use (which took a long time since neither of us were experienced web front-end developers), and that required me to strip off the most interesting parts of the project because noobs wouldn’t immediately understand it.

So I want to re-orient (3) to make it more satisfying for me. I want to allow myself to make the large strides that I envisage rather than baby-stepping toward success — to encourage myself to use my own talents in design and abstraction rather than trying to be a front-end person, to emphasize the exciting parts (what Audrey Tang calles -Ofun). By funding myself, I will not feel the guilt that comes with working on a project at the same time as (1). I can do no more than hope that something like (2) doesn’t happen. (I have a wonderful, stable and supportive relationship right now, so if that continues, that’d cover it :-)

I have many ideas; the reason I want to return to CodeCatalog in particular is mainly because I have identified most of my ideas as aspects of this project. My specific fancies change frequently (usually to things I have thought about before but never implemented), and so by focusing on this project in a researchy rather than producty way, I can entertain them while still working toward a larger goal and eventually benefitting the community.

Here is a summary of some ideas that fit in the CodeCatalog umbrella (just because I’m excited and want to remember):

  • Inter-project version control — I have always been frustrated by the inability of git and hg to merge two projects while still allowing interoperation with where they came from. The “project” quantum seems arbitrary, and I want to globalize it.
  • Package adapters — evolving the interface of a package without breaking users of the old interface by rewriting the old package in terms of the new one. There is a great deal that can be done automatically in this area with sufficient knowledge about the meaning of changes. I talked with Michael Sloan about this some, and some of the resulting ideas are contained in this writeup.
  • Informal checked documentation — documenting the assumptions of code in a machine-readable semi-formal language, to get the computer to pair-program with you (e.g. you write a division x/y and you have no y /= 0 assumption in scope, you’d get a “documentation obligation” to explain in english why y can’t be 0).
  • Structural editing — coding by transforming valid syntax trees. Yes it’d be cool, but the main reason it’s compelling to me is in its synergy with other features. Once you have the notion of focusing on expressions, holes with contextual information (a la Agda), semi-automatic creation of package and data-type adapters, smarter version control (e.g. a change might rename all references to an identifier, even the ones that weren’t there when the change was made) all come as natural extensions to the idea.

I think the challenge for me will be to focus on one of these for long enough to make it cool before getting distracted by another. My plan for that is to set short-term goals here on my blog and use it to keep myself in check. I am considering involving other people in my project as a way to keep myself focused (i.e. maybe I can make a little mini-kickstarter in which my devotees can pledge small amounts in exchange for me completing a specific goal on time).

This is all two years away or more, which feels like a long time, but in the grand scheme is not that long in exchange for what I see as the potential of this endeavor. I’m just excited and couldn’t help but to think about it and get pumped up. Thanks for reading!

Oh, despite the date, this is totally not an April Fools joke (as far as I know ;-).

Follow Your Nose Proofs

We just had the first Categories for the Boulderite meetup, in which a bunch of people who don’t know category theory tried to teach it to each other. Some of the people there had not had very much experience with proofs, so getting “a proof” was hard even though the concepts weren’t very deep. I got the impression that those who had trouble mainly did because they did not yet know the “follow your nose” proof tactic which I learned in my first upper division math class in college. That tactic is so often used that most proofs completely omit it (i.e. assume that the reader is doing it) and skip to when it gets interesting. Having it spelled out for me in that class was very helpful. So here I shall repeat it, mostly for my fellow Categories members.

Decide what to do based on a top-down analysis of the sentence you are trying to prove:

Shape of Sentence Shape of Proof
If P, then Q. (aka. P implies Q) Suppose P. <proof of Q>
P if and only if Q (→) <proof of if P implies Q>. (←) <proof of Q implies P>
For all x such that C(x), Q Given x. Suppose C(x). <proof of Q>
There exists x such that Q. Let x = <something> (requires imagination). <proof of Q>
P or Q Either <proof of P> or <proof of Q> (or sometimes something tricksier like assume not P, <proof of Q>)
P and Q (1) <proof of P>. (2) <proof of Q>.
not P Assume P. <find contradiction> (requires imagination)
X = Y Reduce X and Y by known equalities one step at a time (whichever side is easier first). Or sometimes there are definitions / lemmas that reduce equality to something else.
Something really obvious (like X = X, or 0 ≤ n where n is a natural, etc.) Say “obvious” or “trivial” and you’re done.
Something else Find definition or lemma, substitute it in, continue.

Along the way, you will find that you need to use the things you have supposed. So there is another table for how you can use assumptions.

Shape of assumption Standard usage
If P, then Q (aka P implies Q) Prove P. Then you get to use Q.
P if and only if Q P and Q are equivalent. Prove one, you get the other.
For all x such that C(x), P(x) Prove C(y) for some y that you have, then you get to use P(y).
There exists x such that C(x) Use x and the fact that C(x) somehow (helpful, right? ;-).
P and Q Therefore P / Therefore Q.
P or Q If P then <goal>. If Q then <same goal>. (Or sometimes prove not P, then you know Q)
not P Prove P. Then you’re done! (You have inconsistent assumptions, from which anything follows)
X = Y If you are stuck and have an X somewhere in your goal, try substituting Y. And vice versa.
Something obvious from your other assumptions. Throw it away, it doesn’t help you.
Something else Find definition, substitute it in, continue.

Let’s try some examples. First some definitions/lemmas to work with:

Definition (extensionality): If X and Y are sets, then X = Y if and only if for all x, x \in X if and only if x \in Y.
Definition: X \subseteq Y if and only if for every a, a \in X implies a \in Y.

Theorem: X = Y if and only if X \subseteq Y and Y \subseteq X.

Follow your nose proof.

  • (→) Show X = Y implies X \subseteq Y and Y \subseteq X.
    • Assume X = Y. Show X \subseteq Y and Y \subseteq X.
    • Substitute: Show X \subseteq X and X \subseteq X.
    • We’re done.
  • (←) Show X \subseteq Y and Y \subseteq X implies X = Y.
    • Assume X \subseteq Y and Y \subseteq X. Show X = Y.
    • (expand definition of = by extensionality)
    • Show forall x, x \in X if and only if x \in Y.
    • Given x.
    • (→) Show x \in X implies x \in Y.
      • Follows from the definition of our assumption X \subseteq Y.
    • (←) Show x \in Y implies x \in X.
      • Follows from the definition of our assumption Y \subseteq X.

See how we are mechanically disassembling the statement we have to prove? Most proofs like this don’t take any deep insight, you just execute this algorithm. Such a process is assumed when reading and writing proofs, so in the real world you will see something more like the following proof:

Proof. (→) trivial. (←) By extensionality, x \in X implies x \in Y since X \subseteq Y, and x \in Y implies x \in X since Y \subseteq X.

We have left out saying that we are assuming things that you would naturally assume from the follow your nose proof. We have also left out the unfolding of definitions, except perhaps saying the name of the definition. But when just getting started proving things, it’s good to write out these steps in detail, because then you can see what you have to work with and where you are going. Then begin leaving out obvious steps as you become comfortable.

We have also just justified a typical way to show that two sets are equal: show that they are subsets of each other.

Let’s see one more example:

Definition: Given sets A and B, a function f : A → B is a surjection if for every y \in B, there exists an x \in A such that f(x) = y.

Definition: Two functions f,g : A → B are equal if and only if for all x \in A, f(x) = g(x).

Definition: (g \circ f)(x) = g(f(x)).

Definition: For any set A, the identity \mathit{Id}_A is defined by \mathit{Id}_A(x) = x.

Theorem: Given f : A → B. If there exists f-1 : B → A such that f \circ f^{-1} = \mathit{Id}_B, then f is a surjection.

Follow your nose proof.

  • Given f : A → B.
  • Suppose there exists f-1 : B → A and f \circ f^{-1} = \mathit{Id}_B. Show f is a surjection.
  • By definition, show that for all y \in B, there exists x \in A such that f(x) = y.
  • Given y \in B. Show there exists x \in A such that f(x) = y.
  • Now we have to find an x in A. Well, we have y \in B and a function from B to A, let’s try that:
  • Let x = f^{-1}(y). Show f(x) = y.
  • Substitute: Show f(f^{-1}(y)) = y.
  • We know f \circ f^{-1} = \mathit{Id}_B, so by the definition of two functions being equal, we know f(f^{-1}(y)) = \mathit{Id}_B(y) = y, and we’re done.

Again, notice how we are breaking up the task based on the structure of what we are trying to prove. The only non-mechanical things we did were to find x and apply the assumption that f \circ f^{-1} = \mathit{Id}_B. In fact, usually the interesting parts of a proof are giving values to “there exists” statements and using assumptions (in particular, saying what values you use “for all” assumptions with). Since those are the interesting parts, those are the only parts that an idiomatic proof would say:

Proof. Given y \in B. Let x = f^{-1}(y). f(x) = f(f^{-1}(y)) = y since f \circ f^{-1} = \mathit{Id}_A.

Remember to take it step-by-step; at each step, write down what you learned and what you are trying to prove, and try to make a little progress. These proofs are easy if you follow your nose.

Constructions on Typeclasses, Part 1: F-Algebras

This post is rendered from literate Haskell. I recommend doing the exercises inline, so use the source.

> {-# LANGUAGE DeriveFunctor
>            , DeriveFoldable
>            , DeriveTraversable
>            , TypeOperators #-}
>
> import Control.Applicative
> import Data.Foldable
> import Data.Traversable

Certain kinds of typeclasses have some very regular instances. For example, it is obvious how to implement (Num a, Num b) => Num (a,b) and (Monoid a, Monoid b) => Monoid (a,b), and similarly if F is some applicative functor, (Num a) => Num (F a) and (Monoid a) => (Monoid F a) are obvious. Furthermore, these instances (and many others) seem to be obvious in the same way.

(+) a b     = (+)     <$> a <*> b
mappend a b = mappend <$> a <*> b

fromInteger n = pure (fromInteger n)
mempty        = pure mempty

And take them on pairs:

(x,x')     +     (y,y')  = (x     +     y, x'     +     y')
(x,x') `mappend` (y,y')  = (x `mappend` y, x' `mappend` y')

fromInteger n = (fromInteger n, fromInteger n)
mempty        = (mempty       , mempty)

It would be straightforward for these cases to derive the necessary implementations from the type signature. However, it would be nice if there were a more abstract perspective, such that we didn’t have to inspect the type signature to find the operations – that they could arise from some other standard construction. Further, it is not quite as obvious from the the type signature how to automatically instantiate methods such as

mconcat :: (Monoid m) => [m] -> m

without making a special case for [], whereas hopefully a more abstract perspective would inform us what kinds of type constructors would be supported.

In this post, we will see such an abstract perspective. It comes from (surprise!) category theory. I disclaim that I’m still a novice with category theory (but in the past few weeks I have gained competence by studying). So we will not get very deep into the theory, just enough to steal the useful concept and leave the rest behind. I welcome relevant insights from the more categorically educated in the comments.

F-Algebras

The unifying concept we will steal is the F-algebra. An F-algebra is a Functor f and a type a together with a function f a -> a. We can make this precise in Haskell:

> type Algebra f a = f a -> a

I claim that Num and Monoid instances are F-algebras over suitable functors. Look at the methods of Monoid:

mempty :: m
mappend :: m -> m -> m

We need to find a functor f such that we can recover these two methods from a function of type f m -> m. With some squinting, we arrive at:

> data MonoidF m
>     = MEmpty
>     | MAppend m m
>
> memptyF :: Algebra MonoidF m -> m
> memptyF alg = alg MEmpty
>
> mappendF :: Algebra MonoidF m -> (m -> m -> m)
> mappendF alg x y = alg (MAppend x y)

Exercise 1: work out the functor NumF over which Num instances are F-algebras, and write the methods of Num in terms of it.

Exercise 2: for each of the standard classes Eq, Read, Show, Bounded, and Integral, work out whether they are expressible as F-algebras. If so, give the functor; if not, explain or prove why not.

Exercise 3: write a function toMonoidAlg which finds the MonoidF-algebra for a given instance m of the Monoid class.

Combining Instances

Motivated by the examples in the introduction, we can find the “instance” for pairs given instances for each of the components.

> pairAlg :: (Functor t) => Algebra t a -> Algebra t b -> Algebra t (a,b)
> pairAlg alga algb tab = (alga (fmap fst tab), algb (fmap snd tab))

Also, we hope we can find the instance for an applicative functor given an instance for its argument

applicativeAlg :: (Functor t, Applicative f)
               => Algebra t a -> Algebra t (f a)

but there turns out to be trouble:

applicativeAlg alg tfa = ...

We need to get our hands on an t a somehow, and all we have is a t (f a). This hints at something from the standard library:

sequenceA :: (Traversible t, Applicative f) => t (f a) -> f (t a)

which indicates that our functor needs more structure to implement applicativeAlg.

> applicativeAlg :: (Traversable t, Applicative f)
>                => Algebra t a -> Algebra t (f a)
> applicativeAlg alg tfa = fmap alg (sequenceA tfa)

Now we should be able to answer the query from the beginning:

Exercise 4: For what kinds of type constructors c is it possible to automatically derive instances for (a) pairs and (b) Applicatives for a typeclass with a method of type c a -> a. (e.g. mconcat :: [a] -> a). Demonstrate this with an implementation.

Combining Classes

Intuitively, joining the methods of two classes which are both expressible as F-algebras should give us another class expressible as an F-algebra. This is demonstrated by the following construction:

> data (f :+: g) a = InL (f a) | InR (g a)
>     deriving (Functor, Foldable, Traversable)
>
> coproductAlg :: (Functor f, Functor g)
>              => Algebra f a -> Algebra g a -> Algebra (f :+: g) a
> coproductAlg falg _ (InL fa) = falg fa
> coproductAlg _ galg (InR ga) = galg ga

So now we can model a subclass of both Num and Monoid by type NumMonoidF = NumF :+: MonoidF.

Exercise 5: We hope to be able to recover Algebra NumF a from Algebra NumMonoidF a, demonstrating that the latter is in fact a subclass. Implement the necessary function(s).

Exercise 6: Given the functor product definition

> data (f :*: g) a = Pair (f a) (g a)
>     deriving (Functor, Foldable, Traversable)

find a suitable combinator for forming algebras over a product functor. It may not have the same form as coproduct’s combinator! What would a typeclass formed by a product of two typeclasses interpreted as F-algebras look like?

Free Constructions

One of the neat things we can do with typeclasses expressed as F-algebras is form free monads over them – i.e. form the data type of a “syntax tree” over the methods of a class (with a given set of free variables). Begin with the free monad over a functor:

> data Free f a
>     = Pure a
>     | Effect (f (Free f a))
>     deriving (Functor, Foldable, Traversable)
>
> instance (Functor f) => Monad (Free f) where
>     return = Pure
>     Pure a >>= t = t a
>     Effect f >>= t = Effect (fmap (>>= t) f)

(Church-encoding this gives better performance, but I’m using this version for expository purposes)

Free f a can be interpreted as a syntax tree over the typeclass formed by f with free variables in a. This is also called an “initial algebra”, a term you may have heard thrown around in the Haskell community from time to time. We demonstrate that a free construction over a functor is a valid F-algebra for that functor:

> initialAlgebra :: (Functor f) => Algebra f (Free f a)
> initialAlgebra = Effect

And that it is possible to “interpret” an initial algebra using any other F-algebra over that functor.

> initiality :: (Functor f) => Algebra f a -> Free f a -> a
> initiality alg (Pure a) = a
> initiality alg (Effect f) = alg (fmap (initiality alg) f)

Exercise 7: Give a monoid isomorphism (a bijection that preserves the monoid operations) between Free MonoidF and lists [], ignoring that Haskell allows infinitely large terms. Then, using an infinite term, show how this isomorphism fails.

Next time: F-Coalgebras

How GADTs inhibit abstraction

Today I want to talk about this snippet:

This program ought to be well-behaved — it has no recursion (or recursion-encoding tricks), no undefined or error, no incomplete pattern matches, so we should expect our types to be theorems. And yet we can get inconsistent. What is going on here?

Exercise: Identify the culprit before continuing.

The problem lies in the interaction between GADTs and generalized newtype deriving. Generalized newtype deriving seems to be broken here — we created a type B which claims to be just like A including instances, but one of A‘s instances relied on it being exactly equal to A. And so we get a program which claims to have non-exhaustive patterns (in unSwitchB), even though the pattern we omitted should have been impossible. And this is not the worst that generalized newtype deriving can do. When combined with type families, it is possible to write unsafeCoerce. This has been known since GHC 6.7.

In this post I intend to explore generalized newtype deriving and GADTs more deeply, from a more philosophical perspective, as opposed to just trying to plug this inconsistency. There are a few different forces at play, and by looking at them closely we will see some fundamental ideas about the meaning of types and type constructors.

Generalized newtype deriving seems reasonable to us by appealing to an intuition: if I have a type with some structure, I can clone that structure into a new type — basically making a type synonym that is a bit stricter about the boundaries of the abstraction. But the trouble is that you can clone parts of the structure without other parts; e.g. if X is an applicative and a monad, and I declare newtype Y a = Y (X a) deriving (Monad), then go on to define a different Applicative instance, I have done something wrong. Monad and applicative are related, so you can’t just change them willy nilly as though they were independent variables. But at the very least it seems reasonable that you should be able to copy all the structure, essentially defining a type synonym but giving it a more rigorous abstraction boundary. But in Haskell, this is not possible, and that is because, with extensions such as GADTs and type families, not all of a type’s structure is clonable.

I’m going to be talking a lot about abstraction. Although the kind of abstraction I mean here is simple, it is one of the fundamental things we do when designing software. To abstract a type is to take away some of its structure. We can abstract Integer to Nat by taking away the ability to make negatives — we still represent as Integer, but because the new type has strictly fewer operations (it must be fewer — after all we had to implement the operations somehow!) we know more about its elements, and finely tuning that knowledge is where good software engineering comes from.

When implementing an abstraction, we must define its operations. An operation takes some stuff in terms of that abstraction and gives back some stuff in terms of that abstraction. Its implementation must usually use some of the structure of the underlying representation — we define addition on Nat by addition on Integer. We may take it for granted that we can do this; for example, we do not have trouble defining:

    sum :: [Nat] -> Nat

even though we are not given any Nats directly, but instead under some type constructor ([]).

One of the properties of type constructors that causes us to take this ability to abstract for granted is that if A and B are isomorphic (in a sense that will become clear in a moment), then F A and F B should also be isomorphic. Since we, the implementers of the abstraction, are in possession of an bijection between Nats and the Integers that represent them, we can use this property to implement whatever operations we need — if they could be implemented on Integer, they can be implemented on Nat.

This isomorphism property looks like a weak version of saying that F is a Functor. Indeed, F is properly a functor from a category of isomorphisms in which A and B are objects. Every type constructor F is a functor from some category; which category specifically depends on the structure of F. F's flexibility to work with abstractions in its argument is determined by that category, so the more you can do to that category, the more you can do with F. Positive and negative data types have all of Hask as their source category, so any abstractions you make will continue to work nicely under them. Invariant functors like Endo require bijections, but fortunately when we use newtype to create abstractions, we have a bijection. This is where generalized newtype deriving gets its motivation -- we can just use that bijection to substitute the abstraction for its representation anywhere we like.

But GADTs (and type families) are different. A functor like Switch b has an even smaller category as its domain: a discrete category. The only thing which is isomorphic to A in this category is A itself -- whether there is a bijection is irrelevant. This violates generalized newtype deriving's assumption that you can always use bijections to get from an abstraction to its representation and back. GADTs that rely on exact equality of types are completely inflexible in their argument, they do not permit abstractions. This, I claim, is bad -- you want to permit the user of your functor to make abstractions.

(Aside: If you have a nice boundary around the constructors of the GADT so they cannot be observed directly, one way to do this when using GADTs is to simply insert a constructor that endows it with the necessary operation. E.g. if you want it to be a functor from Hask, just insert

    Fmap :: (a -> b) -> F a -> F b

If you want it to be a functor from Mon (category of monoids), insert:

    Fmap :: (Monoid n) => MonoidHom m n -> F m -> F n

(presumably F m already came with a `Monoid` dictionary). These, I believe, are free constructions -- giving your type the structure you want in the stupidest possible way, essentially saying "yeah it can do that" and leaving it to the consumers of the type to figure out how.)

In any case, we are seeing something about GADTs specifically that simple data types do not have -- they can give a lot of different kinds of structure to their domain, and in particular they can distinguish specific types as fundamentally different from anything else, no matter how similarly they may behave. There is another way to see this: defining a GADT which mentions a particular type gives the mentioned type unclonable structure, such that generalized newtype deriving and other abstraction techniques which clone some of a type's structure no longer succeed.

DI Breakdown

I’m having a philosophical breakdown of the software engineering variety. I’m writing a register allocation library for my current project at work, referencing a not-too-complex algorithm which, however, has many degrees of freedom.  Throughout the paper they talk about making various modifications to achieve different effects — tying variables to specific registers, brazenly pretending that a node is colorable when it looks like it isn’t (because it might work out in its favor), heuristics for choosing which nodes to simplify first, categorizing all the move instructions in the program to select from a smart, small set when the time comes to try to eliminate them.  I’m trying to characterize the algorithm so that those different selections can be made easily, and it is a wonderful puzzle.

I also feel aesthetically stuck.   I am feeling too many choices in Haskell — do I take this option as a parameter, or do I stuff it in a reader monad?  Similarly, do I characterize this computation as living in the Cont monad, or do I simply take a continuation as a parameter?  When expressing a piece of a computation, do I return the “simplest” type which provides the necessary data, do I return a functor which informs how the piece is to be used, or do I just go ahead and traverse the final data structure right there?  What if the simplest type that gives the necessary information is vacuous, and all the information is in how it is used?

You might be thinking to yourself, “yes, Luke, you are just designing software.”  But it feels more arbitrary than that — I have everything I want to say and I know how it fits together.  My physics professor always used to say “now we have to make a choice — which is bad, because we’re about to make the wrong one”.  He would manipulate the problem until every decision was forced.  I need a way to constrain my decisions, to find what might be seen as the unique most general type of each piece of this algorithm.  There are too many ways to say everything.