Talk, March 7, Effective Programming: Adding an Effect System to OCaml

announce
type-system

#1

Leo White is giving a talk at Jane Street’s NY office on March 7th about adding an effects system to OCaml. This is pretty cool stuff; he shows how to add effects tracking to OCaml seamlessly, so that all existing programs continue to compile as is, and yet, you can track purity quite precisely. It even has region support to let you write pure functions that use mutability locally, like the ST-monad without the monad. He was showing me some of the demos today, and they looked pretty sweet.

Space is limited, so if you’re interested, you should register soon.

https://www.janestreet.com/tech-talks/effective-programming/

y


#2

Will the session be recorded and uploaded for public viewing? :slight_smile:


#3

Any chance of getting the talk recorded?


#4

For sure. We record and post all of our talks.


#5

Still no record available?


#6

Sadly, there was a problem with the recording, so we’re not going to post it. However, in the next few weeks Leo is going to do an internal version of the same talk in our London office, and we’ll post that.

y


#7

OCaml’s recording curse strikes again.


#8

This is really apropos. I did a ReasonML talk last night and the mic got switched off somehow right before I started speaking. I’m thinking I’ll dictate a new ‘soundtrack’ synchronised with the screencast that I recorded…


#9

The recorded talk was probably too bleeding edge for a wider audience :smirk:


#10

Luckily the problem with the recording was fixable. So here’s the video:

https://www.janestreet.com/tech-talks/effective-programming/


#11

Wonderful talk, Leo. You present these concepts very clearly, and this is all extremely exciting. I hope we can integrate this stuff before multicore is merged.

I gather that this demo is off of your effect-typing branch. Can we get this branch into opam to play with? Also, how much do you feel is missing at this point, not including the future work stuff?


#12

It’s not quite in a state to put on opam at the moment. There’s a week long seminar on algebraic effects in a few weeks and I hope to get it into a decent state whilst I’m there.

In terms of what’s missing:

  1. I’m still not happy with the particular form of row polymorphism / subtyping that it uses. I’ve been working on a better system for a while and I think I should be able to try that out this year.
  2. Some of the future work – lift which I skipped over in the talk – is needed to be really usable in practice.
  3. The implementation of the inference is too inefficient. It’s not conceptually hard to fix but it still needs doing.

That only applies to the first half of the work described i.e. a system that tracks algebraic effects but does not track OCaml’s built-in effects. I think the design of the second half still needs a lot of thought. My plan is to try to merge the first half into multicore in the not too distant future – it’s forwards compatible with the second half and a lot closer to being stable.

I think getting the inference really good will require some more fundamental changes to the type-checker. Luckily there is a planned rewrite of the system over the next few years, and I think that will be a good opportunity to make those changes. However, the system should still be usable without those changes, and they’ll be backwards compatible anyway.


#13

Does that mean not to expect anything in the next few years?


#14

Is that because the type signature gets too large?

Also, what do you do with recursive effects – a handler catching an effect and also performing a different one as a response?

Not sure where lift would fit in, since the whole point is that we got rid of monads. What are you lifting into?

Are you doubting the effectiveness of the region management? Seems like you already put a lot of thought into that. What effects does OCaml have other than mutation, IO and exceptions?


#15

No, as I said, it should be usable without those changes and the changes should be backwards compatible. Ideally we’d just have the best system from the first release, since it will be easier to use, but I think it would be fine to upstream the earlier version.


#16

Is that because the type signature gets too large?

No. I don’t really want to go into technical details, but it is about having more subtyping in the system.

Also, what do you do with recursive effects – a handler catching an effect and also performing a different one as a response?

That is not a recursive effect, the effects of a handler will be handled by a outer handler, not passed back to the paused computation.

Are you doubting the effectiveness of the region management?

There are all kinds of issues around how regions are handled. Currently they are much more awkward to use than they need to be, and unlike the improvements to effect inference, some of the fixes for that would not be backwards compatible with the current implementation.