Re: [Caml-list] Purity in ocaml

[Goswin von Brederlow <goswin-v-b@web.de>]

On Thu, Jan 23, 2014 at 01:18:00PM -0500, Yotam Barnoy wrote:
> > Unfortunately in ocaml you have to annotate a lot if done right. You
> > need to create a lot of .mli files, module types or class types. Not
> > to mention GADT need type annoation for nearly every function.
> >
> > So I'm not too sure about keeping this transparent.
> >
> >
> I haven't dealt much with GADTs myself, so I'm not sure if they present a
> special challenge.

No special challenge there I think. I just ment that GADTs need to be
annotated so the purity annotation might have to be spelled out there
too.
 
> It might be better to talk about the scope of impurity there. The
> > impurity dies with the death of the mutable. Like when you create a
> > local hashtbl to speed up computations, get the result and then return
> > the result (destroying the hashtbl). The impurity ends there. Global
> > mutables are just a special case of having the lifetime of the
> > programm.
> >
> >
> Fair enough. This is why the st annotation would exist for
> functions/expressions that use the same local mutable state: the
> interaction of these statements must retain its ordering, but once the
> scope is exited, nothing else can interfere with this local state. Global
> state can always be interfered with by other code.

If the global scope is exited the program is done. Just a special case
of a rather large scope.

> That won't work. You need to be able to declare purity in the source.
> > Otherwise, for example, how would you pass a module to a function that
> > must have a pure function? (as you say below)
> >
> >
> I'm not sure what you mean. Are you asking for purity annotations in the
> syntax? It's always possible to do
> let f : pure 'a -> 'a = fun x -> ...
> as one option, but I agree that having some shortcut in the syntax would be
> useful. I'm open to suggestions. Regarding first class modules, those are
> in the same category as higher-order functions that cannot be inferred --
> they must be annotated.

"pure" would be a new keyword, like "type"?
 
> > If you can annotate that in the source (.ml or .mli files) then that
> > should end up in the .cmi file as well, right. Then why would the
> > compiler generated purity, in case you don't have a .mli file, not end
> > up in there too?
> >
> > Note that if a library does not annotate purity but the function
> > happens to be pure then you can't have the compiler fill that in. The
> > library makes no promise that the function will remain pure in the
> > future and by having the compiler adding that promise you would change
> > the API of the library. This would break dynamic linking.
> >
> > So I realy think purity belongs in the .mli and .cmi files. Not
> > something seperate. And the compiler can only fill in the purity when
> > there is no .mli file. With .mli file it can only check that the given
> > type can be unified with the code regarding its purity.
> >
> >
> This is a very good point that I haven't considered before. Inferred
> cross-module purity supplies more information than the interface provides.
> I can see a few ways to approach this:
> 
> 1. Your method, which is the simplest method, of requiring all purity
> annotations to be in the .mli file. This may make the most sense, but it
> also means that to take advantage of the resulting potential optimizations,
> a company like Jane Street would have to go back and modify all of its .mli
> files, constraining the purity of functions. I really wanted this to be
> more of a transparent feature -- one which can help with optimization, but
> can also allow for more advanced uses (like forcing purity in monads and
> other special cases). However, maybe this is the only 'proper' way to do
> this. It would mean that ocaml becomes a fully purity-conscious language.
> .mli files are encouraged (for good reason), and if you constrain any part
> of your code to purity, any functions called by that code must also be
> pure, causing a cascade of purity annotations.

I think this can be somewhat mitigated by cross module optimization.
The compiler could record in the .cmi file that the function is
annotated as impure but happens to be pure at this point in time. The
type checker would check that impure is correct with its usage but the
optimizer would optimize for purity.

This might make it more complex but probably worth it. You get the
best of both worlds.
 
> 2. Allowing for the method I outlined, which is that impure functions can
> be constrained by the compiler even in the presence of impure signatures in
> the .mli file. The advantage here is that you don't need to change much in
> the code to get potential optimizations. It also doesn't transform ocaml in
> any meaningful way -- it simply allows for another style of programming.
> The problem is (as you mentioned), what happens if a library changes its
> implementation of a function that was not annotated with purity but was
> internally pure, and now makes it impure? Well, one approach is that if you
> annotated your code with purity, the code should break with a type error.
> You obviously had a reason to choose to annotate your code with purity.
> Choosing to use an external library's function that was NOT annotated with
> purity (but happened to be pure and therefore compiled) was not a very safe
> thing to do -- there was no guarantee that the function would stay pure. So
> maybe this isn't much of a problem after all.
> 
> 3. Another approach is to follow a process similar to 2, but to limit it
> when it comes to libraries. For example, perhaps libraries should never
> ship with/be loaded with the file that supplies function purity metadata.
> So a library would be forced to annotate its functions with their purity,
> but a regular module would not. I think that would be fair.
> 
> Now that I think about it, an external compiler-generated metadata file
> containing inferred purity information could be simplified to just modules,
> their function names, and those functions' purity level (and an md5 of the
> mli/cmi+ml file). We can't infer anything else cross-module anyway -- any
> purity information within types would have to be specified by the user.
> This could even be appended to the cmi file to ensure that the data is
> always up to date. A simple [function;purity] list would be readable even
> within a binary file.

Please don't special case files. Purity should work the same with
modules in seperate files or modules in a single file. With code from
libraries or code directly in the source and so on. It would be bad
for code to suddenly break or just behave differently because you
split the source into multiple files or libraries.

MfG
	Goswin