ocamllinear-types

Linear types in OCaml


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.


Solution

  • 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
    
    (* starting with OCaml 4.13, you can use binding operators:
       ( let* ) instead of ( >>= ) *)
    let test =
      let open File in
      let ( let* ) = bind in
      run begin
        let* () = open_ "/tmp/foo" in
        let* content = read in
        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.