OCaml中的线性类型

Question

锈有一个线性系统。有没有（好的）方法可以在OCaml中模拟这种情况？例如，在使用ocaml lua时，我想确保只有在lua处于特定状态时（堆栈顶部的表等）才会调用某些函数。

编辑：这里有一篇关于资源多态性的最新论文，与这个问题有关：https://arxiv.org/abs/1803.02796

编辑2：还有一些关于OCaml中会话类型的文章，包括语法扩展，以提供一些语法方面的支持。

Answer 1

正如约翰·里弗斯（John Rivers）所建议的，可以使用一元样式来表示“有效”计算，以隐藏effect API中的线性约束。下面是一个示例，其中使用类型（'a，'st）t）来表示使用文件句柄（其标识是隐式的/未声明的，以保证它不能被复制）的计算，将生成类型'a的结果，并将文件句柄保持在状态'st（幻象类型为“打开”或“关闭”）。你必须使用monadñ的run来实际执行任何操作，它的类型确保文件句柄在使用后正确关闭。

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

当然，这只是为了让您体验一下API的风格。有关更重要的用途，请参见Oleg的一元区域示例。

您可能还对研究编程html" target="_blank">语言Mezzo感兴趣，它旨在成为ML的变体，通过具有分离资源的线性类型学科对状态（和相关有效模式）进行更细粒度的控制。注意，它目前只是一个研究实验，实际上并不针对用户。ATS也是相关的，尽管最终不那么像ML。铁锈实际上可能是这些实验的合理“实用”对应物。

它实际上不是monad，因为它没有返回/单元组合器，但关键是像monadicbind运算符那样强制类型控制的排序。不过，它可以有一个map。