(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

[necaris.livejournal.com]

Oooh, that sounds *fascinating*...