Is there a good way to encode linear types in OCaml?

Learning
2

(Note you mixed the wrapping order above.)

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.

2 Likes