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