Friday, December 10, 2010

Unsafe native functions in Frege 2

Integration of Frege and Java is easy, one just declares a native function, for example

    native indexOf :: String -> Char -> Int

This makes an expression like

    indexOf "Frege" 'g'

well typed, and the compiler generates code like


This is all very nice, but there are some potential problems with java code:

  • it can return null
  • it can throw exceptions
  • it can have side effects, including, but not limited to, performing input/output
The problem is not that java code can do such things, it is rather that one must declare it correctly to avoid compromising safety of Frege code. Frege can handle all 3 cases or combinations thereof very well:

  • if the java method returns null, one declares the return type Maybe instead just t
  • if the java method throws exceptions, one declares the return type Exception t instead just t
  • if the java method is not pure, one declares the return type IO t instead just t
The compiler generates then appropriate wrapper functions or call sequences.

In the presence of unrestricted native (i.e. java) functions, whether the Frege code will be type safe or not depends on the good will and good knowledge of the programmer. It is (currently) quite easy to write a small program that tries to cast an Int to a Bool in Frege without getting even a warning from the compiler. This is clearly 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.