OCaml 中的线性类型

Rust http://www.rust-lang.org/有一个线性类型系统。有什么（好的）方法可以在 OCaml 中模拟这个吗？例如，当使用 ocaml-lua 时，我想确保仅当 Lua 处于特定状态（堆栈顶部的表等）时才调用某些函数。

Edit：这是最近一篇关于与该问题相关的资源多态性的论文：https://arxiv.org/abs/1803.02796 https://arxiv.org/abs/1803.02796

Edit 2：还有许多关于 OCaml 中会话类型的文章，包括提供一些语法糖的语法扩展。

正如 John Rivers 所建议的，您可以使用一元样式来表示 以隐藏线性约束的方式进行“有效”计算 效果API。下面是一个示例，其中类型('a, 'st) t是 用于表示使用文件句柄的计算（其身份是 隐式/不言而喻以保证它不能被复制），将 产品是类型的结果'a并将文件句柄保留在状态'st（幻像类型为“打开”或“关闭”）。你必须使用 这runmonad1 实际执行任何操作，其类型确保 文件句柄在使用后正确关闭。

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

当然，这只是为了让大家领略一下风格 API。对于更严重的用途，请参阅 Oleg 的单子的 地区 http://okmij.org/ftp/Haskell/regions.html例子。

您可能还对研究编程语言感兴趣Mezzo http://gallium.inria.fr/%7Eprotzenk/mezzo-lang/，其目的是 是 ML 的一个变体，具有更细粒度的状态控制（以及相关的 有效的模式）通过线性打字规则与分离 资源。注意，目前只是一个研究实验，不是 实际上是针对用户的。ATS http://ats-lang.org/也相关， 虽然最终不太像 ML。 Rust 实际上可能是合理的 这些实验的“实际”对应物。

1：它实际上不是一个单子，因为它没有return/unit组合器，但重点是强制类型控制排序作为单子bind操作员这样做。它可以有一个map， 尽管。