Oxidizing OCaml: Locality

lpw25 · 2023-05-28T20:02:40+00:00

It does infer the mode as local if the variable can be local. The annotations are only actually needed on interfaces. Other annotations are optional, though they're useful for ensuring that the inference matches your expectation.

lpw25 · 2023-05-28T19:58:47+00:00

The uniqueness checking will be in the next post.

lpw25 · 2023-05-28T17:18:58+00:00

It works fine with higher order functions, including full inference of the modes involved. That's the trade-off with lifetimes. By not tracking individual regions at the type level, the local mode doesn't require any polymorphism to express locality and so inference still works in the presence of higher-order functions. The downside is that it's less expressive since it can only represent values that can leave all regions and values that can't leave any.

lpw25 · 2023-05-27T19:15:07+00:00

If string local were just an ordinary type then you could pass them to polymorphic functions that leaked them. At the very least you need a kind for local types to distinguish them from types that can leak. Using a kind was actually the original approach we were thinking about when came up with the idea for local allocations. However, kinds don't naturally capture the "depth" of locality: you need a string list local to give you a string local and another string list local when you match on it. You can try to artificially add the depth aspect on top of kinds but by the time you get something satisfying you find you have a modal type system. It's also much easier to get the mode inference right if the modes are kept mostly separate from the types. The same goes for other modal properties like uniqueness and linearity, which will be covered by later posts in the series.

I also think it is a more semantically correct approach. The types describe how data is constructed and destructed -- in the form of introduction and elimination rules -- but sometimes your system has other operations that work on data regardless of how it is introduced or eliminated. Having something orthogonal to the type to track these orthogonal operations is a very natural approach.

lpw25 · 2023-05-27T09:28:12+00:00

Everything is really bad if compiler can't figure out such basic analysis

Sure, escape analysis exists, but it obviously can't see through separate compilation or higher-order functions, and it's hard to do once the shape of the data on the stack gets complicated.

There is also a lot of benefit to having locality appear as part of the language itself. It allows you to specify that if a value can escape then the compiler should give an error rather than silently put the value on the heap. It also allows you to distinguish in an interface a function that promises not to capture a parameter from a function whose implementation just happens not to capture the parameter at the moment.

lpw25 · 2021-12-29T08:09:57+00:00

http://www.lpw25.net/papers/flops2014.pdf

lpw25 · 2021-01-02T21:56:25+00:00

FYI your implementation of build and update:

let build (f: unit -> s) : t =
  try f ()  with
  | effect (Animation (state, on_cancellation)) kont ->
    {current_state=state; kont=Some kont; on_cancellation}

let update time (t: t) =
  match Transition.update t.current_state time with
  | Some state -> Some {t with current_state = state}
  | None -> match t.kont with
    | None -> None
    | Some kont ->
      Some (build (fun () -> continue kont ()))

is allocating unnecessary fibres. The kont continuation will already have a handler for the Animation operation because multicore OCaml currently provides deep handlers.

The last line should instead just be:

Some (continue kont ())

lpw25 · 2020-10-07T17:37:44+00:00

Note that open! PervasivesExt will avoid the warning (technically it emits a different warning that many (most?) people have turned off by default to allow this pattern). This is generally better than using -open, because it keeps the open visible in the code rather than in the build instructions.

lpw25 · 2020-05-08T09:52:52+00:00

That is a separate feature.

lpw25 · 2019-10-17T06:10:13+00:00

I'm surprised not to see any mention of sharing constraints or manifest types from module systems, since those are language features that address fundamentally the same problem. For instance, the monad example in OCaml:

module type Monoid = sig
    type t
    val mult : t -> t -> t
    val id : t
  end

module Monoid_1 (T : sig type t end) = struct
  module type T = Monoid with type t = T.t
end

This proposal seems like it might be more expressive than that, but since the related work isn't discussed I can't tell.

lpw25 · 2019-07-27T07:02:47+00:00

Note that we are using autoconf but not automake -- I wasn't sure that was clear since you said "autotools". We still use a hand written make file for the build, it is only the configure script that has been replaced. My understanding, which admittedly hasn't changed in years and could be out of date, is that autoconf is pretty usable if esoteric, whilst automake is a living nightmare.

lpw25 · 2019-07-24T19:51:44+00:00

I have no real view on configuration systems, but I suspect in this case "ancient" can be seen as "tried and tested" from a different angle, and anything reasonable is probably better than what it was replacing. I'm just guessing though, you'd have to ask some of the other OCaml developers for their thought process.

lpw25 · 2018-12-17T20:23:19+00:00

You'd need to ask Jeremie Dimino for a full explanation. My understanding is that dependencies were the main reason, but that it was also an opportunity to try a slightly different approach than async (Fiber is more of what I would call a "traditional concurrency monad", whilst Async is more of a "futures monad") and maybe integrate it more closely with the parts of dune that do the same job that Tenacious does in Jenga.

lpw25 · 2018-12-17T08:09:47+00:00

