(no subject)

[pozorvlak]

Here's something I've been wondering about for ages. When I'm programming, I find worrying about the types of variables to be generally unhelpful, and being forced to think about such things by the compiler is downright irritating. Yet when I'm doing mathematics, I think type-centrically all the time. The two activities are strongly connected in my mind, so it's surprising to me that there's this difference.

Here are some theories I've been kicking around:

• Mathematics is not, in general, testable, whereas code is. Since I can't test my proofs, I have to look for invariants and sanity checks, and types fit the bill here. But my life would be so much easier sometimes if I could run my proofs through a debugger...
  
  By the way, that's why I'm suspicious of the notion of proving code correct: I simply don't trust my proofs enough, because I can't test them. I've been known to make exactly the same error in a piece of code and in the "proof" of its correctness, an error that was picked up trivially in testing.


• In category theory, it's often the case that there is exactly one object of a given type. For instance, let T be a monad: then there's exactly one natural transformation made up of ηs and μs (that's returns and joins to the Haskellers) from Tⁿ to T. Or for a simpler example, think about sets and cartesian products: if A is a set, then A x {*} is isomorphic to A, via the map (a,*) → a, and {*} x A is also isomorphic to A via (*,a) → a. If X and Y are sets, then X x Y is isomorphic to Y x X, via the map (x,y) → (y,x). So we have two isomorphisms from A x {*} to A: either throw away the * on the right immediately, or switch the components round and throw away the * on the left. But these two maps are actually the same function.
  
  This kind of thing happens all the time in category theory (in a sense, finding out how often it happens is the point of my PhD), and the net effect is that you can often work by working out what type you need something to have, and then picking the unique thing which has that type. But (I submit) this doesn't often happen in non-categorical mathematics, and certainly doesn't happen much in programming.


• The programs I write are all too trivial for typeful programming to be very useful, or worth the extra effort. Conversely, the maths I do is often hard, so typeful thinking shows its benefits.


• Because it's all happening in my head, I'm free to pick (without extra effort) the notion of "type" that's most useful for the problem at hand. Here's an example.
  
  Last week, I was helping one of my high-school students with some basic statistics. The problem was something on the lines of "The mass of the contents of a can of beans is normally distributed, with mean 505g. 10% of cans contain less than 500g of beans. What is the standard deviation?". Now, the probability that a normally-distributed variable X is less than some value x is determined by working out how many standard deviations x is above the mean of X: the students are provided with tables which allow them to look up these probabilities given the number of standard deviations (written z). Or, as here, given a probability, to look up the number of standard deviations: then the size of the standard deviation is given by dividing 5g by the relevant value of z. Unfortunately, my student kept writing down nonsensical expressions, asking for the probability that the number of standard deviations was less than the probability of something else. "That doesn't make sense!" I kept saying, "that's a probability, and that's a number of standard deviations...". It didn't help that almost all the numbers concerned were real numbers in the range 0 to 1, so it was easier to get confused - is 0.6781 a number of standard deviations, or a probability? Not easy to tell just by looking at it.
  
  I suppose in Haskell one could do something like (untested):

  newtype Prob = Prob Float deriving (Eq, Ord, Show, Num)
  newtype StdDevs = StdDevs Float deriving (Eq, Ord, Show, Num)
  newtype Milligrams = Mg Float deriving (Eq, Ord, Show, Num)
  
  phi :: StdDevs -> Prob
  -- Probability that X is less than z standard deviations above the mean
  -- implementation left as exercise :-)
  
  invPhi :: Prob -> StdDevs   -- inverse to phi
  -- likewise an exercise :-)
  
  zify :: Mg -> Mg -> Mg
  -- number of std devs a given value is above the mean
  zify (Mg mean) (Mg stddev) (Mg x) = StdDevs $ (x - mean)/stddev 
  
  probLessThan :: Mg -> Mg -> Mg -> Prob
  -- probability a random var will be less than given value x
  probLessThan mean stdDev x = phi $ zify mean stdDev x
  
  times :: StdDevs -> Mg -> Mg
  times (StdDevs z) -> (Mg m) -> Mg (z * m)
  
  stdDevsGivenProb :: Mg -> Mg -> Prob
  stdDevsGivenProb (Mg mean) (Mg x) p = Mg $ (invPhi p) `times` (x - mean)

  Now, that would stop you making the kinds of mistakes that my student kept making, but you've had to write a fair bit of extra code there and spend extra time and effort just marshalling the types - in particular, I've had to write the basically unnecessary functions zify and times. I don't know if it's possible to derive all those typeclasses with newtypes: I'll just note in passing that if it isn't, the amount of unnecessary boilerplate code in the program becomes considerably greater.
  
  Now, the kind of "Is it a string? Is it a double?" type-checking that most people think of would be precisely no use here. The higher-level kind of typechecking that I tend to do in mathematical proofs would. It's good that it's possible to get the Haskell type system to work on this level, but it's annoying that it takes so much work (and all too often, it takes Oleg-like levels of wizardry to express the invariants I want to use). I suspect that (owing to my experience with mathematics and with dynamic languages), I'm naturally thinking of the higher-level sorts of types, to the extent that I ignore the lower-level sort (something type-coercive languages like Perl encourage you to do). Consequently, I don't need higher-level typechecking so much (because I'm doing it myself subconsciously), and my lack of lower-level checking keeps tripping me up.
  
  
  Of course, there are probably benefits that would come from handing off my high-level typechecking to a machine, which would do it more reliably than me :-)

