From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 1AEDFBB81 for ; Mon, 13 Dec 2004 14:42:45 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iBDDgi4w018641 for ; Mon, 13 Dec 2004 14:42:44 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id OAA32109 for ; Mon, 13 Dec 2004 14:42:44 +0100 (MET) Received: from mail.dcs.qmul.ac.uk (vicar.dcs.qmul.ac.uk [138.37.95.146]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iBDDghmP015381 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Mon, 13 Dec 2004 14:42:44 +0100 Received: from xenografia.plus.com ([212.159.85.26] helo=[192.168.7.2]) by mail.dcs.qmul.ac.uk with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.43) id 1CdqTK-0001W5-Jm; Mon, 13 Dec 2004 13:42:43 +0000 Message-ID: <41BD9DF9.4040408@dcs.qmul.ac.uk> Date: Mon, 13 Dec 2004 13:49:45 +0000 From: Martin Berger User-Agent: Mozilla Thunderbird 0.6 (X11/20040519) X-Accept-Language: en-us, en MIME-Version: 1.0 To: skaller@users.sourceforge.net Cc: caml-list Subject: Re: [Caml-list] environment idiom References: <9410EC84C0872141B27A2726613EF45D02A52E08@psmrdcex01.psm.pin.safeco.com> <41BB04D8.60405@andrej.com> <20041211181313.GA9656@fichte.ai.univie.ac.at> <1102809398.2611.637.camel@pelican.wigram> <20041212023636.GA12724@force.stwing.upenn.edu> <1102829608.2768.77.camel@pelican.wigram> <877e9a170412121109ec02d44@mail.gmail.com> <1102898935.2768.88.camel@pelican.wigram> <877e9a17041212180365f76e4a@mail.gmail.com> <1102916483.2768.204.camel@pelican.wigram> <877e9a17041213012926f7e18a@mail.gmail.com> <1102941011.2578.182.camel@pelican.wigram> In-Reply-To: <1102941011.2578.182.camel@pelican.wigram> X-Enigmail-Version: 0.84.0.0 X-Enigmail-Supports: pgp-inline, pgp-mime Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-DCS-Interface-Port: 465 X-DCS-Auth-User: martinb X-DCS-clamav-result: clean (1CdqTK-0001W5-Jm) X-DCS-uvscan-result: clean (1CdqTK-0001W5-Jm) X-Miltered: at nez-perce with ID 41BD9C54.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41BD9C53.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; dcs:01 qmul:01 caml-list:01 monads:01 partitioning:01 programmer's:01 misleading:01 type-based:01 dependencies:01 simonet:01 inference:01 publis:01 idiom:01 typing:01 behaviour:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: > 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