Linear types in OCaml

Question

Rust has a linear type system. Is there a (good) way to simulate this in OCaml? For example, when using ocaml-lua, I want to make sure that some functions are only called when Lua is in a certain state (table over stack, etc.).

Answer 1

As John Rivers suggested, you can use the monadic style to represent "efficient" computation in such a way as to hide the linear constraint in the API effect. The following is one example where the type ('a, 'st) t used to represent calculations using a file descriptor (whose identity is implicit / unexpressed to ensure that it cannot be duplicated), the product will result in type 'a and leave the descriptor A file is in the state 'st (a phantom type that is either "open" or "closed"). You must use run monad¹ to actually do something, and its type ensures that file descriptors 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 mf = fun () -> let x = run m in run (fx) 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 just to give you a feel for the style of the API style. For more serious applications, see Oleg monadic regions .

You may also be interested in learning the Mezzo programming language, whose goal is to be an ML variant with finer state control (and related spectacular patterns) through a linear typing discipline with shared Resources. Please note that this is only a research experiment, not actually aimed at users. ATS also matters, although finally less ML-like. Rusta can indeed be a reasonable "practical" analogue of these experiments.

¹: in fact, this is not a monad, because it does not have a return / unit combinator, but the point is to force control of sequencing by type, as the monadic bind operator does. However, it may have a map .