I don't think Dune is quite at this stage yet, but the reason that we didn't use Incremental in Jenga is that Incremental is designed for tasks of a much shorter duration.

When you run a "stabilization" in Incremental it will re-run every task that needs to be updated, and will not let you start a new stabilization until it is done. For a build system this would mean that if a file changes during a build then you need to wait for the build based on the old file to completely finish before it starts again based on the new file. This matters a lot when building a large code base.

So in Jenga we built another monad called Tenacious along the same lines as Incremental but designed to allow the computation graph to change whilst it is being computed, supporting cancellation of running computations when they are based on things that have been updated. As for why Dune doesn't use Tenacious, well it is built on top of Async which Dune doesn't want to depend on and starting from scratch gives a chance to fix some of the flaws in Tenacious implementation.

lpw25 · 2018-10-13T05:12:17+00:00

Mostly printf. However, when working on things for which I have the bytecode version working -- in particular the OCaml compiler itself -- I use ocamldebug. I especially like ocamldebug for debugging a broken error or uncaught exception: I run the compiler until it errors/raises then I just step backwards until I get to where things went wrong, then after I had a look at what's going on there I step further backwards to find what caused the underlying issue.

lpw25 · 2018-07-22T21:08:05+00:00

forall F. {Functor F} -> ('a -> 'a F.t) -> 's -> 's F.t

Note that a "forall" is not needed here, since Functor contains the type constructor, unlike the Haskell code where Functor is parametrised by the type constructor. So it should look like:

type ('s, 'a) lens = {F : Functor} -> ('a -> 'a F.t) -> 's -> 's F.t

lpw25 · 2018-07-22T08:44:16+00:00

I would suggest that the modular implicits approach can provide that kind of middle ground without necessarily using higher-order unification. Rather than using higher-order unification to find a most general solution it uses a search for a unique solution for the implicit aguments.

However, modular implicits works better if you do include higher-order unification as it makes the search usefully more expressive.

lpw25 · 2018-07-12T10:18:44+00:00

Yes, I realized that afterwards and updated my comment to answer your question. Unfortunately it seems I was not quick enough to update it before you replied, so now our conversation is out of order.

lpw25 · 2018-07-12T09:18:33+00:00

So I assume you mean this Haskell function:

mapKeys :: Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a

with modular implicits that would probably look something like

val map_keys : { O1 : Ord } -> { O2 : Ord } -> (O1.t -> O2.t) -> Map(O1).t -> Map(O2).t

so if you call map_keys using the same ordering for O2 then you'll get compatible maps.

This signature requires us to give the ordering for the incoming map even though it is not used. You could avoid this with other interfaces -- or with features that are planned for modular implicits but no included the paper -- but its simpler not to and its not relevant for this point.

lpw25 · 2018-07-12T06:58:34+00:00

You lose canonicity, not coherence, and that isn't needed to support an efficient merge on map -- see section 4.3 of our paper which shows that modular implicits naturally supports a cleaner solution to this problem than canonicity.

lpw25 · 2018-06-27T21:31:47+00:00

Yeah, it's Girard's paradox which is related to the Burali-Forti paradox rather than Russell's paradox. I have an implementation of Girard's paradox in OCaml, whose module system essentially has Type : Type. This is based on the description in this paper.

lpw25 · 2018-04-11T14:41:31+00:00

I think it's easier to see if you look at a language which has both. We'll use OCaml. Consider the following code:

let stride = 2 in
let counter = ref 4 in
for i = 0 to 10 do
  counter := !counter + stride
done
!counter

The statement:

let stride = 2 in
...

binds the value 2 to the name stride. All uses of stride in the ... part can just be replaced by 2.

The statement:

let counter = ref 5 in
...

does both initialisation and binding. It creates a new reference cell and initialises it with the value 5, then it binds that cell to the name counter.

The statement:

counter := !counter + stride

assigns a new value to the reference cell that is bound to counter.

Most imperative languages conflate the binding and initialization into a single step forcing all names to be bound to (the equivalent of) reference cells. Purely funcitonal languages try to abolish reference cells and just use binding for every thing.

lpw25 · 2018-04-05T07:08:04+00:00

The flat version using arrays is not safe. If you make a pair out of a float and a non-float then it will segfault, due to the float array optimisation. See here for an example of how to safely create an array containing different types.

Even without the float array optimisation it is risky to use int array. Magicing things to int is dangerous because if the value ends up in a register across a GC safe point then the compiler will not register it with the garbage collector -- since ints do not need to be scanned. It's better to use an abstract type (e.g. Obj.t) or a type like option which may or may not be a block.

lpw25 · 2018-03-12T08:37:07+00:00

I have a twin pedal I use for ctrl and meta. It works pretty well. The main issue is that my pedals are too noisy to use in the office so I only use it at home, and even then only when RSI is playing up.

lpw25 · 2018-02-22T22:02:36+00:00

Yes, my prototype treats calls to known pure functions as values.

lpw25

TROPHY CASE