By the way, remember a while ago when I was musing on the possibility of static duck-typed languages? Well, it seems that Scala is one :-)

Comments

[metamoof.livejournal.com]

I suppose it's an interesting problem, why you do it in one case and not another.

One type of testing I've been known to do in some of my code is generic runtime constraint checking, something that I've not seen enough of out there.

For example, after much suffering in one of my web scraping prgorams (unfortunately not open source) I ended up writing a URI object to pass around to avoid me having too many issues with transformations and so on being applied to it.

Up til that point, I was basically passing the URI around as an 8-bit string, and having to deal with unicode was the straw that broke the camel's back. Yes, it's strange having to think of unicode-compliant URLs, but believe me, it happened on a badly coded spanish site that insisted in using accented characters in at least two different encoding formats for no readily apparent reason in their URL scheme.

Anyway, by refactoring my entire codebase to pass around URI objects (which handily inherited from str, and thus broke almost no code at all) I suddenly found that I could consistently test the URI for well-formedness before throwing it out to some other unsuspecting part of my code that had no idea where the URI came from, and I actually ended up catching a bunch of errors I didn't even know exsted just by doing that. I started adding more tests in the constructor, for validity, applicability to the task at hand (e.g. that it belonged to a bunch of domains, that it was accesible from the current computer), and so on, and attempting to correct the most common egregious cases, as well as adding switches for some of the less common ones, such as, on one memorable occasion, removing the string "C:\Documents and Settings\Administrador\Mis Documentos\La puta web de los cojones\html/" from the start of the string.

At one point I realised that what I was effectively doing was type checking, though admittedly it was a heck of a lot more concrete than just "is it something of a URI type?". Also, it was voluntary, rather than enforced, as this is python, and the URI quacked like a string. That is, until I started adding convenience methods, to it, at least. And, strangely enoguh for me, it was runtime checking, rather than unit testing, though I did get confident enough in my code at one point to put most of the tests in assert statements that could be optimised out in production.

Anyway, as a python advocate, I'm definitely against static type checking, as mostly static language programmers rely on them too much, but there are times when I do do it myself, and in a much more exacting manner than I would in Java or C. So sometimes type checking helps, and there is a blurry line between what you can consired type checking or not, or for tht matter, testing, or not.

There was a point to all this beyond just common, or uncommon, programming practice, but right now, it's escaped me.

I suppose as a supplementary question, when debugging your mathematics, would this sort of automatic, sporadic, and very specific kind of type checking on the critical path be more useful, and something you could program up to help you?

[pozorvlak.livejournal.com]

Sweet! I especially like the idea of inheriting from String to reduce the impact on the rest of your code.