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.
I ended up spending this weekend learning a lot about topos theory. Why? I have no idea. But for whatever reason, this happened. Like many areas of category theory, the biggest hurdle is figuring out the terminology— in particular, figuring out what terminology you actually need to know now vs the terminology you can put off learning until later.
So, with that in mind, I threw together a quick sketch of topos/logos theory. I should emphasize that this is only a very quick sketch. It shows when one kind of category is also another kind of category, but for the most part it doesn't say what the additional characteristics of the subkind are (unlike in my other terminology maps). One major thing missing from this sketch is a notation for when one kind of category is exactly the intersection of two other kinds (e.g., a pretopos is precisely an extensive exact category). Once I figure out how to show that in PSTricks, I'll post a new version. As before, the dashed lines indicate things you get for free (e.g., every pretopos is coherent for free). The dotted line from Heyting categories to well-powered geometric categories is meant to indicate that, technically, all WPG categories are also Heyting categories, but the Heyting structure is not preserved by geometric functors and therefore should not be "relied on" when reasoning about WPG categories as a whole. And finally, the table at the bottom shows what operators exist in the internal logic of these various categories, as well as what structure the subobject posets have.
Despite being far less polished than my other maps, hopefully it'll give you enough to go on so that you can read through the pages at n-lab in the correct order.
 For the arcs which are explained, the following abbreviations are used: "So.C." = subobject classifier; "AMC" = axiom of multiple choice; "NNO" = natural numbers object.; "LCCC" = locally cartesian closed.
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?
Full-time position available: computer scientist to create data types for scientific computing, in Haskell. Location: anywhere (telecommute).
We need a functional programming expert (Haskell preferred) with a deep knowledge of type theory and theorem proving. You should have an understanding of applied mathematics, physics, or engineering -- including continuous & discrete dynamical systems, ODEs and PDEs, and the basics of computer simulations for scientific problems.
This is a full-time position, initially as a contractor (with full pay) and with a significant chance of a long-term offer. You may be located anywhere, and must be comfortable working by Internet with an English-speaking team based in the western USA.
Key task: to find the right (probably high order) types to enable functional programs to be built to simulate scientific systems. This is a senior position working with a senior team. If you are the right person, please PM me, or email me at email@example.com.
Thanks.submitted by FPguy
[link] [12 comments]
I'm trying to get a handle on using the n-Dimensional vectors from ekmett's linear library. I can't figure out how to do anything with them. For instance, I'd like to know how to, given some 'V n a', produce or operate on a 'V n (V (n-1) a)', an n-sized collection of vectors in (n-1) space.
So far, V seems like a black box type. Is there class behavior that I'm missing that would allow me to do interesting things with it?submitted by resrvsgate
[link] [4 comments]
There is increasing interest in integrating dynamically and statically typed programming languages, as witnessed in industry by the development of the languages TypeScript and Dart, and in academia by the development of the theories of gradual types, hybrid types, and the blame calculus. The purpose of our project is to bring the academic and industrial developments together, applying theory to improve practice.
The successful candidate will join the ABCD team, carrying out a research programme investigating sesion types and web programming. The project is jointly supervised by Andrew Gordon of Microsoft Research Cambridge and the University of Edinburgh.
You should possess an undergraduate degree in a relevant area, or being nearing completion of same, or have comparable experience. You should have evidence of ability to undertake research and communicate well. You should have a background in programming languages, including type systems, and programming and software engineering skills.
We seek applicants at an international level of excellence. The School of Informatics at Edinburgh is among the strongest in the world, and Edinburgh is known as a cultural centre providing a high quality of life.
The successful candidate will receive a studentship covering tuition and subsistence. Students from the UK or EU are preferred. Consult the University of Edinburgh website for details of how to apply.
If you are interested, please send an outline of your qualifications to: Prof. Philip Wadler (firstname.lastname@example.org).