keigoi / linocaml

Monad-based linear types in OCaml, with a few syntax extensions
Apache License 2.0
37 stars 4 forks source link

Non-linear value (Data__) constructor should be usable inside %linval #3

Closed keigoi closed 7 years ago

keigoi commented 7 years ago

Data should be public, while Lin is not. Make this distinction more explicit -- remove from Data and rename Lin__ to "Lin_Internal__" or something

keigoi commented 7 years ago

Nope, this actually compromises linearity. A short example:

let f () =
  let%lin #s = [%linval Data !!s ]
  in
  match%lin get s with
  | _ -> return () (* here the content of s is disposed without actually using it *)
keigoi commented 7 years ago

At least, we must limit the use of Data inside %linval and forbid !!s inside Data