Friday, December 10, 2010

Possible solutions for problems with native functions

In my last post I described the problems that occur in the presence of native functions whose alleged properties are not checked by the compiler.

I can think of the following approaches to deal with those problems:
  1. do not allow native functions at all - clearly unacceptable
  2. all native functions must have a return type like IO (Exception (Maybe t)). This would be safe, but very troublesome. Most, if not all Frege code would be in the I/O Monad.
  3. like 2., but maintain a database of pure java methods so that the compiler  knows them and allows less restrictive return types. A nightmare.
  4. Refuse to accept native declarations that are provably wrong.
  5. Refuse to accept native declarations with potential problems, but there is a way - not necessarily an easy one! - to force the compilers to accept.
  6. Warn the programmer about potential problems, but trust him anyway and accept the native declaration.
  7. Trust the programmer no matter what.

Scenarios 1 and 3 are out of the question for obvious reasons.

Scenario 2 is the safest of all, nothing can go wrong. However, its adoption would make Frege almost unusable. One could think, however, of a "scenario 2 light" where functions defined in the Frege base libraries would be exempt from the harsh rule. But I do not like that anyway, because I know that there are many useful java functions out there. It's nonsensical to make their usability clumsy.

Scenario 4 is definitely the way to go. Often one can read from the type that the function cannot be pure. For example, a function with no arguments is either absolutely trivial or it cannot be pure: unless it computes the same result all the time it uses global state or does input. One example is System.nanoTime().

Likewise, a void function is either absolutely trivial like
     public void doNothingUseful() { return; }
or it exists to encapsulate side effects like setting a field in an object or printing a newline on the screen. In either case, it is wise to demand that such a  function lives in the IO Monad.
A side note: when talking about such matters, it must be understood that due to the architecture of Java and the JVM, it'll never be possible to prevent abuse or to guarantee safe execution. For example, one can always deliberately fool the type system by replacing or modifying class files. With "fool the type system" I mean that run time errors are made possible that the type system promised to prevent - such as calling a method with the wrong number of arguments or with arguments of wrong type. 
But while this is especially easy in Java (yes, there is a reason why there are a dozens of java "build-tools" out there!) it is nothing that could not be done for other type safe languages. 
Unfortunately, not all impure functions are that easy to spot. I will devote another post to the question how one could extend the knowledge about a java functions behaviour a bit.
Scenario 5 and 6 also assume that such knowledge exists.

Scenario 7 is what is currently done in Frege2. I already explained why this is unacceptable.

No comments:

Post a Comment

Comments will be censored by me as I see fit, most likely if they contain insults or propaganda for ideologies I do not like. Comments that are on topic will not be censored. If I leave a comment uncensored this does not imply that I agree with the opinions expressed therein.