Thursday, February 9, 2012

Using mutable java types and non-pure methods

For those of my high esteemed readers who suffer from the not yet completed chapter 6 of the Frege language reference that is supposed to explain the native interface, I'll give a small example program today that makes use of a supposedly mutable java type and some impure java methods.

The program prints the current date and time to the standard output every other second and runs until terminated through external means.

    This program displays the
    current time on stdandard output
    every other second.
module examples.CommandLineClock where

data Date s = native java.util.Date where
    native new :: () -> ST s (Date s)           -- new Date()
    native toString :: Date s -> ST s String    -- d.toString()

This data declaration introduces the java class java.util.Date as abstract data type for Frege under the name Date. Objects of this class are mutable, hence we will use this type in the ST monad (or in the IO monad, which is just a special ST monad). We want to employ the safety the ST monad gives us, hence Date is indexed by a phantom type s that will always match that of the ST action.

Because Date is an abstract data type, we can't do anything with it unless we have functions that take or return values of that type. It is natural (but not required) to define such functions in the body of the data declaration.
Unsurprisingly, the functions we provide for Date are themselves native ones, or, in other words, they are java methods. We merely inform the Frege compiler about their existence and  at what type we want to use them.
The function will be an ST action that calls the parameter-less constructor of the java.util.Date class and gives us Date values to work with. The java constructor will initialize the Date value with the current time.
The Date.toString function will be an ST action that calls the toString method of a Date value.

It may not be obvious, but the types of the Date functions and the properties of the ST monad will make it impossible to do anything malicious with Date values. It will not be possible, for instance, to run a ST action, obtain a Date value, keep it around in pure data structures and pass it later to another, totally unrelated ST action. (To understand why, you'll want to read the paper Lazy Functional State Threads, for now, take my word for it.)

We are now in a position to write an ST action that computes the current time as a string, where "current" means the time when the action is actually performed:
--- 'ST' action to give us the current time as 'String'
current :: ST s String      -- works also in the IO monad
current = do
    d <- ()

We said our program will print the current time every other second, but this is just another way to say it will do nothing 99.999% of the time. It's actually quite hard for a computer program to do nothing (even for a lazy one), but to our luck we have the whole Java API at our disposal. For example, in the class java.lang.Thread, we find the following method:

public static void sleep(long millis)
                  throws InterruptedException

The corresponding java documentation states:
Causes the currently executing thread to sleep (temporarily cease execution) for the specified number of milliseconds, subject to the precision and accuracy of system timers and schedulers. The thread does not lose ownership of any monitors.
millis - the length of time to sleep in milliseconds
IllegalArgumentException - if the value of millis is negative
InterruptedException - if any thread has interrupted the current thread. The interrupted status of the current thread is cleared when this exception is thrown.
The only problem left is to make this function known to Frege in an appropriate way, and this means to translate the method signature to a sensible Frege type.
The java type long maps to Long, and void to (), but we must also take care of the possible exception.
In addition, it is obvious that this is not going to be a pure function!
    Encoded in Frege:
    - argument type  long   Long
    - result         void   ()
    - throws ...            Exception ()
    - does IO               IO (Exception ()) 
native sleep java.lang.Thread.sleep :: Long -> IO (Exception ())

The native declaration above in plain English: When n is of type Long, sleep n will be an IO action that, when executed, calls the java method java.lang.Thread.sleep with the argument n, catches any exception that my happen and returns a value of type Exception (). (Since we're ignoring the returned value, we'll not deal with Exception today.)

Now that we have everything we need, the main action couldn't be easier:
main args = 
    forever do
        current >>= print
        print "\r"
        sleep 999L

Try it out, it works!

The alert reader will have noticed, that the type of is actually wrong. The idea is, that an ST action may employ impure operations, as long as the overall result is pure and referentially transparent. Specifically, if a is a ST action, then a

should be a pure value. This is unfortunately not the case for our current

because its value depends on the time of evaluation.
The cause of this is that we erred about the type of
Because its underlying Java code somehow accesses the timer, it is an IO action in reality.
Hence we must write:
native new :: () -> IO (Date RealWorld)

We also need to change
current :: IO String

While it makes no difference in our small program, it teaches us a lesson of how scrupulous one must be with the types of native functions! If, for example, the semantics of the java constructor was to initialize the object with some fixed time value, then the given type was correct.

The (corrected) code can be found, along with other example code on the project source page.

1 comment:

  1. Note that the rules for native data have meanwhile changed a bit and, the corresponding chapter in the language reference is up to date.


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.