Great questions. There are indeed different definitions of the word 'pure'. What I'm going for here is very similar to what haskell does by default:
1) Purity in my definition means no side effects, including the lack of access to mutable state. That means no reading from or writing to mutable fields, strings, arrays, and refs. It also means no printing, no network messages etc.
Pure code has many advantages, particularly in functional languages. Since the result of each call to a pure function is entirely dependent on its arguments (and its closure, which by definition is constant), pure calls can be made in any order and still produce the same result. This is great for optimization, for example, for grouping allocations together.
Additionally, knowledge of purity can allow advanced optimization techniques like deforestation (
http://research.microsoft.com/apps/pubs/default.aspx?id=67493), which allows intermediate data structures to be eliminated. So, for example, a range creation that feeds a map function that feeds a fold function that outputs a value could be optimized into a single for loop, allowing all allocations to be eliminated. This is a huge performance benefit for functional languages.
Pure code is also safer. The lack of side effects means that there's less chance for complexity and interdependence -- ideas well known to functional programmers. Purity tends to cause formation of programs arranged in a star schema: impure central code, usually manipulating input, output and global state, calls out to pure functions forming the arms of the star. which do the main calculation of the program. This is because impure code can call pure code, but pure code can only call other pure code. In fact, I already program this way in ocaml, and I imagine many others do as well. It's a great way to make sure your programs don't involve unintended interactions through global state. (In haskell, you're forced to program this way because of the type system).
Finally, purity is often very useful for parallelization. Functions without side effects can easily be run in parallel in many paradigms.
It also makes sense to define a half-pure annotation to enable reuse of library functions. The classic map and fold functions don't do anything impure themselves, but they can't vouch for the higher-order functions they call. By declaring half-purity (hpure), you can now use these functions in both pure and impure context (something haskell cannot do). Any pure function that takes a higher function without restricting its purity is essentially a half-pure function.
The nice thing is, this can all be done mostly transparently. You never need to annotate anything, since the compiler will just figure out which parts of your code are pure and impure and add annotations to your type signatures.
In response to your question, a function that doesn't modify its mutable argument can be considered pure so long as it also doesn't read from said argument. This is very useful when you have a large record with some mutable fields. So long as a function reads only from the immutable fields, it's still pure. If it accesses the immutable fields, it becomes an st function, though that means it can also be called with a global reference, in which case it functions as impure in that context. If it calls an impure function directly, it becomes impure, and can no longer be called from a pure function.
2) I've been debating syntax for a long time. I've settled on pure, st, hpure, hst and unsafe in function types for now. In most cases, the programmer should not have to think of purity. The way I envision it, you write your function signatures as you do now, and the compiler would try to infer if it can make the signatures any stricter. It would save the stricter signatures into another signature file. If an extra signature file is present, the compiler will use that when compiling modules. Otherwise, it will use the regular signature file and assume every function in the module is impure (which is the default).
Sometime you will want to control the purity of functions. For example, a parallel monadic library may want to make sure the functions it calls are pure. In this case you can put in type annotations for purity. The compiler will never make functions less strict than their purity annotations.
So many times I've come across libraries where the author says, unfortunately ocaml doesn't side effects so we had to do X and hope for the best. Well, this changes that. It allows for ocaml to be as pure as haskell is when there's a need for it. Nevertheless, I don't expect pure code to become the dominant paradigm in ocaml.
3) Exceptions are considered a side effect. See this answer
http://stackoverflow.com/a/10720037. I can't say I understand all the specifics, but one can reason that unless every exception thrown by a function is caught right at its invocation (like different variants), the behavior of said function is unpredictable. Haskell's solution is to only allow exceptions to be caught by impure code, and I'm mimicking this solution, with an additional allowance for catching exceptions raised within the same function (and serving as gotos). An alternative solution is to annotate the types of functions with all the exceptions they may raise, but this becomes extremely hairy when you consider higher order functions (functions become incompatible with each other's type because they raise different exceptions), so I'd rather not go that way.
Pure code in general doesn't rely much on exceptions except to signal a catastrophic failure, and I don't see a reason to stray from that. For the most part, I don't see people programming exclusively in pure code anyway. Rather, an impure function can have pure, st and impure parts within it. For example, suppose an impure function writes to some global state, catches an exception, reads from some local state, and maps and folds pure lambdas over a collection. The function as a whole is clearly impure. However, the parts of the function that are pure can be rearranged and optimized -- the map/fold may be turned into a for loop if there are no intermediate dependencies between them and the st/impure parts. The st parts cannot be reordered - state modification to the same reference must retain its order - but they can be moved around to different areas of the function for optimization. Thus, with good cross-module information about purity, you can still do a lot within impure functions to improve performance. On the other hand, libraries for parallel computation probably want to enforce purity, and that means eschewing exceptions as well.
One issue I haven't discussed is the matter of strings and arrays. Strings are mutable by default, which means that any read of a string amounts to reading mutable state, causing at least an st annotation. One way of dealing with this is by adding an immutable string type, which could be constructed by something like "hello world"p, where the p stands for pure. Another option is that since mutation of strings is so rare, a flag could exist per type scope to signal if strings are modified anywhere in the local scope. If they're not, they can be treated as immutable within the local type scope. Type scope can be defined as the extent up to which a type is kept abstract -- if I have a module with a type t that contains a string and writes to it, but t is not fully exported, then outside of this module, nobody can write to strings. It would also be useful to have immutable arrays, which can be turned into mutable arrays only after optimization.
I hope this clarifies things.
-Yotam