Sunday, May 20, 2012

Thank you, KeyRemap4MacBook!

At long last! I managed to fully reproduce my Linux xmodmap layout on OS X.


I don't think I have particularly peculiar typing needs. I often type code, which frequently uses characters like "[", "{", and "<". Those are easy to type using the US keyboard layout. I also often type French, which frequently uses accented characters like "é", "à", and "û". In that situation, most people opt for switching between keyboard layouts depending on the situation. I, however, opted for a custom keyboard layout.

My custom keyboard layout is mostly the US keyboard layout, plus some Alt+key combinations for dead keys like "´", "`", and "^". On Linux, this was easy to setup using xmodmap. Implementing the keyboard layout on OS X was a bit more complicated, because its XML representation of keyboard layouts is very long and it's not easy to test changes incrementally, but I eventually managed to do it.


Then one day, I decided that the modifier keys were too low.

I am not even using Emacs, but typing Ctrl with my pinky is really twisting my hand in a way I don't like. So I bought an ergonomic keyboard. It didn't help.


One of the reasons I chose this particular keyboard was because of the two little extra arrow keys below the space bar. I thought I could remap them to Ctrl and Shift, thereby allowing me to type those troublesome modifiers using my thumb instead of my pinky. That didn't work either. The keyboard preferences which were installed with the keyboard helpfully allow me to remap those to any other key... except modifiers. No luck directly modifying the layout files either, not even through keyboard layout creation tools like Ukulele. I did manage to turn Caps Lock into an extra Ctrl, but the other modifiers looked like they would be stuck in place forever.


I had no such problems with Linux. Again using xmodmap, I converted the key above the enter into an extra Shift key, much to the relief of my right pinky. The only annoyance with this solution was that I kept trying to use that key as a Shift on the Mac computer too, only to be presented with a disappointing backslash character as a result.

Well, those days are now behind me! Today, I downloaded KeyRemap4MacBook, a very helpful tool which managed to accomplish what so many others had failed. I am now typing this text on my Mac, using the backslash key as a Shift! And my right pinky is very grateful.


Thanks, KeyRemap4MacBook!

Sunday, April 29, 2012

Building qtHaskell on OS X

Update

The author of qtHaskell recommends a simpler approach. In addition to the "slotReject" patch below, simply change lines 308-309 of build.pl as follows:

$ghcdv = ((($ghcmv == 6) && ($ghcsv >= 12)) || ($ghcmv > 6)) ? 1 : 0;
$ghcfv = ((($ghcmv == 6) && ($ghcsv < 12)) || ($ghcmv < 6)) ? 1 : 0;

Original post

Finally! I spent the entire weekend on this, but I finally managed to compile qtHaskell on OS X. I spent a lot of that time on the internet googling for the error messages I encountered, to no avail. So, to save some time to the next person who google them, here is what worked for me. The qtHaskell documentation recommends that you use their ./build perl script. That almost works, but not quite. Thankfully, by giving arguments to the scripts, we can run the parts which work, and skip over the parts which don't. Speaking of arguments, one the most annoying errors is the "scattered reloc r_address too large" error message which only occurs at the very end of a very length compilation. I stumbled upon a page recommending to use "--extra-ld-opt=--architecture=x86_64" to fix a similar error message, and since then I have superstitiously stuck the argument everywhere I could, just to be sure. So, let's build qtHaskell, shall we? First of all, qtHaskell is a set of Haskell bindings for Qt, so you need to install Haskell and Qt. I used Qt 4.7.1, qtHaskell 1.1.4, and GHC 7.0.4 (64 bits). Actually I had the 32 bits version of GHC at first, and that let to the aforementioned r_address problems, followed by linking problems afterwards. Better upgrade to 64 bits!
brew uninstall ghc
brew install ghc --64bits
We should now be ready to compile qtHaskell proper. There are actually two parallel hierarchies to be compiled, the C++ implementation and its Haskell FFI interface. Both are very large, because, well, Qt is large. First, the C++ part: no problems here, the build script works just fine for this part.
./build user cpp qmake cmake \
    --extra-ld-opt=--architecture=x86_64
./build user cpp-install \
    --extra-ld-opt=--architecture=x86_64 --no-sudo
Note that even though the "user" flag was given, the build script will still install the files globally in /usr/local/lib/libqtc_*. Presumably, the flag is only for the Haskell part, for which the steps would ideally be as follows.
./build user haskell configure \
    --extra-ld-opt=--architecture=x86_64
./build user haskell build \
    --extra-ld-opt=--architecture=x86_64
./build user haskell-install \
    --extra-ld-opt=--architecture=x86_64 --no-sudo
Unfortunately, the middle step fails with the following error message.
unrecognised command: makefile (try --help)
runghc Setup.hs makefile: No such file or directory
Fear not! This cryptic-looking error message is actually a clue towards the solution. Apparently, "runghc Setup.hs makefile" is the command used for building the Haskell part. Using the help, as recommended in the error message, leads to the following alternative build commands.
runghc Setup.hs configure --user \
    --extra-ld-opt=--architecture=x86_64
