Qi is completely type inferring, so it proves the type correctness of the code at compile time from a minimum number of declarations, like the ML family of languages.
However, as this is optional, it can also be switched off in places to handle code that the type system can not prove correct.
To make a similar system work, you'd have to label the inputs and return type of each function, and enforce the consistency of this, all at compile time. There is a complete prolog system buried in QI allowing the types to self reference and be turing complete in terms of complexity.
Having said that, the whole of QI is only meant to be 4k lines of common lisp and under an MIT license, so it'd be quite easy to port the interesting bits of it once the core of arc has stabilised.
pg, I was referring to Jekyll's explanation of optional typing. The 'maybe' means that I don't know the value in it, I've just heard that some people like it.
