OCaml中的线性类型

Question

Rust有一个线性类型的系统.在OCaml中是否有任何(好的)模拟方法？例如,当使用ocaml-lua时,我想确保只有当Lua处于特定状态(堆栈顶部的表等)时才会调用某些函数.

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

Answer 1

正如John Rivers所建议的那样,您可以使用monadic样式来表示"有效"计算,其方式是隐藏效果API中的线性约束.下面是一个示例,其中一个类型('a, 'st) t用于表示使用文件句柄进行计算(其标识是隐式/未说明以保证它不能被复制),将生成类型的结果'a并将文件句柄保留在状态 'st(幻像类型)要么"开放"要么"关闭".您必须使用runmonad¹实际执行任何操作,其类型确保文件句柄在使用后正确关闭.

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的monadic区域示例.

您可能也对研究编程语言Mezzo感兴趣,该语言 旨在成为ML的变体,通过具有分离资源的线性类型学科对状态(和相关的有效模式)进行更细粒度的控制.请注意,它现在只是一项研究实验,并非实际针对用户.ATS也很重要,但最终不像ML那样.Rust实际上可能是这些实验的合理"实际"对应物.

¹:它实际上不是monad,因为它没有return/ unitcombinator,但重点是强制类型控制的序列,就像monadic bind运算符一样.但它可能有一个map.