Reading a couple things pointed me to the other day; A Dependent Type Theory with Names and Binding by Schöpp and Stark, and some slides of Swierstra's about version control. Turns out Darcs is a relatively principled VCS.

My categorical intuition tells me that most of what is going on there is really a category C whose objects are pieces of data, whose arrows are patches, equipped with a functor to a group G which is the "names" of those patches. That is, when I have a square
```     v
A  / \  B
/   \
v     v
\   /
B  \ / A
v
```

Clearly the two copies of A (resp. two copies of B) are not the *same* change, but they have the same intention. The idea would be that the functor maps these down to the same group element.

was talking to me for a bit about his attacking of separation logic with a labelled sequent calculus. Funny how (I → I) * A does entail (I → I) ^ A in that system, but (apparently) not in bunched logic. His axiomatization of the nontrival equality theory that involves hypothetical equalities doesn't permit the unificationesque decompositions that would allow you to infer a * b = a * c |- b * c, but I can't come up with a raw proposition that would lead to such an equational test.
Tags:
• #### (no subject)

Oh jeez Boulet, this is what you casually slap together for a 24-hour comic? Come on, now, you're just showing off. (But seriously it is so cute)

• #### (no subject)

I really liked this multiple choice test full of nonsense words that was solveable only on the basis of metagaming the questions. This is not…

• #### (no subject)

So Donald Barthelme apparently is back from the dead and writing craigslist missed connections: http://newyork.craigslist.org/brk/mis/3985247459.html

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic