(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

[fanf]

Djinn generates a Haskell function given its type. http://lambda-the-ultimate.org/node/1178

[pozorvlak.livejournal.com]

Oh yes, I'm aware of that :-) But such a function will not in general be unique, which makes it considerably less useful. I wasn't aware of the connection to the Yoneda Lemma, though - that requires some thought.

[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.

[totherme.livejournal.com]

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.

I might be missing the point, but I'm afraid I don't see anything particularly high level in those types... Here's an attempt at a sketch of a roughly equivalent set of objects in the much maligned (presumably not very high level) java type system:

public class Table {
        // Implementation provided by examiner
        public static Prob phi(StdDevs key) { ... }
        public static StdDevs invPhi(Prob key) { ... }
}

public class Prob {
        private final float val;
}

public class StdDevs {
        private final float val;

        public StdDevs(val) { this.val = val; }

        public Mg times(float f) { return new Mg(val * f); }

}

public class Mg {
        private final float val;

        public float zify(Mg mean, Mg stddev) {
                return new StdDevs((val - mean.val)/stddev.val);

        }

        public Prob probLessThan(Mg mean, Mg stddev) {
                return Table.phi(zify(mean, stddev));
        }

        public Mg stdDevsGivenProb(Mg mean, Prob p) {
                return new Mg(Table.invPhi(p).times(val-mean.val));
        }
}

I've resisted the temptation to turn the mean and stddev into static variables in Mg (which might be a more OO way of seeing things). As a result, there's more boiler plate than there needs to be (and there's always going to be more boiler plate in a state-free java program than in the haskell equivalent), but the types check just as well here as they do in ghc. I didn't even need to use generics.

I've seen some of the genuinely weird virtually-impossible-to-express type problems you've come across before, but at the moment it looks to me like this case actually is a job for "is it a string? Is it a double? Is it a probability?" simple type checking.

Am I missing something?

[pozorvlak.livejournal.com]

Well, I meant "high-level" in the sense of "closer to my mental representation of the problem, as opposed to the computer's representation of the problem as a bunch of bits". It so happens in this case that my mental representation of the types concerned can be implemented without using especially advanced type-system features.

Here's the thing. In untyped languages (like, er, BCPL), you can treat a variable containing an integer as if it were a character, or a pointer: if you do this and are less clever than you think you are, Bad Things happen. There are two ways to address this: either scan your program at compile-time, eliminating all such problematic usages, or track types at run-time, and perform error-correction when necessary. Both of these strategies eliminate the problem completely (though possibly introduce less severe problems as side-effects). This kind of thing is what I'm calling "low-level" typechecking: preventing problems that arise from misusing the computer's representations of data.

At the other end of the scale, we have something more interesting, and that's what I've called "high-level" typechecking: encoding your understanding of the "types" concerned into your program, and reasoning about correctness (automatically, or in your head) using this information.

So that's what I was talking about :-)

Now, in the normal distribution example, I wouldn't have needed to reason typefully if I were doing it myself - it's simple/well-known enough that I'd have just written down the right expressions. If anything, I'd have had a picture of a bell curve in my head and reasoned geometrically. But it was interesting that my student was making errors that could be caught by (high-level) type-checking, and perhaps more interesting that that was the first way that occurred to me to show to him why he was wrong! :-)

This is related to your point 1: in a problem like this, where we have only three types and not much code to write, the effort of coding up the necessary typechecks probably isn't worth it. Similarly, in your average short system-administration script, your high-level types might be "filename", "directory", "md5 hash", and "map of filenames to hashes" (represented as strings, strings, strings, and string to string hashes): simple enough to keep everything in your head. But if you additionally have to worry about the low-level types, you have to think about eight types at once, which is getting a bit more uncomfortable.

[totherme.livejournal.com]

I think your last two points are important. I'll paraphrase and enumerate:

1. If something's too trivial, types are less obviously useful. As things get hard, types show benefits


2. With Maths "I'm free to pick (without extra effort) the notion of 'type' that's most useful for the problem at hand."

I think these are related. If you're writing a URI processor, you might be thinking in terms of email types, web types, telnet types, etc. An overly simple compiler might force you into the uniformity of the "String" type. That makes the compiler's idea types pretty useless. There are (at least) two easy ways to change the world to make types useful:

1. Make the program requirements bigger. If you have to deal with complex numbers as well as URIs, (and if the compiler can tell the difference), maybe types might start to be useful again.


2. Make the compiler better. By which I mean, "make the type system closer to the one in your head". Maybe you could have functions parse :: String -> [Email + Web + Telnet], and (filter isWeb) :: [Web + X for all X] -> [Web] (I've used "+" as type union here)

Almost the inverse of (2) is learning to encode whatever you're thinking into the type system of a language you know well.

I'm afraid I'm about to waffle a bit - I'll come back to (1) and (2) at the end, but I need to be clear about what I think a type is first:

I claim that all programmers have "types" in their head when they're programming. I don't claim that all programmers have "haskell types" in their head. I believe that in modern computer science, the definition of "static type" is "any property that can be known about piece of code without running it". Examples include:

• "Will this code ever segfault?"


• "Will this code ever try to divide by 0?"


• "Will a malformed URL ever be passed into the http library?"


• "Can there ever be information leakage of any kind from any of the variables marked 'high security' into any of the variables marked 'low security'?"

Some types can be checked by some compilers, while others can't (compilers do exist that can statically check each of the above statements). If there's something you want to know (presuming that it can be known - see the halting problem) about your code that can't be checked, I believe that to be the fault of the compiler. Given two otherwise identical compilers, where one can statically check if my code will ever segfault and the other cannot, I'll choose the first one. The problem is that they're rarely "otherwise identical", so we come to making engineering compromises. What information can the compiler give you? How valuable is that information? What freedom do you lose in exchange for that information? How valuable is that freedom?

Hold that thought for a moment - I'll come back to it in the next comment...

[totherme.livejournal.com]

What does it mean to "understand a program"? It means that you know a certain important set of static properties of the program. You might know that the program never tries to connect to port 80 of the mail server given by the domain of an email address. It might be that you know that because you checked every branch of the code in your head, or because you did some more abstract reasoning about sets of branches in your head, or because you encoded that property into a type system against which the program checks.

I don't think good programmers tend to check every branch in their heads. I think they fit bigger programs into their heads by abstracting away a lot of that fine detail. I propose that if the abstraction they're using matches the one the type system is based on, then the compiler won't take away any freedom of expression that they were going to actually use. If you weren't going to use the freedom that you lose, then its value is 0. So the gain from the type system is worth it.

This is pretty common in folk that have spent a lot of time programming in static languages. It can appear rare in folk who have spent most of time coding in dynamic languages. It's hard to measure though, because even when their internal abstractions match up, they usually don't know what buttons they need to push in order for their natural abstractions to be supported by the language.

Put another way: I think you have the best type system in the world in your head. It can change to suit the problem you're dealing with at any given time, and it can take empirical data from test runs into account when it's constructing the probability that a given property holds. But it's fallible. Particularly as code gets big, and as the number of <1 probabilities to multiply together gets big. The type system in your compiler is effectively infallible, but not nearly as flexible and totally blind to test data. When the two sets of abstractions match up, you can let the compiler take a lot of the strain.

I think it'd be a good thing to make the type systems in compilers better, so that when a good programmer has a good abstraction in his head, the compiler can match it.

I also think that most programmers can benefit from training their internal type checkers with new abstractions. It means you can understand, and therefore write, more programs. Possibly more elegantly.

(Of course, there's an engineering compromise here too. Neither the compiler nor the programmer will benefit from complex number types if all the programs in the world are string-munging programs.)

[totherme.livejournal.com]

This started off with points (1) and (2) - code size and abstraction matching. I've said I think they're related, and I've talked about why I think compilers need more abstractions that better match with people, and why people need more abstractions in general (possibly inspired by existing compiler abstractions). Notice about (1) that if the program is truely trivial, then it's decidable, so everything about it can be known statically. You can even think of it as its own type :) As soon as the program becomes undecidable, I claim that understanding the program is equivalent to knowing the program's type in some ideal type system for that problem.

At POPL last week, there was a neat paper that ties together (1) and (2) quite nicely. The Design and Implementation of Typed Scheme. These guys were working with PLT Scheme, which is an untyped lisp dialect designed and used as a scripting language. They found that they could design a type system which would type check the vast majority of real (bug free) programs written in their community. It's quite neat - you can type up a module at a time. As data crosses the module boundary, it's checked dynamically. All the internals are statically checked. If you type check two modules that talk to each other, the dynamic checks between them aren't necessary any more. So, a 100% dynamic program performs the same as a 100% static program (there's no static performance optimisation yet). A hybrid program has a slight slowdown because of the dynamic checks at the boundaries, but it's not a lot.

They were motivated by (1) (they had a problem of maintainability as things scaled up, which they wanted to solve with explicit typing) and they were constrained by (2) (their type abstraction had to match real code written by real dynamic programmers).

In their talk, they mentioned investigating applying these techniques to ruby, python, etc in future work. Pretty exciting stuff.

[necaris.livejournal.com]

Oooh, that sounds *fascinating*...

[pozorvlak.livejournal.com]

Cool!

I saw a paper a while ago, with the title First-class macros have types (http://citeseer.ist.psu.edu/bawden00firstclass.html), also about typeful Scheme...

[pozorvlak.livejournal.com]

I think we're largely in agreement :-)

[(Anonymous)]

times (StdDevs z) -> (Mg m) -> Mg (z * m)

Of course you mean:

times (StdDevs z) (Mg m) = Mg (z * m)

I don't know if it's possible to derive all those typeclasses with newtypes (...)

GHC has a "cunning newtype deriving" (http://www.haskell.org/ghc/docs/latest/html/users_guide/deriving.html#newtype-deriving) extension that allows you to do exactly that (-XGeneralizedNewtypeDeriving). I was astonished the first time I saw "deriving (Functor, Monad)" :)

[pozorvlak.livejournal.com]

Er, yes, well spotted :-)