Re: [Caml-list] Purity in ocaml

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

On Wed, Jan 29, 2014 at 12:16:12PM -0500, Yotam Barnoy wrote:
>     > 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"?
> >
> >
> It could be. Maybe it should be let_pure, let_hpure, let_st or some such
> thing. It requires further thought, but in general I think it's easier to
> add keywords to the type domain than it is to the syntax domain.
> 
> 
> 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.
> >
> >
> That's basically what I meant to say.
> 
> I guess the issue here is that I'm proposing 2 features: purity as a
> language feature and cross-module purity optimizations as an optimization.
> These 2 features overlap, since we can't infer purity in a function
> container -- we can only do so for a function itself. So if you want to
> optimize a function container (ie. a function within another type) you have
> to annotate it yourself, at which point it becomes a language feature.
> 
> Cross-module optimization (such as cross-module inlining) is another place
> where the interface boundary is broken -- you're assuming things about the
> workings of the another module that aren't guaranteed to be right if you
> load that module dynamically. That means that the dynamic loader has to
> check that the other module hasn't changed from the version that was
> compiled against. This scheme would work for purity as well, which means
> that there isn't really a big problem -- at least no bigger than
> cross-module inlining, which is a must-have feature for performance.
> 
> Yotam

Cross-module optimization and dynamic loading are somewhat opposite
concepts. Optimizing with infered purity only works with static
linking. Dynamic linking will have to limit itself to the annotated
types to be future proove.

MfG
	Goswin