Lambda the Ultimate

- concurrent futures which represent the result of a thread

- lazy futures which execute the expression on demand when requested

- promised futures which can be fulfilled explicitly.

Promised future somewhat resemble logic variables from prolog, but the interface is made explicit.

The actual interface is:

signature PROMISE =
    sig
        type 'a promise
        type 'a t = 'a promise
        exception Promise
        val promise : unit -> 'a promise
        val future :  'a promise -> 'a
        val fulfill : 'a promise * 'a -> unit
        val fail :    'a promise * exn -> unit
    end

They are for example used in alice to implement locks:

  
 structure Lock :>
    sig
        type lock
        type t = lock
        val lock : unit -> lock
        val sync : lock -> ('a -> 'b) -> ('a -> 'b)
    end
    =
    struct
        type lock = unit ref
        type t = lock
        fun lock () = ref ()
        fun sync lock f x =
            let
                val p = Promise.promise ()
                val u = Ref.exchange (lock, Promise.future p)
                val _ = Future.await u
                val y = f x handle e => (Promise.fulfill (p, ()); raise e)
            in
                Promise.fulfill (p, ()); y
            end
    end

A future will have one value at some (future) time in the computation, and it will retain that value from that time forward.

Whereas in Prolog, a logic variable will have zero or more values over time, based on the truth of the expression that contains the variable and the database used to unify values to logic variables in that expression.

A Prolog variable has zero or one value: you can't unify two values (ground terms) unless they're equal.

From my reading of the tour, Alice does have lazy expressions like that (only with implicit forcing, as Benedikt Grundmann pointed out) -- but futures are not quite the same thing. You can fulfill the future at any time, including concurrently. You can `fail' the future with an exception to indicate failure. And trying to implicitly force an unfulfilled future blocks the current thread.

This is almost the same as E's promises -- trying to force an unresolved promise in E raises an exception instead of blocking, since E has event-loop concurrency instead of threads. E has a 'when-catch' construct to wait for a reference to become more resolved. (I like E's terminology here better than Alice's: you resolve or clobber a promise instead of fulfilling or failing a future.) Note that you can resolve a promise with another promise, like unifying two logic variables.

The earliest I've heard of this general idea was Arvind's I-structures, I think...

val a = Array.tabulate (1000, fn i => spawn ... some big computation...)
val sum = Array.foldl op+ 0 a