If you spend enough time around me, you will probably hear me extol the virtues of statically typed languages such as ML or Haskell. Statically typed languages are great, because they find so many bugs before you even run your program. In fact, a good friend of mine jokes about OCaml program that “If it compiles it is correct!” This is not true, of course. OCaml does not check that your algorithm’s logic is correct, for instance.

Yesterday I encountered what I would consider a “type bug” in OCaml. There was human error involved, but I was still surprised that such a bug is possible in a type-checked program.

In BAP, we have a utility function, Util.timeout, which performs a computation, and if it takes too long, aborts it and raises an exception. The timeout function has type: int -> ('a -> 'b) -> 'a -> 'b, or in plain english, takes the number of seconds, a function f to execute, and a value x such that f x is computed.

The problem we observed was that timeouts were simply not working: the code would run for a very long time. The timeout function was being called, though, and at first glance I thought it looked fine: Util.timeout 3 Asmir_disasm.vsa_at p addr vsa_at takes two arguments, so this makes some intuitive sense. But a closer look reveals that we are psssing 4 arguments to Util.timeout, and it only takes 3 — How is this possible?

The problem is that timeout is polymorphic, and the type inference engine decided that 'a = Asmir.asmprogram and 'b = Type.addr -> Cfg.AST.G.t * unit, or in plain english: we want to partially evaluate the vsa_at function on only one argument, and timeout if that takes too long. Unfortunately, partial evaluation is usually very fast. The slowdown occurs when the extra argument, addr is then consumed by this partially evaluated function. Another way of viewing this is that OCaml thinks we wanted to do (Util.timeout 3 Asmir_disasm.vsa_at p) addr.

The solution is simply to force the partial evaluation to occur earlier, i.e., Util.timeout 3 (Asmir_disasm.vsa_at p) addr. I think that such a bug should at least trigger a warning, or maybe even require explicit parenthesization in such cases to denote currying is intentionally being applied. However, the consensus at lunch was that I am wrong, and the programmer should not make such mistakes. But isn’t the point of static type checking to find dumb mistakes?