runghc Setup.hs build
Unfortunately, that doesn't work either, at least not with a recent GHC. There is a problem in the qtHaskell code, which leads to the following error message.
Qtc/Core/Attributes.hs:583:13:
    Could not deduce (Qstt a (QDialogSc b))
      arising from a use of `slotReject''
    from the context (Qstt a (QDialogSc b1))
      bound by the instance declaration
      at Qtc/Core/Attributes.hs:581:10-52
    Possible fix:
      add (Qstt a (QDialogSc b)) to the context of
        the instance declaration
      or add an instance declaration for (Qstt a (QDialogSc b))
    In the expression: slotReject'
    In an equation for `reject'': reject' = slotReject'
    In the instance declaration for `QsaSlotReject a'
If you are familiar with Haskell, you should be able to fix the problem on your own. Alternatively, you could grab Uduki's hsQt fork of qtHaskell, which comes pre-patched. Or you might apply the following patch yourself:
diff --git a/Qtc/Core/Attributes.hs b/Qtc/Core/Attributes.hs
index 197c506..217d585 100755
--- a/Qtc/Core/Attributes.hs
+++ b/Qtc/Core/Attributes.hs
@@ -580,7 +580,7 @@ class QsaSlotReject w where
 
 instance (Qstt a (QDialogSc b)) => QsaSlotReject (a) where
   slotReject' = (Qslot "reject()", \_ -> ())
-  reject' = slotReject'
+  reject'     = (Qslot "reject()", \_ -> ())
 
 class QsaSignalRejected_nt_f w x f where
   signalRejected', rejected' :: x -> SltConf w f
Now that the source is patched, the Haskell part should finally compile.
runghc Setup.hs build
If you run out of memory during this phase, just run the command again. And again. As many times as it takes to compile all the targets. When you get the the very last target, qtHaskell is finally linked... and then, like me, you might get one of those nasty "scattered reloc r_address too large" errors. Did you? If so, you might have skipped the very first step and be stuck with a 32 bits version of GHC. Check using "ghc --info". If you insist on using the 32 bits version, you could try the following variant of the build command, which got me through that step. Still got troubles when linking programs using qtHaskell, though.
runghc Setup.hs configure --user --disable-library-for-ghci
Now that the Haskell part is built, we can finally install it! This time, the "user" flag is honored.
./build user haskell-install \
    --extra-ld-opt=--architecture=x86_64 --no-sudo
Let's test this! The qtHaskell helpfully provides the following Hello World code, just put it in a file with the "hs" extension and build it into an executable using "ghc --make".
module Main where

import Qtc.Classes.Qccs
import Qtc.Classes.Gui
import Qtc.Gui.Base
import Qtc.Gui.QApplication
import Qtc.Gui.QPushButton

main :: IO Int
main = do
  qApplication ()
  hello <- 60::int="" ello="" hello="" nt="" pre="" qapplicationexec="" qpushbutton="" qshow="" qthaskell="" resize="" world="">
Tada!
At long last. A button!

Saturday, March 31, 2012

As the story dragged on


The main reason I decided to experiment with non user-visible stories was to keep stories short. That part worked great; as long as they were short, I breezed through the stories and was eager to start the next. But then one particular story — I'm looking at you, story 19! — turned out to be a lot more work than expected. As the story dragged on, I lost my motivation... and then it took even longer to get it done. I would like to avoid this situation in the future, if possible.

But how? By adjusting my process, of course! Ideally, I should be able to complete each story in one sitting; and now that stories don't need to be user-centric, there is no reason not to make them as small as needed. If they aren't, then the plan needs to be refined. Thus, this time, I am going to break something even more fundamental than the user-centric nature of stories: the fixed-length iterations! How naughty.

This iteration will end in one week, or when a story drags on for more than a day, whichever happens first. If it is the latter, I will have the opportunity to adjust the offending task, by dividing it into smaller chunks.


Alternatively, I could rethink my design so that the offending task is not needed, or vastly simpler. Or just different. Or more fun to code.

I mention this possibility because I stumbled upon a post from a writer explaining how she quintupled her productivity by optimizing her process, and she found out that she was more productive when writing scenes she was enthusiastic about. Well, I was enthusiastic about Story 20. And hated Story 19. I'm not sure why.

In order to figure it out, from now on I am also going to write down the best and the worst story of each iteration. Hopefully, a pattern will emerge. Although, to be honest, even if I had an easy criterion to distinguish stories which are going to be fun from those which are going to be boring, I don't really know what I could do with that information. Sure, some stories are less pleasant than others, but they still need to get done, right? Unlike passages in a book, if the code is boring to write, it doesn't mean the user won't enjoy the result. Who knows, maybe I'll find a different software organization which minimizes annoying tasks?


Iteration 5

As yet another crazy departure from conventions, I'm dropping story numbers. They haven't been very useful so far.
  • Setup continuous compilation (using Substrate to detect when the source files change).
  • Use signals to propagate errors.
  • Implement an InputNode which can bake itself.
  • Implement a Gui which links the input nodes with the input pane widget.

Saturday, March 17, 2012

Who cares about the user?

As promised, I am going to play with my process. Unlike what I promised, I am not going to waste an entire iteration on this. I am going to waste several!

I have already tried one change: scheduling optional stories. It didn't work, but I'm glad I tried. I am not on a tight schedule, so I can take the time to experiment and see what works. I even tried the Spiral idea of trashing all my code and starting from scratch using my newly accumulated experience: that's what I did on the very first iteration, when I decided to drop everything and start fresh, Agile-style this time. What should I try for the next iteration?


Well, is there something from the last iteration which could be improved? Let's see, was there anything at all which went wrong? Let me think. Oh, right. Maybe the fact that I totally failed to produce anything at all?

Yeah, during the past iteration, I didn't accomplish much. Or rather, that's what you would think if you only looked at the number of stories I completed: zero. And indeed, when I run Substrate, it looks exactly as it did two weeks ago. But that is only part of the picture! Sure, the look didn't change and there are no new buttons to click on, but I did spend a lot of time working on Substrate, trying out new architectures and comparing design approaches. Even as I worked, I felt like I was wasting precious time, because days went by and my metric wasn't improving.

Well, screw the metric. Screw the users, I mean. Erh... that's not what I meant either.


This iteration, I am testing a variant on story descriptions: instead of focusing on user-visible features, I am going to focus on developer-visible features. If code needs to be written, then I don't care whether that code is producing buttons, menus, bells, or whistles: by golly, this code is going to be divided into small story-like chunks and assigned to an iteration!


Iteration 4

This iteration is still about geting Substrate to interact with external files, but the steps to reach this goal are more detailed. Stories 18 and 20 have no user-visible impact.

Story 10 (1 story point): I can save the current project. Use a version number in case the format changes.
Stories 11 to 16: Postponed.
Story 17 (1 story point): I can reload and run the entire project.
Story 18 (1 story point): Simple filesystem-backed key-value store with one file per key.
Story 19 (2 story points): The project reloads when the filesystem copy of the store changes.
Story 20 (2 story points): Specialized store interface for strings, integers, and string arrays.
Story 21 (1 story point): The project stores the active input tab.


p.s.: Don't take the title of this post seriously. The only user Substrate ever had, so far, is myself.

Thursday, March 15, 2012

Unifying the Agile and Spiral models

If, like me, you have never heard of the Spiral model of development, here is a summary: it is a bit like Agile, except that all the code is thrown away at the end of the iteration. Also, the scope increases each time, so the iterations grow longer and longer.

Yes, I know this sounds like a terrible idea, but that's only when compared to Agile as a reference point. From that angle, Waterfall is the model where you only get one, very big, very long iteration, and hope to get it right the first time. When put in the context in which it was invented, doesn't the Spiral idea of starting with a smaller version of the project seem like a great improvement?

Not throwing away the code all the time sounds like an even better improvement, but when I first heard of the Spiral model (just a few hours ago), I thought the opposite. Throwing code away! What a novel and intriguing idea! Should I try? Maybe? Being in an Agile team doesn't guarantee good design, after all. And changing a bad design is sometimes a large endeavor. With Substrate, for example, I haven't been able to implement any story at all this iteration, because I was busy refactoring the entire application to use MVC.


Instead of being forced to either drop all the existing code or keep all of it, I suggest we should be allowed to do either. And those two possibilities are just two ends of a continuum: using version control, we can easily revert to a number of intermediate steps between the two extremes, whichever is most convenient.


An Example

Let's start with an empty project, in the middle of Design Space, the space of all possible designs.



We discuss the product idea, draw a bit of UML, and end up with a particular design (a particular point in Design Space).



A few iteration go by, moving the project toward the goal established in the design.



While implementing new features, suppose we come up with a new design for the project. Could happen! Otherwise, we would still be doing big design up front and it would work great. The goal is moved a bit to the left.



Since we are using iterations, we adapt to this unexpected change without a sweat. We just start writing the new code with the new code in mind!




But what if the new design was very, very different from the first?



In that case, starting from scratch is less work.



But this is not an all or nothing decision. Yes, you can start from scratch, but you can also start from any other past point. Just pick the one which represents the least amount of work!



Future Work

Now, as I said, I only heard about the Spiral model today, so there are still many rough corners in my generalization of it and Agile. For one thing, going back in time means removing some features, and if those features have shipped already, maybe you don't want to remove them. Feature Space is not necessarily aligned with Design Space.

The other big problem is that history is linear, while Design Space is multidimensional. When your goal changes its position, it probably won't move across all the dimensions, only some of them. So while it is true that some of your code can be thrown away, most of it probably shouldn't; in order to reach the commit you want to restart from, you will have to throw away some commits which are still good, just because they were submitted after the restarting commit. I recommend using a history-rewriting tool such as git, but when I tried, solving all the merge conflicts was still a lot of work.


Ideally, each new feature could be implemented on a bare-bones version of the application, containing only the elements on which the new feature builds. In that setting, implementing the new feature is much easier, because there are no unexpected interactions with the other features, the codebase is small enough to be understood all at once, and the debug-edit-compile cycle is fast. Theoretically, using feature branches, maybe this ideal could even be reached!

The problem, of course, is that the unexpected interactions bite back once we try to merge all of the feature branches into a complete product.

I think I am going to try anyway. If I can afford wasting an entire iteration redesigning my code, maybe I can also waste one redesigning my process?

Tuesday, February 28, 2012

Still not ready for private consumption


Good news! This time, I did manage to find a use for Substrate. It turns out that if you want to suck the motivation out of your programmers and make them want to quit, forcing them to use Substrate is a really good way to achieve that!

So, yeah. Eating your own dog food is a great way to find flaws in your own software, but not necessarily a good way to get them fixed. I mean, I want to fix them, I do, but the idea of eating my own dog food is that I should be using Substrate to manipulate its own source code. So I'm supposed to fix those debilitating flaws using a debilitatingly flawed software. No fun there! It would also take a while, because the sub-par tool would drag me down. Better do it all in vim and forget about the dog thing.


Iteration 3

This iteration is about using Substrate and vim, together. My goal is to make Substrate a good complement for vim.

My goal was never to replace vim. That would be silly! I was not thinking of Substrate as a text editor at all, but as a text manipulator. Sometimes I would need an editor, and sometimes I would need a manipulator. But I have now realized that I won't be developing Substrate using Substrate, I will be developing Substrate using vim! Mostly vim. So if I want to keep Substrate in the loop, to eat it as dog food, then I need Substrate and vim to play along.

And to do that, I need Substrate to interact with the external files I'll be editing in vim.


Story 10 (1 story point): I can save the current project. Use a version number in case the format changes.
Story 11 (1 story point): I can run the script with a particular file as input.
Story 12 (1 story point): I can run the script with each file from a directory (recursively) as input.
Story 13 (1 story point): I can run the script with only the changed files as input.
Story 14 (2 story point): I can perform story 13 from the command line, or when a file change is detected.
Story 15 (1 story point): I can write multiple parallel scripts (all with the same input).
Story 16 (1 story point): I can write multiple sequential scripts (feeding one into the other).


No "bonus" stories this iteration, not anymore. Listing the stories in advance gives me a short term goal to accomplish, and that's motivating. There no motivation in completing optional stories: who am I trying to impress? I just want to be done with the mandatory stories as early as possible, and play video games for the rest of the week.

Saturday, February 18, 2012

What one hat said to the other

Developers know which features would be easy to add, but it is users who know which features would be useful to add. This is why, after completing what I thought was the Minimal Viable Product version of Substrate, I decided to trade my Developer hat for a User hat. This turned out to be a very, er, humbling experience.

I wanted to know which lack-of-a-feature was causing the most pain to my non-existent users. To find out, I tried to use Substrate for all the tasks it could handle. And the main conclusion of my experiment was that there were, in fact, very few tasks it could handle. Or, as User hat would put it: What a crappy, buggy, useless software.


Well, thanks for your feedback, User hat. For what it's worth, Developer hat here is more worried about "useless" than about "buggy". That's because I, too, aspire to be a User some day! I want to eat my own dogfood. Substrate is a text manipulation tool, code is made of text... surely one day a version of Substrate will be useful enough for me to use it while developing later versions?

One day, perhaps, but not yet. The current Substrate is great for twea— ok, the current Substrate is a crappy, buggy program aiming to make it easy to tweak long chains of bash commands. But even if it wasn't buggy, the bigger problem is that very few tasks can actually be accomplished through a single long chain of bash commands.


I'm really glad I tried this MVP approach, because this is a major flaw which I could only have discovered by actually using the software, as opposed to merely developing it. I have long paid lip service to The Unix Way, and I am not alone in thinking that a few carefully chained Unix commands can go a long way. But not, it would seem, all the way.

Since my long term vision for Substrate was a GUI for creating complex chains of text-manipulating nodes, I need to revise my approach. And that's precisely what short iterations are for, aren't they?


Iteration 2

In this iteration, I will focus on adding new features, not on fixing the many bugs User hat found. Hopefully, by the end of the iteration, Substrate will evolve into a crappy, buggy, marginally useful product. Useful enough, I hope, for Developer hat to use.

Story 5 (1 story point): I can enter different inputs for the script.
Story 6 (1 story point): I can run the script on a series of different inputs.
Story 7 (2 story point): I can save the script and its inputs as a single project.
---
Story 8 (2 story point): I can write multiple scripts which call each other.
Story 9 (2 story point): I can write a script which applies multiple inputs to another script.


Adjusting from last iteration, this time I intend to finish the first three stories in two weeks, not one month. I have also added two optional stories, in case I finish early again. This is my personal extension to the Agile process: even if your velocity indicates that you can only deliver 4 story points per iteration, you should still schedule a bit more than that. I'll let you know if it's a great way to empirically measure by how much to increase your velocity, or just another idea which sounds better to one hat than to the other.

Thursday, February 09, 2012

Success!

Has it only been a week? Wow. This challenge was both easier and harder than expected.

Easier, because I expected to finish in a month, rather than a week. I'm really bad at making time estimates.

Harder, because I ended up writing much more code than I expected. I initially thought that I would implement the four stories back-to-back, with a few lines of code each. That was the plan. But I ended up organizing my code a lot, and implementing a few visual niceties which were not in the original stories. I'm really bad at sticking to a plan.


In any case, tada! Here is Substrate, iteration 1.

The greyed-out text is one of the extra visual niceties
I couldn't help but add. This shows you which lines
are going to run when you press F5.


That's right! I escaped from my curse, and completed a project: an MVP version of Substrate. I think laying down a plan at the beginning really helped, even if I didn't follow it too closely. I'll definitely need to write down new stories for iteration 2. But not yet.

For now, I need to play a bit with the product. Only then, as a user, will I have the authority to decide which parts of the product could be improved.

Saturday, February 04, 2012

May the day I actually complete something finally come

Completing projects is hard

I have a curse.

My curse is that I have too many great ideas. Now, I know that ideas are cheap, so I don't just publicly announce my ideas and then complain that nobody is acting on them. I know that if I want my ideas to have an impact, I must act on them myself. I do act! But I'm still cursed.

Often, my idea is something that I can code on a computer. That's great! I have a computer, and I know how to code. I can act. So I put everything aside, fire up my favorite text editor, and enthusiastically put in the hours necessary to create something out of nothing. But it doesn't work! I'm still cursed.

The main problem with this "put everything aside" approach is that the main thing I put aside is usually the code I was writing in order to implement my previous idea. And by the time the code for my new idea becomes something usable, it will in turn be shoved aside by an even newer, better idea! That's why great ideas are my curse. If only I was coming up with worse and worse ideas instead of better and better ones!


Well, this curse ends now.

I was discussing Agile with Nadya yesterday, and I asked her how small she thought a team could be while still being Agile and benefiting from it. Since she and I love to work on common projects, I expected her to answer "two", suggesting that our common projects should use Agile. But to my surprise, she answered "one".

I guess it makes sense. If following the Agile methodology can help a team to ship, why couldn't it help me complete my personal projects? Let's give it a shot.


The project I will actually complete

My current project is Substrate, a text processing tool making it easy to build text processing pipelines.

I got that idea while using Houdini, a 3D software package making it easy to build 3D-model and 2D-image processing pipelines. It's very different from other 3D packages. Using Houdini was much more fun than using 3DS Max. Houdini felt more like programming than modelling, but at the same time, it also felt more fun than programming. Very few things do! I suddenly wanted all of my tools to be like Houdini.

I started immediately, and that was my first mistake. I should have taken the time to figure out what it was that made Houdini so different. Instead, I immediately started working on a Houdini clone, with the major exception that my clone would manipulate text, not 3D models.

So far, I have a pane system where I can open and close tabs, split panes horizontally and vertically, and... well, that's it, really. No text manipulation yet. I just copied Houdini's pane system because Houdini had it. From an Agile perspective, the state of the project is highly embarrassing: totally unshippable, with the "team" focussing on miscellaneous GUI features over the core functionality.


Well, this ends now.

I still don't know what it is that makes Houdini feel different, but I will find it. Iteration after iteration. And each iteration will be shippable. Amen.


Iteration 1

Since I am working on this during my free time, I will need relatively long iterations in order to have enough coding hours to produce anything. Let's say one month: I shall have a shippable MVP at the end of February. And here is what this MVP will contain.

Story 1 (1 story point): I can load a Bash script and view its contents.
Story 2 (1 story point): I can run the currently-loaded script and run it using a command from the menu. I will see the script's output on stdout.
Story 3 (1 story point): I can run a prefix of the script using a command from the menu. I will see the output of the truncated script on stdout, or an error if the truncated code doesn't represent a valid Bash script.
Story 4 (1 story point): I can successfully run a script prefix even if the last line ends with a pipe character.

The hypothesis tested by this first iteration is that while working on a pipeline, the ability to see intermediate results from the middle of the pipeline will make it much easier to debug the pipeline. The Houdini feature which corresponds to this is the ability to click on any node to see what the 3D model looks like at this point.

I'm not convinced that this is really what makes Houdini fun to use, but it's certainly a core feature, and it's one which I am confident I can implement quickly.


Well, let's get to work!

Friday, December 30, 2011

An unusual "terms and conditions" page


You might have noticed my new "Terms and conditions" page, above. But then again, if you're like most users, you probably haven't.

Which is the whole point.


Nobody reads those pointless agreement pages, yet they are legally binding. This is crazy! I don't want to be legally bound by contracts I haven't even read.

For this reason, today, I counter-attack using my own "Terms and conditions" page. I am not a lawyer, but if I ever get into trouble with one of the many agreement pages I have not read, my opponents should not be able to claim that I am bound by their terms and conditions without accepting that they are also bound by mine.


It is not legal to encourage someone to sign a contract without reading it. Similarly, it should not be legal to encourage a user to click "I agree" without reading and understanding the conditions he or she is agreeing to. Yet, that is precisely what service providers are doing! Successful service providers streamline their website's user experience to encourage a particular behaviour, for example, signing up for the service. And my experience with online agreements is that the encouraged behaviour is always to click "I agree" without reading anything.

For example, service providers often go to great lengths making sure the product offering is crystal clear, by using short punchy sentences or video presentations. By contrast, those same service providers use many pages of long-winded, cryptic legalese to describe their legal agreement. And even when I do take the time to read and consider such terms, I am often rejected with a "this page has expired" message.

The only way to reach the service, in this case, is to click "I agree" without reading the contract. Since that is the expected behaviour, that's what I am going to do from now on. But since you don't expect me to read your contracts, don't expect me to be bound by them.

Monday, December 05, 2011

Our Life in 3D

By the way, my girlfriend and I will be updating the blog Our Life in 3D, a blog about our common project: modelling her entire condo using Houdini and 3DS Max.

Wednesday, September 14, 2011

Time != Money

Today's xkcd comic depends on a very common, but unjustified economic equation: that time is money. More precisely, I am objecting to the practice of using a person's hourly salary to evaluate the amount of money lost when that person wastes one hour of his time.

Granted, if that person wastes time during working hours, then he costs at least that much to his employer. At least as much, because employers expect employee work to yield returns over and above the cost of their salary; otherwise, it would be economically pointless to have employees.

But why would the employee himself be deemed to lose that money? If he wastes his time during office hours, he gets his hourly salary anyway. If the time wasted is not during office hours, then the opportunity cost of wasting this time is zero: had he done something else with his time, he would not be earning any money either.

Perhaps "time is money" only applies to startup founders, whose startup-related work directly impact their bottom line. But this line of thinking works precisely because founders don't have an hourly salary; rather, their net worth is a function of the worth of the company they own. So it still doesn't make sense to compare time and hourly salary.

That being said, I still think that Time is a very precious resource. I want to enjoy every minute of it; I just don't buy the idea that I'm wasting money doing so.

Saturday, October 09, 2010

Equality is a (useless) transmutation machine

Even since I heard about the Curry-Howard isomorphism, I've been wondering: to which computational principle corresponds equality? and the axiom of choice? and all those other mathematical concepts which would probably be much more intuitive to me in computational form? Unfortunately, there is no Curry-Howard dictionary translating concepts from one domain to the other, much like a French-English dictionary would translate words from one language to the other.

A few of the correspondances are well-known. A proposition corresponds to a type, and the proofs of this proposition correspond to the inhabitants of this type. A theorem using the hypothesis A to prove proposition B corresponds to a function from type A to type B.

A number N corresponds to a type with exactly N inhabitants. The multiplication A × B corresponds to the tuple type (A, B). The addition A + B corresponds to the algebraic type Either A B, whose set of inhabitants is the disjoint union of the inhabitants of A and the inhabitants of B. The exponentiation BA corresponds to the function type A → B. But what is equality?

In Agda, a programming language / theorem prover exploiting the Curry-Howard isomorphism, (propositional) equality is defined as follows.

agda data _≡_ {X} : X → X → Set where agda refl : (x : X) → x ≡ x

I must admit that this doesn't help much. This states that the only valid proof for x ≡ y is refl x, and even then, it only proves that x ≡ x. In other words, the only inhabitants of the type x ≡ y are values of the form refl x, which actually have type x ≡ x.

A more inspiring piece of Agda code is an example showing how to make use of an equality proof.

agda subst : {X : Set} agda → (P : X → Set) agda → (x y : X) agda → x ≡ y agda → P x agda → P y agda subst P .v .v (refl v) p = p

This code takes some arbitrary proposition P(x), say, "x is prime", a proof that x equals y, a proof that P(x) is true, and concludes that P(y) is also true. For example since 7 is prime and 3 + 4 equals 7, it follows that 3 + 4 is also prime. The code does this by pattern-matching on the proof that x ≡ y, obtaining refl v for some value v. Since refl v has both type v ≡ v and type x ≡ y, Agda concludes that x and y are both v. This changes the type of p from P x to P v and the type of the goal from P y to P v, making it possible for subst to return p.

The feat is more impressive if we use counter-factual equalities. If P(x) says that "x is pink", and you have a proof that Leonardo the Flamingo is pink, and also a counter-factual proof that Leonardo the flamingo is "equal" to Bob the Filthy Frog, then you can convince anyone that Bob is pink, thereby gaining him access to all those cool pink-only bars in town. An x ≡ y equality instance is like a machine you can use to transmute x's access cards into access cards for y.

For this reason, it is in the interest of all the cool pink kids that equality instances should be hard to forge.

And equality instance really are hard to forge. refl x has type x ≡ x, remember? The only transmuter you can build is the one which doesn't actually perform any transmutation. Hence my title: equality is a (useless) transmutation machine.


Oh! One last thing. The bird's-eye view of this post is that equality is a transmutation machine because by using subst, equality instances can be used to transmute things. Couldn't it be that using functions other than subst, equality instances could be used to do even more incredible (yet useless) things?

It turns out the answer is no: an equality instance is no stronger than a substitution machine. The proof of this is that from a substituting machine, we can obtain an equality instance, as follows.

agda unsubst : {X : Set} agda → (x y : X) agda → (subst : (P : X → Set) → P x → P y) agda → x ≡ y agda unsubst x y subst = subst (λ – → x ≡ –) (refl x)

We simply use our substitution machine to transmute the trivial equality instance refl x of type x ≡ x into an equality instance of type x ≡ y. Tada! Equality is (as strong as) a transmutation machine.

Friday, September 17, 2010

How to cope with changing requirements

the context

Programming an application is a complicated endeavor. Often, people outside of the field greatly misjudge the amount of work necessary to implement one; either by vastly underestimating the work necessary to build programs similar to the ones they already use, or by vastly overestimating the work necessary to build programs unlike the ones they already use.

A misguided client in the first category might, for example, come to you saying he would like you to build him a program "just like Microsoft Word, except that [such and such]". An equally misguided client in the second category might be manually adding the same country code to a list of phone numbers every day, because his partners are sending him phone numbers of potential clients, he has to post these phone numbers on a website in order to filter out the numbers that are on the do-not-call-list, and the website expects the phone numbers in a slightly different format.

In a way, the second situation is sadder than the first. In the first situation, the programmer will of course explain immediately that Microsoft Word has a lot of hidden features and that single-handedly duplicating the entire application would take forever. But in the second situation, the poor client might continue to manually perform the task for years until a colleague with some programming experience happens to step into his office at the right moment to ask what he's doing.

the problem

This lack of magnitude appreciation causes a lot of problems when comes the time to settle for the price of a commissioned application. Ideally, clients would know exactly what they want and programmers would know exactly how much work it will take to build what is wanted. In practice, however, clients change their requirements mid-way once they see how their imagined program looks like in real life, or ask for "just one little extra feature" which requires a complete redesign of the application. Programmers could simply stubbornly refuse to deviate from the specification; but alas, not only this isn't a way to treat a paying client, programmers are also notoriously bad at estimating the amount of time a given task will take them.

There exists a number of methodologies (agile, SCRUM...) which aim to solve this problem by involving the client in the process. The basic idea is very simple: if you show intermediate versions of the product to your client, he will change his mind sooner, so you will waste less time working on a version which your client doesn't like.

I must admit that I am not very familiar with these methodologies. My understanding is that they are intended for teams of programmers working together on a single project, so that you would only bother to learn about a methodology if your manager suggests or decides that your team should use it. For an individual programmer working with an individual client, these methodologies look overkill. They sell books explaining these methodologies, and you want to write code, not read books.

the solution

Here's a very simple, no-book-required methodology.

The first time your client comes to see you, let him awkwardly attempt to explain what he wants. Ignore his ill-conceived notion of what the program should look like or how one would use it; you broadly understand what he's trying to accomplish, right? Good. Now, give your client a magazine and tell him that the first version of his software will be ready in an hour. "ONE hour? no way." He'll be shocked, but he'll wait. He won't even notice that you haven't started discussing compensation yet. I bet he didn't expect to see a demo for at least a month.

Now, of course you won't have a working program ready within an hour. But you certainly have the time to create a crude mockup of a program. A few buttons here and there, with the keywords you have heard him rant about written on them. They don't have to do anything when you click on them. The important thing is to have something to show the client as soon as you can.

Once the hour is complete, show the program to the client and tell him that this is version zero, and that many features are still missing. Okay, let's be honest, all of the features are missing, but from the point of view of the client, what you are showing him is already impressive. It's an application built just for him, with buttons labelled with the things he cares about, and it's only been an hour since he met you. I bet he thinks that making the buttons actually do something is "just one little extra feature".

And actually, it is. Let your client play with the mockup interface for a while, then ask him to pick one single feature he would like you to add during the next hour. Help him to pick something of the appropriate complexity. Now, once he understands that the application is going to be built step-by-step, one small feature at a time, and now that he understands how small such a one-step feature actually is, now is the time to discuss pricing.

Ask to be paid a fixed price per version. He's already seen the first version, and you have just told him what the next version will look like, so he can roughly assess how much a single version is worth to him. Negotiate the price as needed. Of course, the client doesn't have to visit every hour for the entire project; after confidence is built, he will probably ask on his own if he could simply give you a list of half a dozen features and come back six versions later. Just make sure not to let him list all the features of his misconceived dream application in one go.

Having the client only pay for running programs also gets rid of one painful situation in which the programmer is making progress on the internals of the application while the client sees an accumulation of bills and no concrete progress, gives up, and decides to cut his losses by abandoning the project. But the point of this payment method is mainly to let the client notice by himself that he can't keep on asking for "just one more little feature" forever, as each time he does so, he pays a little more. Eventually, the client will need to decide that the software is good enough for his needs, and walk away with the last version he paid for.

Wednesday, December 09, 2009

intra-line diff

Introducing linediff, a quick ruby wrapper around diff to highlight changed words instead of changed lines.
#!/usr/bin/ruby
pre, post = $stdin.read.split("\n=======\n")
post[-1..-1] = ""

class String
  def bash
    `bash -c #{inspect.gsub("$", "\\$")}`
  end

  def binspect
    split("\n").map {|s|
      "echo #{s.inspect.gsub("$", "\\$")}"
    }.join(";")
  end

  def to_lines
    gsub("\n", "\\n").gsub(" ", "\n")
  end
  def to_lines!
    gsub!("\n", "\\n")
    gsub!(" ", "\n")
  end

  def to_words
    gsub("\n", " ").gsub("\\n", "\n")
  end
  def to_words!
    gsub!("\n", " ")
    gsub!("\\n", "\n")
  end
