Линейные типы в OCaml

Question

Rust имеет систему линейного типа. Есть ли (хороший) способ имитировать это в OCaml? Например, при использовании ocaml-lua я хочу убедиться, что некоторые функции вызываются только тогда, когда Lua находится в определенном состоянии (таблица поверх стека и т. Д.).

Answer 1

Как предложил Джон Риверс, вы можете использовать монадический стиль для представления «эффективного» вычисления способом, который скрывает линейное ограничение в эффекте API. Ниже приведен пример, где тип ('a, 'st) t - , используемый для представления вычислений с использованием дескриптора файла (идентификатор которого равен , неявный/нечеткий, чтобы гарантировать, что он не может быть дублирован), произведет результат продукта типа 'a и оставьте дескриптор файла в состояние 'st (фантомный тип, который либо «открыт», либо «закрыт»). Вы должны использовать run monad¹, чтобы на самом деле что-либо сделать, и его тип обеспечивает , что дескрипторы файлов правильно закрыты после использования.

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. Более серьезное использование см. В статьях Олега monadic regions.

Вы также можете быть заинтересованы в исследовании языка программирования Mezzo, целью которого является быть вариант ML с более мелкозернистой контроля состояния (и связанных с ними effectful моделей) через линейную типизации дисциплины с разделенными ресурсов. Обратите внимание, что это только исследовательский эксперимент, а не , фактически нацеленный на пользователей. ATS также уместен, хотя, наконец, меньше ML-like. Руста может фактически быть разумным «практическим» аналогом этих экспериментов.

¹: на самом деле это не монада, потому что у него нет комбинатора 4444, но дело в том, чтобы заставить секвенировать с контролем типа, как это делает монадический оператор bind. Это может быть map.