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.

Heyduck

You can use monads to hide "linear" type handling in monadic bind and only export monadic type as abstract. – Uteutensil

What do you mean by simulate? runtime checks? – Kahl

No, static. With "simulate" I mean using existent type system to achieve a (close to) linear type system. – Monies

Here is some interesting research about dependent types: okmij.org/ftp/Computation/lightweight-dependent-typing.html – Monies

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

(* 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.

Fifteenth

Could you please provide a usage example too? I haven't really got this monad thing yet. :P – Monies

@OlleHärstedt: there is an usage example at the end (let test ...). Or do you want something else? – Fifteenth

Out of curiosity, would it be possible to define a phantom type that exactly corresponds to the state of the stack? When communicating between Lua and OCaml/C, we use a stack: Lua.newtable state;; (* Put new table on stack *) Lua.pushstring state "index";; (* Put table index on stack *) So the phantom type would now be something like [string, table]. – Monies

How do you alternatingly read lines from 2 files and write them to a thrird? – Immeasurable

Maybe we can rewrite this example using the new let* syntax? – Monies