end

pre.to_lines!
post.to_lines!
len = pre.length+post.length

both = "diff -U#{len} <(#{pre.binspect}) <(#{post.binspect})".bash
both = both.split("\n")[3..-1]

pre = both.select {|s| s[0..0] != "+"}.join("\n")
post = both.select {|s| s[0..0] != "-"}.join("\n")

pre.gsub!(/^-/, "+")
pre.gsub!(/^ /, "")
post.gsub!(/^ /, "")

pre.to_words!
post.to_words!

puts "#{pre}\n=======\n#{post}"
I use it mostly to handle git conflicts which, in my current setup, show up more often than they should (I repeatedly sync with both a git and an svn repository, which I should not be doing according to git-svn). Here's an example conflict. Can you spot the difference?
<<<<<<< HEAD:thesis.tex
    Once we are done with binary functions, we turn to unary functions, shifting our focus from the aspect weavers to the aspects themselves. Our goal is to help programmers to build aquariums containing the aspects they need, while minimizing the number of proofs needed to achieve this goal. To this end, we provide several generic proofs that create, extend, and translate aquariums with aspects of specific forms. Note, however, that not every pair of functions that commute can be shown to do so using our proofs only, so the programmers are expected to complete our collection with proofs of their own whenever the aspects they need are not of the specific forms covered by our theorems.
    \begin{enumerate}
    \item For every associative and commutative binary function, such as those created using our unordered pair strategy, we can create an aquarium of unary functions corresponding to the elements of the algebraic datatype.
    \item Given an aquarium containing a function $f$, the aquarium can be extended with function $f^n$, for any natural number $n$. The function $f^n$ is the function which repeatedly applies, $n$ times, the function $f$. If $f$ is invertible, the theorem extends to negative integers.
