Is there any way to emulate Linear Types in OCaml yet? Specifically I’m wanting to be able to generate an opaque type in a module and allow the user to only ever store one copy of it at a time, and if it is ever stored anywhere else or passed to a function then where-ever it was stored in before is no longer useable. I know the tricks of behaviour types and so forth, but these do not prevent the user from holding copies of it and reusing a prior ‘state’ of the variable. And of course I can always test at run-time, but that does nothing to prevent compilation on code that is invalid. In addition if it is not finally consumed somewhere (so I can close a resource) then there is no compile error either.
I guess if I wanted a syntax in OCaml then it would be something like:
type inner = Inner of int
type t = inner Linear.t
let make () = Linear.make 42
let get (Inner l) =
let v = Linear.extract l in
v, Linear.make (v + 1)
let inc i =
let _, ni = get i in
ni
let close (Inner i) =
let _ = Linear.extract i in
()
Where the inner type is opaque outside this module, it is not allowed to be stored in anything that is copyable and if stored in something like a variant or a record then that variant/record becomes uncopyable as well, cannot be stored globally, if it drops out of scope (instead of being passed to some consuming function) then it should fail compilation as well, etc…
I’m guessing a ppx could be made to handle this, but I’ve been as yet unable to find one. Or better yet, is this on the roadmap to be added to the compiler at some point (at which point a full lifetime type would be useful as well, where something can be returned that has to be consumed ‘before’ something else is used on again as well, though that seems like adding lifetime bindings through the signatures would be painful)?
Given your definition, consider if Random.bool () then close resource else (). The type system does not see the difference between this and close resource. Even if we give close resource a different return type, this can be thrown away without linear types. The well-known solution is to embed the whole lifetime of the resource in a monad. Though, the monad-transformers might get hairy when tracking multiple resources and maybe effects, so it’s not a practically straight forward embedding linear types. (Note that e.g. Lwt don’t track IO channels this way.) [Edit: But see @aspiwacks upcoming post.]
I think writing a ppx will be challenging. A major issue is that linear types must be prevented from instantiating arbitrary type parameter, as exemplified by
val dup : 'a -> 'a * 'a
with the obvious definition. (We can infer from the above type that instantiating a linear type for 'a is unsound since the only ways to produce the pair given the parametric type is to duplicate it, to raise an exception, to exit, or to diverge, which we may consider misuse of the resource. But then consider
module M : sig
type 'a t
val create : 'a -> 'a t
end
In this case we have no way of telling whether 'a gets duplicated.)
(Note also that if a type has a component which is is linear, then values of that type must be treated linearly, so in particular linearity must be exposed for abstract types in some way. E.g. type t becomes type t = ... Linear.t for some ..., so the _ Linear.t notation may not be ideal.)
I think one reason we’re seeing so many PPXes is that the mapper makes it simple to implement useful transformations while avoiding a full program transformation. In this case however, one needs to track the full program flow, and deeply inspect types for parameters, and the linearity checking itself involves a some effort.
[eta: I see that there is some duplication with the answer which was posted just before me, which I hadn’t yet seen when I wrote mine]
The only general approach that I know for languages without native support for linear types, is the following: https://www.cis.upenn.edu/~jpaykin/papers/pz_linearity_monad_2017.pdf (there exists variants of the same idea on the literature, this is the latest incarnation of this idea).
It consists of an encoding of a linear language as a EDSL. It’s a bit heavy-handed, and does require some type-level programming which is quite hard to perform in Ocaml, so it’s not necessarily a good idea to try this (I haven’t reread the paper to see if the ideas could easily be ported to Ocaml).
The cheaper solution, but more bespoke, is to store the resource in some sort of state monad:
.ml
type 'a t = resource -> ( 'a , resource )
return = …
(>>) = …
.mli
type 'a t
return : 'a -> 'a t
(>>=) : 'a t -> ('a -> 'b t) -> 'b t
If you are careful of only exposing linear primitives, you can make sure that no illegal usage of your resource is performed. The price is that the resource can only be access indirectly, and that if you need several resources at the same time, it becomes tricky.
The basic idea is embedding a typed DSL using module system instead of GADT. This simple typed language with int and bool using GADT:
type _ expr =
| Int : int -> int expr
| Bool : bool -> bool expr
| Add : int expr * int expr -> int expr
| If : bool expr * 'a expr * 'a expr -> 'a expr
let rec eval : type a. a expr -> a = function
| Int i -> i
| Bool b -> b
| Add (a,b) -> (eval a) + (eval b)
| If (b,t,e) -> if (eval b) then (eval t) else (eval e)
eval (If (Bool true, Add (Int 1, Int 2), Int 5));;
- : int = 3
is encoded this way:
(* all the constructors of the GADT become functions *)
module type SYM = sig
type 'a repr
val int : int -> int repr
val bool : bool -> bool repr
val add : int repr -> int repr -> int repr
val if_ : bool repr -> 'a repr -> 'a repr -> 'a repr
end
(* an expression is a functor parametrized by a module of type SYM *)
module Ex(I: SYM) = struct
open I
let res = if_ (bool true) (add (int 1) (int 2)) (int 5)
end
(* and you can implement different interpretations *)
module Eval = struct
type 'a repr = 'a
external int : int -> int = "%identity"
external bool : bool -> bool = "%identity"
let add = (+)
let if_ b t e = if b then t else e
end
module View = struct
type 'a repr = string
let int = string_of_int
let bool = string_of_bool
let add i j = Printf.sprintf "(%s + %s)" i j
let if_ b t e = Printf.sprintf "if %s then %s else %s" b t e
end
let module M = Ex(Eval) in M.res;;
- : int = 3
let module M = Ex(View) in M.res;;
- : string = u"if true then (1 + 2) else 5"
You use the OCaml type system to implement the typing rules of the embedded language, and in the first article and the second one (§4.3), they implement the typing rules of linear logic.
This is OT but I wanted to point out that not being able to hit the title character minimum is a good opportunity to think about if you could have a better title. In this case, ‘Linear Types’ doesn’t tell the reader much when they’re scanning through the list. But ‘Is there a way to encode linear types?’ tells a great deal more and hits the character minimum.
I’ve stumbled upon a library that implements linear types for OCaml, using monads, lens and some ppx to make it more lightweight. Might be of interest: https://github.com/keigoi/linocaml
(The paper linked on that page is dated 2011/2014. In case anyone wonders whether the authors have found a time machine in a barn to be able to cite papers from 2018, there just seems to be an error in the preparation. It is freshly published, and a PDF with correct dates is available here.)
