Obviously the purity of a higher order function can be dependent on
the purity of its arguments. You need a syntax for the type of a
function that can reflect that.

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.

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.

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)

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.

I think that would be a mistake. Exceptions are wide spread in ocaml.
By not annotating types with their exceptions you MAKE them side
effects because they become unpredictable.

On the other hand if types are annotated with the exceptions they
throw then they become just another return value and become pure.
Same input, same exception every time.

True this would complicate the type of functions because the return
type would be a pair of successfull type and exceptions. You need a
syntax for the type that allows the return type to be a combination of
the argument types, like:

val map : ('a -> 'b ['c] ) -> 'a list -> 'b list ['c]
val mapmap : ('a -> 'b ['c] ) ('b -> 'd ['e] ) -> 'a list -> 'd list ['c | 'e]

This will be hairy for purity, too, or even more so. You need ways to
say that the combined purity is the least pure of the inputs. Or with
to function arguments the purity is the result of passing one function
to the other. And so on.

Then again consider this code:

let f () = raise Not_found
val f : unit -> 'a [Not_found]

let g fn x = try fn x with Not_found -> Empty
val g : ('a -> 'b [< Not_found as 'c | 'd]) -> 'b [ Empty if 'c | 'd]

g takes a function that may raise Not_found or 'd. G then may itself
raise Empty (only if the function can raise Not_found though) or 'd.

let h fn1 fn2 x = fn2 fn1 x
val h : ('a -> 'b [< Not_found as 'c | 'd]) ->
        (('a -> 'b [< Not_found as 'c | 'd]) -> 'b [ Empty if 'c | 'd]) ->
        'a -> 'b [ Empty if 'c | 'd])

let h2 = h f g
val h2: 'a -> 'b [Empty]

Much of the stdlib uses exceptions. So you eigther have to rewrite it
to be pure or it will be too hard to write pure code.

I like phantom types for that. But that gets hairy with containers.
E.g. a Hashtbl of strings can be itself mutable or contain mutable
strings or both. So the type paramters of the hashtbl need phantom
types too. And thats where my ocaml magic broke down when I tried to
generalize that.