=======
    Once we are done with binary functions, we turn to unary functions, shifting our focus from the aspect weavers to the aspects themselves. Our goal is to help programmers to build aquariums containing the aspects they need, while minimizing the number of proofs needed to achieve this goal. To this end, we provide several generic proofs that create, extend, and translate aquariums with aspects of specific forms. Note, however, that not every pair of functions that commute can be shown to do so using our proofs only, so the programmers are expected to complete our collection with proofs of their own whenever the aspects they need are of the specific forms covered by our theorems.
    \begin{enumerate}
    \item For every associative and commutative binary function, such as those created using our unordered pair strategy, we can create an aquarium of unary functions corresponding to the elements of the algebraic datatype.
    \item Given an aquarium containing a function $f$, the aquarium can be extended with function $f^n$, for any natural number $n$. The function $f^n$ is the function which repeatedly applies, $n$ times in total, the function $f$. If $f$ is invertible, the theorem extends to negative integers.
>>>>>>> df2a5b6eb97ded25a34412d6ff946e0c513da6f3:thesis.tex
    \item If $M$ is a functor, then applying $M$ to all the members of an aquarium transforms the aquarium into a new one, while preserving the pairwise commutativity of its elements.
    %\item We show how parametricity \cite{free_theorems} ensures that structure-manipulating aspects cannot interfere with element-manipulating aspects, thereby reducing the programmer's remaining burden of proof.
    \end{enumerate}
