Back to demo list.

Previous demo

Next demo

Demo 1. Timeouts, pauses, choices, and fixed points.

This is based on my blog entry. This one demonstrates timeouts and pauses.

The TBC code is as follows.

        loop(
            nag( ) >
            await(
                click( b1a ) && out("1A")
            ||
                click( b1b ) && out("2B")
            ||
                timeout( 2000 ) && out( "too slow" )
            ) >
            pause(2000) >
            await( click( b2 ) && out("2") )
        )
        

A subtle change from Demo 0 is the use of || to create a choice between three guarded commands.

The nag function returns a loop but not an infinite one. It is defined as follows.

        static function nag() : Process<Triv> {
            function f(repeat : Void -> Process<Triv>) : Process<Triv> { return
                await(
                    click(b0) && out("0")
                ||
                    timeout(1500) && nagTheUser() > invoke(repeat)
                ) ; }
            return fix( f ) ;
        }
        

As you can see, nag is defined with the help of the fix function. The fix function is defined so that fix(f) returns a process p such that p == f( function(){ return p ; } ) So, when the result of nag is executed, each time the repeat function is called, it returns the very same process that is the result of calling nag.

The process returned by invoke(repeat), when run, calls repeat and then executes the result. Since the result of calling repeat is the same as the result of nag, invoke(repeat) is the same process returned from nag. I.e. we have a loop.

In fact we could just invoke nag and that would eliminate the need for repeat and thus the need for fix. I.e. we could rewrite the loop as

        static function nag() : Process<Triv>{ return
            await(
                click(b0) && exec(thankTheUser)
            ||
                timeout(1500) && exec(nagTheUser) > invoke(nag)
            ) ; }
        }        

With this version of the nag function, every time nag is invoked, it reconstructs the process. Since process objects are generally immutable, this make no difference semantically, but it takes time and creates garbage. In the version of nag that uses fix, only one copy of the process is constructed.

The need to use invoke is a bit mysterious. In the version of nag that doesn't use fix, it is clear that, if we wrote nag() instead of invoke(nag), we would have an infinite loop during the construction of the process. But what about the version that uses fix? Could we replace invoke(repeat) with repeat()? The anwer turns out to be no because of the definition of fix:

    /** Create a looping process from a function.
     * The result is a process p of type Process<A> such that
     * p = f( function( t : Triv ) { return p ; } )
     * It is a precondition that f should not call its argument. **/
    public static function fix<A>( f : (Void -> Process<A>) -> Process<A> ) {
         var p : Process<A> = null ;
         function fp() {
             if( p==null )
                 return toss("TBC Error in fix. Possibly a missing invoke?") ;
             else
                 return p ; }
         p = f( fp ) ;
         return p ;
     }

You can see from the precondition of fix that its argument should not call its argument -- violating this precondition is what the use of invoke( repeat ) in place of repeat() avoids. But why the precondition? Let's see what happens if we were to replace invoke( repeat ) with repeat() in the definition of f above. Then, when nag is called, nag calls fix, which calls f passing fp as repeat. Then f would call repeat (i.e. fp); normally this would return p, but, if p is not yet initialized, this would be bad.

When we repect the precondition by using invoke(repeat), what happens is this : When nag is called, nag calls fix, which calls f passing fp as repeat, exactly as before. Then f calls invoke(repeat), which returns a process that, when run, will call repeat (i.e. fp); However this process —the one returned from invoke(repeat)— is only run later, after fix has returned and variable p has been assigned. Thus repeat returns the then current value of p, which is the same as the process returned from fix, and then that process is run. It is crucial here that the function fp and the variable p live longer than the invocation of fix that created them.

The haxe code is here.