Linear types in OCaml

Question

Rust has a linear type system. Is there any (good) way to simulate this in OCaml? E.g., when using ocaml-lua, I want to make sure some functions are called only when Lua is in a specific state (table on top of stack, etc).

Edit: Here's a recent paper about resource polymorphism relevant to the question: https://arxiv.org/abs/1803.02796

Edit 2: There are also a number of articles about session types in OCaml available, including syntax extensions to provide some syntactic sugar.

Answer 1

As suggested by John Rivers, you can use a monadic style to represent "effectful" computation in a way that hides the linear constraint in the effect API. Below is one example where a type ('a, 'st) t is used to represent computation using a file handle (whose identity is implicit/unspoken to guarantee that it cannot be duplicated), will product a result of type 'a and leave the file handle in the state 'st (a phantom type being either "open" or "close"). You have to use the run of the monad¹ to actually do anything, and its type ensure that the file handles are correctly closed after use.

module File : sig
  type ('a, 'st) t
  type open_st = Open
  type close_st = Close

  val bind : ('a, 's1) t -> ('a -> ('b, 's2) t) -> ('b, 's2) t

  val open_ : string -> (unit, open_st) t
  val read : (string, open_st) t
  val close : (unit, close_st) t

  val run : ('a, close_st) t -> 'a
end = struct
  type ('a, 'st) t = unit -> 'a
  type open_st = Open
  type close_st = Close

  let run m = m ()

  let bind m f = fun () ->
    let x = run m in
    run (f x)

  let close = fun () ->
    print_endline "[lib] close"

  let read = fun () ->
    let result = "toto" in
    print_endline ("[lib] read " ^ result);
    result

  let open_ path = fun () -> 
    print_endline ("[lib] open " ^ path)
end    

let test =
  let open File in
  let (>>=) = bind in
  run begin
    open_ "/tmp/foo" >>= fun () ->
    read >>= fun content ->
    print_endline ("[user] read " ^ content);
    close
  end

Of course, this is only meant to give you a taste of the style of API. For more serious uses, see Oleg's monadic regions examples.

You may also be interested in the research programming language Mezzo, which aims to be a variant of ML with finer-grained control of state (and related effectful patterns) through a linear typing discipline with separated resources. Note that it is only a research experiment for now, not actually aimed at users. ATS is also relevant, though finally less ML-like. Rust may actually be a reasonable "practical" counterpart to these experiments.

¹: it is actually not a monad because it has no return/unit combinator, but the point is to force type-controlled sequencing as the monadic bind operator does. It could have a map, though.