When I encounter such a conflict, I select the code between the "<<<<<<< ... >>>>>>>" and type "!linediff" to tell vim to filter the lines through my ruby script.
<<<<<<< HEAD:thesis.tex
Once we are done with binary functions, we turn to unary functions, shifting our focus from the aspect weavers to the aspects themselves. Our goal is to help programmers to build aquariums containing the aspects they need, while minimizing the number of proofs needed to achieve this goal. To this end, we provide several generic proofs that create, extend, and translate aquariums with aspects of specific forms. Note, however, that not every pair of functions that commute can be shown to do so using our proofs only, so the programmers are expected to complete our collection with proofs of their own whenever the aspects they need are not of the specific forms covered by our theorems. \begin{enumerate} \item For every associative and commutative binary function, such as those created using our unordered pair strategy, we can create an aquarium of unary functions corresponding to the elements of the algebraic datatype. \item Given an aquarium containing a function $f$, the aquarium can be extended with function $f^n$, for any natural number $n$. The function $f^n$ is the function which repeatedly applies, $n$ times, the function $f$. If $f$ is invertible, the theorem extends to negative integers. ======= Once we are done with binary functions, we turn to unary functions, shifting our focus from the aspect weavers to the aspects themselves. Our goal is to help programmers to build aquariums containing the aspects they need, while minimizing the number of proofs needed to achieve this goal. To this end, we provide several generic proofs that create, extend, and translate aquariums with aspects of specific forms. Note, however, that not every pair of functions that commute can be shown to do so using our proofs only, so the programmers are expected to complete our collection with proofs of their own whenever the aspects they need are of the specific forms covered by our theorems. \begin{enumerate} \item For every associative and commutative binary function, such as those created using our unordered pair strategy, we can create an aquarium of unary functions corresponding to the elements of the algebraic datatype. \item Given an aquarium containing a function $f$, the aquarium can be extended with function $f^n$, for any natural number $n$. The function $f^n$ is the function which repeatedly applies, $n$ times in total, the function $f$. If $f$ is invertible, the theorem extends to negative integers.
>>>>>>> df2a5b6eb97ded25a34412d6ff946e0c513da6f3:thesis.tex \item If $M$ is a functor, then applying $M$ to all the members of an aquarium transforms the aquarium into a new one, while preserving the pairwise commutativity of its elements. %\item We show how parametricity \cite{free_theorems} ensures that structure-manipulating aspects cannot interfere with element-manipulating aspects, thereby reducing the programmer's remaining burden of proof. \end{enumerate}
Note that my script detects the "=======" separator and diffs between the lines appearing before and after it. It should be trivial to adapt it to examine different files, like the original diff does. Anyway, the result is that the changed words get prefixed with a "+", which I highlight using vim's ":hlsearch" option.
<<<<<<< HEAD:thesis.tex
    Once we are done with binary functions, we turn to unary functions, shifting our focus from the aspect weavers to the aspects themselves. Our goal is to help programmers to build aquariums containing the aspects they need, while minimizing the number of proofs needed to achieve this goal. To this end, we provide several generic proofs that create, extend, and translate aquariums with aspects of specific forms. Note, however, that not every pair of functions that commute can be shown to do so using our proofs only, so the programmers are expected to complete our collection with proofs of their own whenever the aspects they need are +not of the specific forms covered by our theorems.
    \begin{enumerate}
    \item For every associative and commutative binary function, such as those created using our unordered pair strategy, we can create an aquarium of unary functions corresponding to the elements of the algebraic datatype.
    \item Given an aquarium containing a function $f$, the aquarium can be extended with function $f^n$, for any natural number $n$. The function $f^n$ is the function which repeatedly applies, $n$ +times, the function $f$. If $f$ is invertible, the theorem extends to negative integers.
