12 Likes
Is this ever coming to regular OCaml, or will it always be Jane Street skunk works?
I think this is a complex question. From what I know, janestreet wants to upstream it, but it might not be successful, because it has to be reviewable and maintainable for upstream.
1 Like
Jane Street folks have not just been implementing and using these features, but also writing them up to conferences for wider communication to the scientific community. See recent papers in ICFP and POPL. Theyāve also given a number of talks at HOPE, OCaml and ML workshops over the years on this work.
Jane Street developers are regularly engaging with the core devs to discuss the development of these ideas. While I canāt say if and when these features will land, they have been making all the right moves so that if these features are put up for upstreaming, it wouldnāt come as a surprise.
5 Likes
The reason I ask is because I first heard about unboxed types for OCaml five years ago, and Iāve been looking forward to using itā¦ for five years.
I realize these things take time. Iām just eager to get my hands on these features, but I guess I will have to wait some more years. The plus side is that in these five years, the features being discussed in the original video have been implemented and are in use at Jane Street.
4 Likes
Kudos to the speaker! Chrystal-clear exposition of complex topics, no wasted time. Thanks for posting this.
2 Likes
I totally agree!
For those interested in recent discussion about the public availability and stability of this work, check out this thread:
2 Likes
These things do take time. And the cost of releasing a not-yet-ready feature in OCaml and potentially rolling it back / fixing it is quite high. Validation of these features in Jane Street is a useful data point for stability.
4 Likes
I agree the talk was well done. However, when hearing about the now five mode dimensions with more to come, I dread that this could destroy the beautiful simplicity of the language. Is there no simpler way to get more safe performance? Otās somewhat reassuring that they strive for āno cost if not usedā.
3 Likes
Yeah, Iām not sure āmodeā is quite the right term, insofar as it suggests āmethodā or āway of doingā something. Personally Iād like to see the concept expressed in a formal logic if possible (just as linear types come from linear logic, expressible in a sequent calculus.)
I have assumed that āmodeā refers to modality, formalized in modal logic. In any case, I found a presentation of their āmode calculusā in terms of sequents on page 11 of Oxidizing OCaml with Modal Memory Management.
I am not an expert, but afaiu it has long (nearly always?) been understood that that the exponential (! and ?) operators of linear logic are modal, and since this work seems to be downstream of that, āmodeā seemed sensible to me. E.g., the abstract of Girardās 1987 exposition Linear Logic reads
Abstract. The familiar connective of negation is broken into two operations: linear negation which
is the purely negative part of negation and the modality āof courseā [!] which has the meaning of
a reaffirmation. Following this basic discovery, a completely new approach to the whole area
between constructive logics and programmation is initiated. [Emphasis added.]
In terms of the concrete syntax, I think the choice to specify modalities via an additional annotation seems reasonably ergonomic. AFAIU, you can always put this stuff directly into the types. But that can become quite cumbersome, because you often have the larger part of values used in the same modality and having to annotate this explicitly everywhere adds a lot of noise. Having a separate annotation space makes it pretty easy to have a default modality that can be left implicit, so that you only need to increase the complexity of the annotation when you are using the more exotic modes. This partition in the syntax also means that instead of having to digest all the information from one deep nest of types, you are able to look to different areas for different kinds of information (e.g., look to the types for information about the values, look to the modes for information about how they can be used).
when hearing about the now five mode dimensions with more to come, I dread that this could destroy the beautiful simplicity of the language
I share the concern about the implications of adding complexity to the language 
I think the promise of improved perf and correctness is well worth the experimentation, but I am glad that there is a slow and circumspect process for extending the language exactly because it helps to guard against the premature introduction of cumbersome and possibly non-orthoginal complications.
None of this dampens my interest and enthusiasm in this work tho, and I am eager to have time to experiment with it in earnest! 
6 Likes
Thanks, thatās just the kind of thing I was thinking of. Iād forgotten about the use of modality in linear logic. I confess Iāve never fully grokked the concept - the āmodalityā of Necessity and Possibility is intuitive enough (and closely related to linguistic mood), but the formal logical notion involves more than that. So maybe āmodeā is indeed the right term.
1 Like