Linear Lazy Evaluation

The feature of linear lazy evaluation, which is considerably advanced, addresses the issue of freeing up resources held by a lazy value (that is, a thunk representing a delayed computation). Let us first see a concrete example involving the issue. In prelude/SATS/file.sats the following function char_stream_make_file is declared:

// making a lazy char stream out of a file handle
fun char_stream_make_file (fil: FILEref):<1,~ref> stream (char)

Note that the syntax <1,~ref> indicates that the function may have all kinds of effects except ref. As suggested by its type, the function char_stream_make_file turns a file handle into a (lazy) stream of characters. We give an implementation of this function as follows:

implement char_stream_make_file (fil) = let
  val c = fgetc0_err (fil)
in
  if c <> EOF then let
    val c = char_of_int (c)
  in
    $delay (stream_cons (c, char_stream_make_file fil))
  end else begin
    let val () = fclose0_exn (fil) in $delay (stream_nil ()) end
  end // end of [if]
end // end of [char_stream_make_file]

Clearly, there is an opened file handle inside each character stream formed by calling char_stream_make_file until all the characters in the file are put into the stream. If such a character stream is discarded during evaluation, then the file handle inside it may be left unclosed indefinitely. This can cause a serious problem in a situation where a large number of character streams need to be formed by calling char_stream_make_file. In general, the inability (or the lack of the ability) to directly free the resources held by lazy values often makes it rather difficult or even infeasible to employ lazy evaluation in a setting that requires great precision in resource management.

A Direct Approach to Freeing Resources inside Lazy Values

The following function char_stream_vt_make_file is also declared in prelude/SATS/file.sats:

// making a linear lazy char stream out of a file handle
fun char_stream_vt_make_file {m:file_mode} {l:addr}
  (pf_mod: file_mode_lte (m, r), pf_fil: FILE m @ l | p_fil: ptr l)
  :<1,~ref> stream_vt (char)

As suggested by its type, the function char_stream_vt_make_file turns a file handle into a linear stream of characters. An implementation of this function is given as follows:

implement char_stream_vt_make_file (pf_mod, pf_fil | p_fil) = let
  val c = fgetc1_err (pf_mod | !p_fil)
in
  if c >= 0 then let // c <> EOF
    val c = char_of_int (c)
  in
    $ldelay (
      stream_vt_cons (c, char_stream_vt_make_file (pf_mod, pf_fil | p_fil))
    , fclose1_exn (pf_fil | p_fil)
    ) // end of [$ldelay]
  end else let
    val () = fclose1_exn (pf_fil | p_fil) in $ldelay (stream_vt_nil ())
  end // end of [if]
end // end of [char_stream_vt_make_file]

The keyword $ldelay is used to form a linear lazy value. Given two dynamic expressions exp1 and exp2, the linear lazy value $ldelay (exp1, exp2) essentially contains two thunks whose bodies are exp1 and exp2, repectively. The first thunk represents a suspended computation while the second thunk represents a finalizer that can be called to free up the resources held in the first thunk. In the case where exp2 is missing, exp1 is assumed to hold no resources.

The code used for illustration is available here.