From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 4AD9A7EE6B for ; Thu, 28 Nov 2013 10:49:10 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel@kerneis.info) identity=pra; client-ip=176.31.113.173; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel@kerneis.info"; x-sender="gabriel@kerneis.info"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel@kerneis.info designates 176.31.113.173 as permitted sender) identity=mailfrom; client-ip=176.31.113.173; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel@kerneis.info"; x-sender="gabriel@kerneis.info"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@wanbli.kerneis.info designates 176.31.113.173 as permitted sender) identity=helo; client-ip=176.31.113.173; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel@kerneis.info"; x-sender="postmaster@wanbli.kerneis.info"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhoFAOEQl1KwH3Gt/2dsb2JhbABZgwe5UYEfFnSCJQEBBToGAQE3AQ8LGAkTEg8FKDSIBQGuP4RSAQWNEREGjwcHFoMKgROOdIkihjYQi06DKQ X-IPAS-Result: AhoFAOEQl1KwH3Gt/2dsb2JhbABZgwe5UYEfFnSCJQEBBToGAQE3AQ8LGAkTEg8FKDSIBQGuP4RSAQWNEREGjwcHFoMKgROOdIkihjYQi06DKQ X-IronPort-AV: E=Sophos;i="4.93,790,1378850400"; d="scan'208";a="45855409" Received: from wanbli.kerneis.info ([176.31.113.173]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 28 Nov 2013 10:49:02 +0100 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=kerneis.info; s=wanbli-rsa1; h=In-Reply-To:Content-Type:MIME-Version:References:Message-ID:Subject:Cc:To:From:Date; bh=FVnqLpf/dxRt+CgfSu2UvGzFQ0UnDBUidF7AaCYcj8g=; b=mf0ZFioqLoL1FrBpu/5w0ornGzSwFGPb9+RQiN8CTvAkFWmn2cZK1Fpo3IWdsuGNSunVad3EYM81blE3iOLu0VJuLuhrNU68xWAAHBcz5lzTaeAFL6N+oWq9ZnzlNgdA7ys9G+sUWZvg0LcJJT4wHJYq4aHQGa6zjqcRReJ797M=; Received: from [2.219.70.22] (helo=wacehi.kerneis.info) by wanbli.kerneis.info with esmtpsa (TLS1.2:DHE_RSA_AES_128_CBC_SHA1:128) (Exim 4.80) (envelope-from ) id 1VlyDU-0005aD-IR; Thu, 28 Nov 2013 09:49:00 +0000 Received: from gabriel by wacehi.kerneis.info with local (Exim 4.80) (envelope-from ) id 1VlyDT-0001K4-JI; Thu, 28 Nov 2013 09:48:59 +0000 Date: Thu, 28 Nov 2013 09:48:59 +0000 From: Gabriel Kerneis To: oleg@okmij.org Cc: caml-list@inria.fr Message-ID: <20131128094859.GB4052@kerneis.info> References: <20131127073030.28963.qmail@www1.g3.pair.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20131127073030.28963.qmail@www1.g3.pair.com> User-Agent: Mutt/1.5.21 (2010-09-15) X-SA-Exim-Connect-IP: 2.219.70.22 X-SA-Exim-Mail-From: gabriel@kerneis.info X-SA-Exim-Scanned: No (on wanbli.kerneis.info); SAEximRunCond expanded to false Subject: Re: [Caml-list] ANN: improved BER MetaOCaml N101, for OCaml 4.01 Hi Oleg, On Wed, Nov 27, 2013 at 07:30:30AM -0000, oleg@okmij.org wrote: > The scope extrusion check first introduced in BER N100 made it > possible to remove environment classifiers while still preserving the > static guarantee: if the generator finishes successfully, the > generated code is well-typed and well-scoped. Environment classifiers > ensured well-scopedness when type-checking the generator -- but only > for pure generators. The scope extrusion check is executed when the > generator is run; however the check is comprehensive. Scope extrusion > is always caught, and caught early, whether the generator is effectful > or not. I'm not sure I understand correctly the difference between open and close code, and what is the challenge with effects. Could you please give examples of: (1) a pure generator for well-typed, well-scoped open code, (2) a pure generator for well-typed, ill-scoped open code, (3) an effectful generator for well-typed, ill-scoped open code. I assume (2) would be caught statically by BER N100, and (3) dynamically by BER N101. But what would happen for (2) with BER N100? Many thanks, -- Gabriel