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…

(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 typ…

[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_linearit…

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 simpl…

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 ty…

[image] yawaramin: 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 taken the liberty of appropriately updating the topic name on @Overmin…

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

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

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: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst https…

One more update - GHC-9.0.1-alpha preliminary release was announced . GHC 9.0.1 will bring a long wanted linear types: A first cut of the new LinearTypes language extension, allowing use of linear function syntax and linear record fields. See also their roadmap .

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

Learning

Konstantin_Olkhovski December 11, 2019, 10:26am 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

Topic		Replies	Views
What changes would be required to the OCaml type system to make session types (or some kind of typestate) idiomatic? Community type-system	8	2337	March 1, 2021
A proposal for a resource-management model for OCaml Community	29	7481	January 1, 2021
What is the "right" way to add constraints on a type, to handle recursive structures with variants and to combine fragments of types? Learning real-world-ocaml , ocaml , gadt	38	11645	November 14, 2018
Major OCaml pain points Ecosystem language-design	33	3594	January 16, 2020
Modular Implicits Ecosystem compiler , faq	63	24375	October 24, 2022

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

Related topics