Re: [Caml-list] environment idiom

[Martin Berger <martinb@dcs.qmul.ac.uk>]

> To avoid that I want to know far more precisely how to
> characterise things . I know what a function is, so the
> problem is that I do NOT know exactly what 'code' is :)

in my opinion, what you want can only been obtained -- and has
been obtained by now -- when you leave functional thinking
behind. the problem with functional thinking, and there are
good historical and sociological reasons for its preponderance,
is that it starts from functional behaviour, realises that
there's certain areas it cannot adequatly deal with (eg state,
jumps and concurrency) and adds them as an afterthough later,
for example by way of monads.

we know much better now that concurrency is indeed fundamental
and state, jumps and functional behaviour are but well
behaved special cases of concurrency. The good thing is that these
very well behaved special cases of concurrency can be characterised
by types and the types for the functional fragment of concurrency
stand out in that they are the only known types where every type is
either a data flow source or a data flow sink. this is at the heart
of why functional programming is much easier than stateful programming,
but also the cause of its limitations.

this viewpoint has been explored powerfully in

   Noninterference through Flow Analysis
   http://www.doc.ic.ac.uk/~yoshida/paper/noninterference.ps

this new typing discipline and its refinemend into types for secure
information flow give a very finegrained partitioning of programs
into parts that depend or do not depend on each other, but in a unified
way. the degree of finegrainedness can be tune to the programmer's needs
by the choice of security lattice (although speaking about security in
this context maybe a bit misleading as it's really about uniform
type-based specifications of program dependencies). This is very
powerful and has been applied to a wide range of language in

   A Uniform Type Structure for Secure Information Flow
   http://www.doc.ic.ac.uk/~yoshida/paper/ifa_long.ps

Francois Potter and Vincent Simonet have applied some of these ideas to ML, cf

   Information flow inference for ML
   http://pauillac.inria.fr/~fpottier/publis/fpottier-simonet-toplas.ps.gz

so these ideas are beginning to trickle down, but it's still mostly on the
drawing board.

martin