types, determination, seperate compilation and side effects

types, determination, seperate compilation and side effects

[Julian Assange]

It would be nice if the hindley-milner type system of ocaml were
extended to provide unioning of determination, world-state-changes,
mutagenic behavior etc as types. That is, if a function is discovered
to lack referential transparency, either because it has side effects
or calls functions which have side effects then that fact is reflected
in the type of the function.  This would permit the optimiser to
perform code-flow elimination accross modules (and might make flow
analysis within the same module easier).

It is quite interesting to consider multiple argument functions. In
ocaml multiple argument functions are rearranged into multiple curried
forms. Type analysis of each form, as above, could result in
elimination of that form if it has been typed as referentially
transparent and found not to contribute to the calculation it was
called from. Code flow analysis could do this already (theoretically),
but not accross seperately compiled modules.

It would be very useful for ocaml hackers to see if a non referentially
transparent type was inferred for a function (and whether the cause
was io, potential non-termination, or operation on mutables) or have
the compiler discover conflicts between functions hand annotated as
referentially transparent but inferred otherwise.

I'm not sure how functions which potentially raise exceptions should be
typed.

Mercury (souped up prolog with functional desires from Melbourne
University) supports determinacy annotations and checking, but the
methodes employed are verbose and visually unpleasant. However, the
designers do say that this has allowed them to catch several hundred
errors during the development of the Mercury compiler and given the
opimiser enough contraints to dramatically improve the speed of
generated code (and it does generate fast code in an absolute sense,
so there must be some truth in this).

Cheers,
Julian.