But then does it mean that for functions we want to explicitly type we wont benefit from the inferred locality and have to go through the hassle anyway?
This is a bit subtle. We're not going to infer exclaves, because doing so can change the asymptotic runtime of your program. (Actually, I should make a video about that. But not for a few weeks!) We can infer everything else -- but (as @goodnight_noom suggests) every time you write a type, you potentially interrupt that inference. So it really is some hassle. And yet my colleagues here at Jane Street are happy to put in the time adding the annotations to get their speedup. The whole system is opt-in, so indeed you'd probably only want to do this where it really counts.
@@RichardEisenberg-JS Why can't there be mode inference even if you specify the types? Why does specifying a type without a mode annotation mean it's global?
@@pdp11 I suppose we could have something like `_ t1 -> _ t2` that indicates we should infer the mode. (Well, not that syntax.) But we need to know what `t1 -> t2` means: is it saying global implicitly? Or does it want inference? Right now, if you write a type, its modes are considered known. (This has to be the case in interface files, regardless of what we do on function annotations.)
It seems like a lot of type annotations. I wonder if the escape analysis could be done beneath the covers so it doesn't surface through the types. I recall Go's escape analysis being pretty good without guidance like this. I'm probably missing something.
Most of the annotations here aren't necessary. They're there to make everything more explicit for the video. The `exclave_`s are necessary, but nothing else. Marking lcoals in mli files is necessary though, to enable separate compilation.
Why do the contents of a local_ list have to also be local_? I feel like that was glanced over but it's not obvious to me. What would be the problem if the argument to iter leaks a reference to a list element? We can still clean up the list itself at the end of the region, right?
Spot on, yes. In general, we have a free choice here: we could say (A) that the contents of a local list are local or (B) the contents of a local list are global. (A) means that we can store local things in a list but we can't let the contents of a local list escape; (B) means that we can let the contents of a local list escape, but we can't store local things in a list. We can't have both. But we can, actually, via a thing called the global modality. We'll get there in a few videos. In brief, it allows you to label a field of a structure as acting like (B). So you get an (A)-list (the normal list type) and a (B)-list (something you'd have to write yourself). These would be different types. This is a bit annoying, for sure, but having one type that can both store local things and then let them escape is definitely worse!
Hmm, so this was just to solve for simple functions like iter and init, where even here, I find the process too complex by itself - imagine doing this for complex functions, and depending on libraries that doesn't support locals. Also, my guess is that this will make people copy other libraries code to their own codebase, to add locals support - so it breaks the modularity of libraries
Decent points, indeed. (Though these functions have the complexity that hits locals -- bigger functions aren't necessarily harder in this respect.) We're currently working our way through `base` (our open-source standard library), adding local annotations throughout. It's not particularly easy! And yet the benefits we're seeing seem worth the cost. A big question we're thinking about is how this will all shake out in the end, which is one of the reasons we want to develop this on a branch of the compiler instead of pushing early for inclusion in general OCaml.
So is the plan to make this inferred by the compiler? Otherwise it seems like a lot of hassle unless you have some hotspots you want to speed up.
But then does it mean that for functions we want to explicitly type we wont benefit from the inferred locality and have to go through the hassle anyway?
This is a bit subtle. We're not going to infer exclaves, because doing so can change the asymptotic runtime of your program. (Actually, I should make a video about that. But not for a few weeks!) We can infer everything else -- but (as @goodnight_noom suggests) every time you write a type, you potentially interrupt that inference. So it really is some hassle. And yet my colleagues here at Jane Street are happy to put in the time adding the annotations to get their speedup. The whole system is opt-in, so indeed you'd probably only want to do this where it really counts.
@@RichardEisenberg-JS Why can't there be mode inference even if you specify the types? Why does specifying a type without a mode annotation mean it's global?
@@pdp11 I suppose we could have something like `_ t1 -> _ t2` that indicates we should infer the mode. (Well, not that syntax.) But we need to know what `t1 -> t2` means: is it saying global implicitly? Or does it want inference? Right now, if you write a type, its modes are considered known. (This has to be the case in interface files, regardless of what we do on function annotations.)
It seems like a lot of type annotations. I wonder if the escape analysis could be done beneath the covers so it doesn't surface through the types. I recall Go's escape analysis being pretty good without guidance like this. I'm probably missing something.
Most of the annotations here aren't necessary. They're there to make everything more explicit for the video. The `exclave_`s are necessary, but nothing else. Marking lcoals in mli files is necessary though, to enable separate compilation.
Why do the contents of a local_ list have to also be local_? I feel like that was glanced over but it's not obvious to me. What would be the problem if the argument to iter leaks a reference to a list element? We can still clean up the list itself at the end of the region, right?
Spot on, yes. In general, we have a free choice here: we could say (A) that the contents of a local list are local or (B) the contents of a local list are global. (A) means that we can store local things in a list but we can't let the contents of a local list escape; (B) means that we can let the contents of a local list escape, but we can't store local things in a list. We can't have both. But we can, actually, via a thing called the global modality. We'll get there in a few videos. In brief, it allows you to label a field of a structure as acting like (B). So you get an (A)-list (the normal list type) and a (B)-list (something you'd have to write yourself). These would be different types. This is a bit annoying, for sure, but having one type that can both store local things and then let them escape is definitely worse!
Hmm, so this was just to solve for simple functions like iter and init, where even here, I find the process too complex by itself - imagine doing this for complex functions, and depending on libraries that doesn't support locals. Also, my guess is that this will make people copy other libraries code to their own codebase, to add locals support - so it breaks the modularity of libraries
Decent points, indeed. (Though these functions have the complexity that hits locals -- bigger functions aren't necessarily harder in this respect.) We're currently working our way through `base` (our open-source standard library), adding local annotations throughout. It's not particularly easy! And yet the benefits we're seeing seem worth the cost. A big question we're thinking about is how this will all shake out in the end, which is one of the reasons we want to develop this on a branch of the compiler instead of pushing early for inclusion in general OCaml.
I am subscribed, I have a bell - I only see this now