How are you all? I’m having an amusing time in Scotland. Gig last Thursday seemed to go well. Interesting day. Lots of type inference going on… Gigging again in just under an hour (on dissecting containers at LFCS lab lunch) and again on Thursday (Epigram busking with the Dreamers). Chewing the fat with the St Andrews crew tomorrow. Back next week sometime; exactly when will depend on what state Edinburgh transport is in after whatever happens this weekend happens. I hope you’re all having lots of fun without me.
Archive for June, 2005
I gave a brief overview of darcs, a new revision control system written in Haskell, and the theory of patches underlying darcs. The key differences with CVS are:
- Every copy of the source tree is a repository
- Every repository is defined in terms of a series of patches
- Every patch can be inverted to recover the situation before it was applied
There are some interesting observations you can make about the algebraic structure of patches. The ‘repository states’ and patches form a category. In fact, we assume every patch is invertible, so they form a groupoid.
Given this model, it is surprisingly easy to define two key operations on patches.
- Given two patches the merge of the two patches corresponds to the pushout of and .
- Given two patches and , commuting the patches and corresponds to computing the pullback of and .
Thinking about patches in this fashion gives new results. For instance, darcs cannot commute the addition of a file and the file’s subsequent deletion. Given the categorical model, commuting two such patches becomes trivial. Unfortunately, it is not immediately clear how to ‘undo’ the commuting of a patch and its inverse. Commuting two patches can lose information about the original patches.
We were discussing partiality today. The approach I presented is joint work with Venanzio Capretta (Ottawa) and Tarmo Uuustalu (Tallinn). Have a look at the definition of the partiality monad in Haskell, you also find some examples. However, I have left out the definition of lfp (least fix point) s.t. you have some fun. An extreme programming spec of lfp is that the programs fib and fac shoiuld work, e.g.
Partial> fib 10
Partial> fact 10
I have updated Partial.lhs, the type of lfp was incorrect (because it was obtained by wrongly instantiating a more general type).
Open for business, now with and lhs2.
There are 3 categories you can post in:
- Lunches – for lunchtime discussions
- General – for extended discussions and FP related interest
- Off topic – for anything of note but not FP related