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
- if the java method returns null, one declares the return type Maybe t 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
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.