=======
    Once we are done with binary functions, we turn to unary functions, shifting our focus from the aspect weavers to the aspects themselves. Our goal is to help programmers to build aquariums containing the aspects they need, while minimizing the number of proofs needed to achieve this goal. To this end, we provide several generic proofs that create, extend, and translate aquariums with aspects of specific forms. Note, however, that not every pair of functions that commute can be shown to do so using our proofs only, so the programmers are expected to complete our collection with proofs of their own whenever the aspects they need are of the specific forms covered by our theorems.
    \begin{enumerate}
    \item For every associative and commutative binary function, such as those created using our unordered pair strategy, we can create an aquarium of unary functions corresponding to the elements of the algebraic datatype.
    \item Given an aquarium containing a function $f$, the aquarium can be extended with function $f^n$, for any natural number $n$. The function $f^n$ is the function which repeatedly applies, $n$ +times +in +total, the function $f$. If $f$ is invertible, the theorem extends to negative integers.
>>>>>>> df2a5b6eb97ded25a34412d6ff946e0c513da6f3:thesis.tex
    \item If $M$ is a functor, then applying $M$ to all the members of an aquarium transforms the aquarium into a new one, while preserving the pairwise commutativity of its elements.
    %\item We show how parametricity \cite{free_theorems} ensures that structure-manipulating aspects cannot interfere with element-manipulating aspects, thereby reducing the programmer's remaining burden of proof.
    \end{enumerate}
Tada! Now I know which words have changed since my last unfortunate sync-and-fix-conflicts cycle.

Sunday, September 06, 2009

Samuel's Really Straightforward Proof of the Parametricity Result, extended (trivially) to dependent types.

[I'll eventually write a version which begins by explaining free theorems, but for now here's a proof for the cognoscenti]


Consider an agda expression, any typed agda expression whose type is a Set1. Here are two examples, including one using dependent types.

id : {a : Set}
   → a
   → a
id x = x

ff : {a : Set}
   → {s : a → a}
   → (F : a → Set)
   → (f : {x : a}
        → F x
        → F (s x))
   → {x : a}
   → (y : F x)
   → F (s (s x))
ff F f y = f (f y)

It is very straightforward to obtain a term, ff₁, which has the same type except that Set has been upgraded to a Set1. In fact, the expression ff already has the desired type, we just need to change its type annotation.

id₁ : {a : Set1}
    → a
    → a
id₁ x = x

ff₁ : {a : Set1}
    → {s : a → a}
    → (F : a → Set1)
    → (f : {x : a}
         → (F x)
         → (F (s x)))
    → {x : a}
    → (y : (F x))
    → (F (s (s x)))
ff₁ F f y = f (f y)

Now, let's make this change a bit more generic. Instead of fixing Set1, let's use an abstract target, Set#. Now, since agda doesn't know that Set# is a member of the Set hierarchy, the validity of the expression (x : a) does not follow from the fact that (a : Set#), as it would for (a : Set) or (a : Set1). For this reason, it is necessary to introduce the abstract type transformer (value# : Set# -> Set1), which inserts Set# into the type hierarchy.

It is very straightforward to obtain a term, ff#, which has the same type as ff except that Set has been upgraded to a Set# and value# has been inserted at the appropriate places. In fact, the expression ff already has the desired type, we again just need to change its type annotation.

id# : {a : Set#}
    → value# a
    → value# a
id# x = x

