Is there a way to indicate that a type isn't safe to escape a callback?


#1

There are fairly common cases where you want to destroy a resource immediately and not wait for the next GC:

  • Closing files / sockets
  • Closing transactions
  • Releasing resources back to their pool
  • Other resources like prepared statements

For Pgx, we’re trying to make our interface guarantee that you can’t use it wrong unless you use a ref to capture something returned by a callback, i.e.:

let db = ref None in
Pgx_async.with_conn (fun db ->
  return (db := Some db))
>>| fun () ->
Pgx_async.execute db "SELECT 1" (* this will break obviously *)

What I’m wondering is if there’s any way to express this in the type system? In general, it’s perfectly safe to save callback params as refs (i.e. when using List.iter), but this does seem like a common thing, and being impossible would be better than “hopefully pretty obvious that this is wrong”.


#2

If you require the function argument be polymorphic in the type you wish to prevent escaping, then it should be impossible to stash it in a ref that outlives the function. This may require adding an otherwise unnecessary argument to the type.

Something like

type 'a resource = R

type resource_function = {
  f : 'a . 'a resource -> unit;
}

let create_resource () = R
let destroy_resource resource = ()

let with_resource f =
  let r = create_resource () in
  try
    f.f r;
    destroy_resource r
  with exn ->
    destroy_resource r;
    raise exn

There are downsides - any error messages will be unclear, and I’m not sure that the complications this would introduce would be worth the benefit.


#3

Without being a type theory expert, the times when I’ve asked similar questions I have been given the answer “this requires linear typing to enforce statically.”
I’d be very happy to be proven wrong on that one.

What you can do dynamically is to define a return type like

module Use_once : sig
  type 'a t

  val wrap : 'a -> 'a t

 (** throws exception if already used: *)
  val unwrap : 'a t -> 'a
    
end = struct
  type 'a t = { used : bool ref;
                leaf: 'a; }

  let wrap leaf = { used = ref false ;
                    leaf ; }

  let unwrap t =
    if !(t.used) then
      t.leaf
    else
      throw_exception ()
end

Potentially coupled with some infix operator like Rresult.R.(>>=)


#4

It looks like the general tool for your sort of problem are monadic regions. They cannot be expressed in OCaml in general (to my limited knowledge), but @lpw25 explains at the end of https://www.janestreet.com/tech-talks/effective-programming/ how one will be able to re-use the type-and-effect system from the work on effect handlers to that effect. Now, I am not familiar enough with your use-case to make an attempt at a more specific solution, but maybe you could play with the fact that you already have an explicit monad. So I am curious to know if @gsg’s idea works out.

In the context of resource management, linearity comes into play when you need non-trivial lifetimes as opposed to the LIFO discipline of monadic regions. For instance if you have producer-consumer situations or when you want data structures to manage your resources (aka move semantics à la C++/Rust).


#5

Hm I don’t think the approve above will work for because you’re allowed to run multiple queries against database before the end of the function, just not afterwards :\


#6

This approach prevents escaping of the type, but not of the values of the type nor the closures containing deferred effects on these values, e.g.

let f = ref (fun () -> assert false);;
let () = with_resource { f = fun a -> f := fun () -> destroy_resource a };;
!f ();;

I once tried a fairly complicated solution with freer monads that I then played with. The idea is that instead of a closure (function), with_resource accepts a value of a free monad that only contains the descriptions of the actions that has to be performed on the resource. So if this value escapes anywhere, the actions can’t performed unless explicitly requested using with_resource. But the limitation of this approach in OCaml is that it only works with a single resource at a time (a single instance of resource of a particular kind e.g. input channel). In my tentative example for file interaction, closer to the end of the file, the functions working on resources look similar to this:

let write s i =
  Freer.(File_writer.(
      write_line @@ "Hello, " ^ s ^ " " >>= fun () -> write_char i >>= fun () -> write_char '\n'))

The type inferred for the result of write is (unit, [> `Write ], [> ]) Freer.t. This encodes that it performs a `Write effect on the output channel and returns unit. The handler function has a type similar to this:

string -> ('a, [>  ] as 'b, [> `Write ] as 'c) Freer.t -> ('a, 'b, 'c) Freer.t

So when passed the result of write it returns (unit, _[> `Write ], _[> `Write ]) Freer.t, which encodes that the effect was handled. It’s already easy to see that the major limitation is caused by inability to express removal of polymorphic variant constructors from the sum type (or any other type e.g. type-level list). This prevents extending this approach to many channels/other resources of the same kind as well as support for re-emitting the same kind of effect in handlers. The proposed effect type system mentioned above allows to express handling of effects fully and without any special tricks. With an analogue of type classes this would be also expressible like in Haskell by using type-level lists.


#7

Oh the monad idea is cool. I think most likely saving the monad and using it after leaving the callback would still need to raise exceptions though, so I’m not sure if it makes it any easier to catch this kind of bad usage at compile time?

(Arguably, it should be incredibly obvious that that usage is wrong, but still… I’m curious about the limits of the type system :wink: )


#8

The trick with effects is that when the saved monad is used it’s handled (interpreted) by the handler at the usage site, so it’s entirely legal to reuse the result of e.g. write "Someone" 'X'. It will just write the line “Hello, Someone X\n” to the file supplied to with_file at usage site (there can be many calls to with_file with the same monad value). Without calling with_file the saved monad doesn’t do anything, it doesn’t contain any code interacting with the file, only values e.g. Write "Hello". But this only works if the monad needs just one file or a small fixed number of them.


#9

Ohh that’s a good point. Yeah, I think that would work (and the compiler would complain if the value was unused). I’ll have to think more about what the interface would look like to use with this a database (not sure if it’s worth it, but it’s fun to consider).