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
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
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,
then consumed by this partially evaluated function. Another way of
viewing this is that OCaml thinks we wanted to do
Asmir_disasm.vsa_at p) addr.
The solution is simply to force the partial evaluation to occur
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?