ff# : {a : Set#}
    → {s : value# a → value# a}
    → (F : value# a → Set#)
    → (f : {x : value# a}
         → value# (F x)
         → value# (F (s x)))
    → {x : value# a}
    → (y : value# (F x))
    → value# (F (s (s x)))
ff# F f y = f (f y)

And now the punchline is that ff# is precisely the proof of the free theorem for ff, using the following instantiations for Set# and result#.

record Set# : Set1 where
  field
    a  : Set
    a' : Set
    a~ : a → a' → Set

record value# (a# : Set#) : Set where
  open Set# a#
  field
    x  : a
    x' : a'
    x~ : a~ x x'

Even more free theorems can be obtained by using other instantiations. Note that in the usual formulation of the parametricity result, the type of the free theorems are usually given in a much longer, record-free form where each field is expanded into an individual parameter. It is tedious, but straightforward to convert between the two representations.

free-id' : {a : Set}
         → {a' : Set}
         → {a~ : a → a' → Set}
         → {x  : a }
         → {x' : a'}
         → a~ x x'
         → a~ (id x) (id x')
free-id' {a} {a'} {a~} {u} {u'} u~ = value#.x~ r# where
  a# : Set#
  a# = record {a = a; a' = a'; a~ = a~}

  u# : value# a#
  u# = record {x = u; x' = u'; x~ = u~}

  r# : value# a#
  r# = u#

free-ff' : {a : Set}
         → {a' : Set}
         → {a~ : a → a'
               → Set}
         → {s : a → a }
         → {s' : a' → a'}
         → {s~ : ∀ {x x'}
               → a~ x x'
               → a~ (s x) (s' x')}
         → {F : a → Set}
         → {F' : a' → Set}
         → (F~ : ∀ {x x'}
               → a~ x x'
               → F x → F' x'
               → Set)
         → {f : ∀ {x}
              → F x
              → F (s x)}
         → {f' : ∀ {x'}
               → F' x'
               → F' (s' x')}
         → (f~ : ∀ {x x' x~}
               → {y : F x }
               → {y' : F' x'}
               → F~ x~ y y'
               → F~ (s~ x~)
                    (f y) (f' y'))
         → ∀ {u u' u~}
         → {y : F u }
         → {y' : F' u'}
         → F~ u~ y y'
         → F~ (s~ (s~ u~))
              (ff F f y) (ff F' f' y')
free-ff' {a} {a'} {a~}
         {s} {s'} {s~}
         {F} {F'} F~
         {f} {f'} f~
         {u} {u'} {u~}
         {y} {y'} y~
         = value#.x~ r# where
  a# : Set#
  a# = record {a = a; a' = a'; a~ = a~}

  s# : value# a# → value# a#
  s# x# = let open value# x# in record
        { x = s x
        ; x' = s' x'
        ; x~ = s~ x~
        }

  F# : value# a# → Set#
  F# x# = let open value# x# in record
        { a = F x
        ; a' = F' x'
        ; a~ = F~ x~
        }

  f# : {x# : value# a#}
     → value# (F# x#)
     → value# (F# (s# x#))
  f# {x#} y# = let open value# y# in record
             { x = f x
             ; x' = f' x'
             ; x~ = f~ x~
             }

  u# : value# a#
  u# = record {x = u; x' = u'; x~ = u~}

  y# : value# (F# u#)
  y# = record {x = y; x' = y'; x~ = y~}

  r# : value# (F# (s# (s# u#)))
  r# = ff# F# f# y#

Thursday, February 05, 2009

An even more careful fox

Firefox goes to great lengths to preserve the user's work. For the rare cases when it fails, read this.

If I browse for some time, opening a bazillion tabs before the computer crashes, firefox will offer to restore those tabs as soon as I start it again.

If I type some text in a <TEXTAREA/> form before the computer crashes, firefox will restore the text.

But if I type some text in a fancy editor such as WikEd, my changes will be lost. That's because the (HTML representation of the) text I've created was generated by a great many javascript function calls, and firefox doesn't know whether it's safe to simply call those functions again. Thankfully, firefox does remember the resulting (HTML representation of the) text! It's hidden in your profile's sessionstore.bak file.

~/.mozilla/firefox/*.default/sessionstore.bak

The recovery process, however, is a little bit more involved. In the case of WikEd, I searched for the title of the Wiki article I was editing, and found an innerHTML:"..." assignment soon after. That string contained all of the (HTML representation of the) text I had lost, but it was encoded using escaped hexadecimal sequences ("\xE9"), plus other javascript and HTML annoyances. I found that the easiest way to recover the pure ASCII text was to copy the innerHTML string into the following template:

<script>
document.writeln("...");
</script>

Then, I loaded the resulting html file into a separate firefox tab: the hexadecimal sequences were interpreted, and the HTML code was rendered. Copy-pasting the HTML into WikEd lost the HTML formatting but keep the ASCII text, which is exactly what I wanted. My changes were recovered! Thank you, firefox.

Saturday, January 24, 2009

Rant against charitable organizations (and solution)

I happen to be an highly optimistic person. That's a good thing.

Sometimes, my less optimistic friends think the world is a terrible place to live in. Thankfully, they're wrong, so I can cheer them up by pointing out solutions to the problems they perceive. Given this ability, I think I'd make a great volunteer at one of those teen help hotlines. The problem is, none of them wants my help! Well, none that I could find in my area, anyway.

You see, I never donate to charitable organizations. I think it's dumb to give an organization money so that someone else can help people out and get paid for it. I say, cut the middle man! Let me give you a hand instead.

And you know what they replied? "Great, we do have some volunteer positions available. Your task would be to call people and ask them for donations. Interested?"

They really don't want us concerned citizens to help. Like everybody else, they just want our money.


And of course, being the resourceful optimist that I am, I've got a solution to that. And of course, being the enthusiastic developer that I am, my solution involves building a website.

An ordinary charitable organization would use its website to tell you about its plans for solving the problems of the world, and to request your "help" (that is, your money) for implementing that plan. On my hypothetical website, I would ask you about your plan for solving the problems of the world. And I would show you the plans of the other users, so you can contact them and contribute if you think the plan is worth trying.

Most importantly, the plans would be highly detailed. Where ordinary charitable organizations would merely draw a pie chart showing how they allocate your money, our plans would tell you exactly which actions we want to see performed, and why each action contributes to (a sub-goal which contributes to a sub-goal which contributes to) resolving the issue at hand, say, "ending world hunger".

One of the reasons for using such detailed plans is to convince visitors that our plan will actually succeed. I think there is a tendency to assume that, by default, big organizations know what they are doing, and we can't compete with that bias unless we show that we know what we are doing.

And for those of us who don't know what we're doing, we can always ask for the help of our creative contributors. As a project grows, it should become more and more complete, more and more plausible, and attract more and more contributors. If it doesn't, then it probably wasn't a very good idea to begin with.

The other reason for writing highly detailed plans is to keep track of progress. At the most-detailed level, a plan should consist of concrete actions which individuals can perform. That way, resourceful visitors who are convinced by a plan will be able to contribute by performing the concrete action, and ticking it off as completed.


The idea of empowering the community by replacing big organizations with self-organizing teams of volunteers is not new; I've merely translated existing ideas from the world of software to the world of charity. What I'm promoting, it seems, could be called Open Source Charity. (or "Open Plan", perhaps?)

And what this means, is you don't even have to wait for me to implement the aforementioned website. If you have an idea that could change the world, then just use your favourite issue tracking system, and start organizing issues into a concrete plan. Easy enough, right? The world has plenty of good things as it is, like I've claimed.


Well, have fun making the world a better place. Good luck!

Friday, January 09, 2009

well-foundedness, part 2 of 2: code is data. or is it codata?

Whether it is represented as finite strings or as finite trees, code is finite, and thus code is data, not codata. That should settle the question.

haskell code = 2 + 3 * 4 haskell string_data = "2 + 3 * 4" haskell data Exp = Lit Int | Add Exp Exp | Mul Exp Exp haskell tree_data = Add (Lit 2) (Mul (Lit 3) (Lit 4))

Except, of course, that's not really the question I wanted to ask. In my very first post, I warned that manipulating code as raw strings or trees was a bit primitive, and I've since been taught an alternative: higher-order abstract syntax. For the purpose of this post, that basically means I'm representing the code using a function instead of a data-structure.


With data-structures, proofs are usually done using structural induction (see part 1). But when using a function to represent code, what could be its internal structure? What are its substructures?

The clue lies in the exponential notation for function types. But first, remember the familiar multiplicative notation for, well, product types. If (a, b, c) is a value of type A × B × C, then b would be a substructure of type B. That seems reasonable. Now, consider a function λx. f x of type A → B. The exponential notation for this type is BA = B × B × ... × B, with one occurrence of B per inhabitant of A. If these inhabitants are (a0, a1, ...), then an alternate representation of our function could be (f a0, f a1, ...). This expanded form contains exactly the same information as the lambda notation, it's just a lot more verbose, especially when A has infinitely many inhabitants.

Seeing this explicit notation, an immediate conclusion is that for any value a of the appropriate type, the (value corresponding to the) application f a is a substructure of f. Wow! It was totally unexpected for me. That's why I'm writing about it. To share my excitement. But don't get too excited yet: there's a warning coming up.


I have mildly motivated our search for substructures in functions with the relatively exciting perspective of creating a structural induction proof whose decreasing structures include functions. Well, I hope you're not that motivated, because you can't do that. Function application isn't well-founded at all, at least in some languages. Take the identity function, for example. In Haskell, it is possible to apply the identity function to itself. The resulting substructure, obviously, will be the identity function. But that substructure also has the identity function as a substructure, and by continuing to recur in this fashion, we will never reach a base case. The proof will instead go on, forever, in an infinite regress.

Uh? I hope you're surprised! How could structural induction work with all of those other kinds of substructure relations, yet fail with this one? What's so special about functions?

Let's pause to ponder the presumed absurdity of an infinitely-nested structure. Take lists, for example. They are finite because after a finite number of elements, we reach the end of the list. An infinitely-nested list would go on forever, cons after cons, never reaching an end. While this would be absurd in most programming languages, infinite lists are actually commonplace in Haskell... So maybe functions aren't so unique after all!

Functions and infinite lists are examples of codata, and induction is indeed known not to work with those. Expressions of infinite depth do not have a terminating evaluation; the evaluator can't even read the entire input! I hear we're supposed to use "coinduction" instead, but I can't comment on that technique yet. What I can say, however, is that even though Haskell allows data and codata to mix, it's apparently a bad idea, and there are languages with type systems strong enough to prevent it. In these languages, there are two distinct types for lists, but I haven't seen a distinct type for "cofunctions" yet. I suspect that a function must be codata whenever some of its possible return values are.

Well, I bet you've heard enough about well-founded and non-well-founded structures (data and codata) for your entire life. But personally, I think I'm just getting started.

well-foundedness, part 1 of 2: who cares?

If you're like me, you've often heard of well-foundedness, but never really bothered to learn what it really meant nor why it's important. If you're like most people, on the other hand, then you've never even heard the word and you couldn't care less. Well, go ahead, skip this post. You'll be back and eager to learn once you try and fail to read part 2.





...see? I told you you'd be back. Since you're presumably only interested in understanding enough about well-foundedness in order to follow part 2, I might as well use the same example: a little expression language for evaluating numerical expressions such as 2 + 3 * 4.

haskell data Exp = Lit Int | Add Exp Exp | Mul Exp Exp haskell eval :: Exp -> Int haskell eval (Lit n) = n haskell eval (Add e1 e2) = eval e1 + eval e2 haskell eval (Mul e1 e2) = eval e1 * eval e2 haskell eval (Add (Lit 2) (Mul (Lit 3) (Lit 4)))

Since there are no looping constructs in this simple language, it's reasonable to expect evaluation to always terminate. It's possible to prove so using traditional induction, say, on the height of the expression tree. Induction arguments are routine in mathematics, and thus the previous statement is usually all that is needed in order to convince another mathematician that the eval function always terminates; but since today's post is about different kinds of induction, I'll flesh out the proof so you can see the difference.

proof: by (traditional) induction on the height of the expression tree. Base case: if the tree has height one, i.e. if it is a leaf, then the expression is a literal number of the form Lit n and the evaluation terminates immediately by returning n. For the induction step, suppose eval e terminates for all expressions e of height strictly less than n. We wish to show that eval also terminates on expressions of height exactly n. There are two cases: expressions of the form Add e1 e2 and expressions of the form Mul e1 e2. In either case, e1 and e2 are subtrees of the entire expression, and thus have a strictly smaller height. By the induction hypothesis, eval e1 and eval e2 both terminate, and thus the expressions eval e1 + eval e2 and eval e1 * eval e2 also terminate (assuming Haskell's numeric primitives do). ☐

There are other versions of the above argument which are equally valid. For example, instead of the expression depth, we could use the expression size, meaning the number of constructors (Lit, Add and Mul) used to construct the expression.

haskell size :: Exp -> Int haskell size (Lit n) = 1 haskell size (Add e1 e2) = 1 + size e1 + size e2 haskell size (Mul e1 e2) = 1 + size e1 * size e2

This metric is also smaller for e1 and e2 than for Add e1 e2 and Mul e1 e2, so the induction step will succeed.


The two variants I have discussed so far use numbers (depth, size) to argue termination. The idea is that the base case proves the statement to be true when the number is one, and then the induction step can use this fact to prove that the statement is also true when the number is two. This new fact can in turn be used to prove the statement when the number is three, after which we can handle case four, then case five, and so on. In the end, we'll have a proof for all numbers, meaning that expressions of all sizes and depths have a terminating evaluation.

An alternative view of induction is to begin with a statement with a particular number, say five, about which we are actually interested. The induction step gives us a conditional proof of the statement, which depends on the statement to be true for the number four. But the statement is true for the number four, because it's true for three, because it's true for two, because it's true for one. And the statement is true for one because the base case proves so.

This second view is even a bit more "efficient" than the first, because we don't actually need to decrement so slowly. Add (Lit 2) (Mul (Lit 3) (Lit 4)), of size 5, has a terminating evaluation because Lit 2 and Mul (Lit 3) (Lit 4), of sizes 1 and 3, also terminate; the first by the base case, the second because Lit 3 and Lit 4 terminate. The last two expressions had size 1 and are also proved to terminate by the base case. Notice that we managed not to discuss expressions of size 2 and 4 at all.

Using the more efficient version, we see that the proof for n doesn't need to recur on n-1, but can actually use any m as long as m < n. We can generalize further. Even though induction traditionally uses the less-than relation of natural numbers, it is totally possible to find other suitable relations. Structural induction, for instance, says that the expression e1 is less than expression Add e1 e2 because the latter contains e1 as a sub-expression.

This structural less-than is very different from the numerical less-than. For one thing, the numerical less-than is total, meaning that given two numbers, one of the two is going to be smaller than (or equal to) the other. With structures such as Add (Lit 1) (Lit 2) and Mul (Lit 3) (Lit 4), neither is contained within the other, so the structural less-than isn't total. But while our intuitive, everyday notion of ordering seems to require totality, the notion isn't required by the induction principle.

One notion which is required, however, is (you guessed it) well-foundedness. The property basically states that when recurring on smaller and smaller values, we will hit the base case after finitely many steps. This is required: otherwise, the proof could go on and on and on without the sceptics even being convinced.

Speaking of sceptics: are you convinced that well-foundedness is a useful concept now?