OCaml中的线性类型 [英] Linear types in OCaml

问题描述

Rust 具有线性类型系统.有没有(好的)方法可以在OCaml中对此进行模拟?例如，当使用ocaml-lua时，我想确保仅当Lua处于特定状态(堆栈顶部的表等)时才调用某些函数.

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).

编辑:这是有关该问题的资源多态性的最新论文: https: //arxiv.org/abs/1803.02796

Edit: Here's a recent paper about resource polymorphism relevant to the question: https://arxiv.org/abs/1803.02796

编辑2 :也有很多有关OCaml中会话类型的文章，包括提供一些语法糖的语法扩展.

Edit 2: There are also a number of articles about session types in OCaml available, including syntax extensions to provide some syntactic sugar.

推荐答案

正如约翰·里弗斯(John Rivers)所建议的，您可以使用单子风格来表示 以隐藏线性约束的方式进行有效"计算 效果API.下面是一个示例，其中类型('a, 'st) t是 用于表示使用文件句柄的计算(其标识为 隐式/无言以保证它不能被复制)，将 产生类型为'a的结果，并将文件句柄保持在状态 'st(幻像类型为打开"或关闭").你必须用 monad¹的run实际上可以执行任何操作，并且其类型可确保 使用后正确关闭文件句柄.

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

当然，这仅是为了让您领略以下风格 API.有关更严重的用途，请参见Oleg的 monadic 地区示例.

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.

您可能也对研究编程语言感兴趣 Mezzo ，旨在 是ML的一种变体，具有对状态的更精细控制(以及相关的 有效模式)，通过线性输入规则进行分隔 资源.请注意，这只是目前的一项研究实验， 实际上是针对用户的. ATS 也很重要， 虽然最终不像ML那样.锈实际上可能是合理的 这些实验的实用"对应对象.

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.

¹:它实际上不是monad，因为它没有return/unit组合器，但是重点是像monadic bind运算符一样强制执行类型控制的排序.它可能会有一个map.

¹: 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.

这篇关于OCaml中的线性类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！