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

Learning
#1

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

2 Likes
What changes would be required to the OCaml type system to make session types (or some kind of typestate) idiomatic?
#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
#3

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

3 Likes
#4

You can also look at this paper embedding a full linear lambda-calculus in Haskell. It is based on typed tagless final interpreters. You can find some full examples in OCaml on this page of Oleg Kiselyov’s blog.

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.

3 Likes
#5

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.

Something to ponder :wink:

2 Likes
#6

I’ve taken the liberty of appropriately updating the topic name on @OvermindDL1’s behalf. :slight_smile:

2 Likes
#7

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

2 Likes
#8

It is the part of even more interesting system - OCaml MPST (Multiparty Session Types) See the slides.

1 Like
#9

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

1 Like
#10

Just a heads up - the Linear Types implementation was merged in the GHC git a few days ago - https://gitlab.haskell.org/ghc/ghc/-/commit/40fa237e1daab7a76b9871bb6c50b953a1addf23

More information here:

1 Like