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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 36B197FFD7 for ; Sun, 15 Jan 2017 09:55:43 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=oleg@okmij.org; spf=Pass smtp.mailfrom=oleg@okmij.org; spf=None smtp.helo=postmaster@mail1.g3.pair.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of oleg@okmij.org) identity=pra; client-ip=66.39.3.114; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of oleg@okmij.org designates 66.39.3.114 as permitted sender) identity=mailfrom; client-ip=66.39.3.114; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail1.g3.pair.com) identity=helo; client-ip=66.39.3.114; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="postmaster@mail1.g3.pair.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AfcaCfRQM+QxkYUfxYPwf8ZPTRdpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa68YxaN2/xhgRfzUJnB7Loc0qyN4vymAjBLvsfJmUtBWaQEbwUCh8?= =?us-ascii?q?QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6?= =?us-ascii?q?OPn+FJLMgMSrzeCy/IDYbxlViDanb75/KBq7oR/fu8QZjodvKKI8wQbVr3VVfO?= =?us-ascii?q?hb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnY?= =?us-ascii?q?UAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhS?= =?us-ascii?q?waMTMy7WPZhdFqjK9DrhyvpwJxzZPXbo6aKPVxY6HSct0BSGpdQspcTTBNDp+m?= =?us-ascii?q?YocRCecKIOZWr5P6p1sLtRawHA2sC/3gyjRVgXL22qk63PouEQzd2wwgHNcOsH?= =?us-ascii?q?XWrNnvM6cSS++1wbDOwD7ebP1WwS/w5YnJfxw7r/yBWah8fMTLxUUyCg/IgU2c?= =?us-ascii?q?pZL5Mz+LzOgBrXWX4uV6We6xhWMrtxt9riWvy8swjITCm5gbxUre9SpjxYY4Pd?= =?us-ascii?q?24R1B/Yd6jCJZQsjuVN4pyQs8/WW1otyg3xqceuZGhfSgK0o4ryALYa/yCa4SI?= =?us-ascii?q?4xTjW/iNITpghX9oeaizihi2/ES6xODwTNS43EtFoyZdl9nDrHEN1xjd6sidTf?= =?us-ascii?q?t9+1+s2TGL1w/N5eFJOkc0laneK54gwL48jJ0TsV7MHiPugkX5kLeWdlk4+uiv?= =?us-ascii?q?8+nofq/pppqYN4NtjgH+M78umtCkDOQjMgkOWnCb9v6m2L3i+035WrRKgecsnq?= =?us-ascii?q?nXqpCJbfgc86GwCRVU34Jl8B2/Ai2ryvwXmHAGKBROfxfUoZLuPgTpJP33RaO4?= =?us-ascii?q?h1mjuDBowvHEeLr7DcOefTD4jL79cOMluAZnww0pwIUH6g=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0B3AgDIN3tYhnIDJ0JdGwEBAQMBAQEJA?= =?us-ascii?q?QEBFgEBAQMBAQEJAQEBgw4BAQEBAX6BCY5KkSCXNyKGAAKCGEMUAQEBAQEBAQE?= =?us-ascii?q?BAQESAQEBCgkLCh0wgjMZgh4BBAE6PwUWITQFhlqCfQcBshGJfAEBCAEBAQEkh?= =?us-ascii?q?kSEaIJrhRCCMQWQIIsaglCEDYp1DYNKjSOSbDaBSCoIOoRIgXlkiHgBAQE?= X-IPAS-Result: =?us-ascii?q?A0B3AgDIN3tYhnIDJ0JdGwEBAQMBAQEJAQEBFgEBAQMBAQE?= =?us-ascii?q?JAQEBgw4BAQEBAX6BCY5KkSCXNyKGAAKCGEMUAQEBAQEBAQEBAQESAQEBCgkLC?= =?us-ascii?q?h0wgjMZgh4BBAE6PwUWITQFhlqCfQcBshGJfAEBCAEBAQEkhkSEaIJrhRCCMQW?= =?us-ascii?q?QIIsaglCEDYp1DYNKjSOSbDaBSCoIOoRIgXlkiHgBAQE?= X-IronPort-AV: E=Sophos;i="5.33,232,1477954800"; d="scan'208";a="209179382" Received: from mail1.g3.pair.com ([66.39.3.114]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 15 Jan 2017 09:55:41 +0100 Received: from Magus.localnet (150.230.214.202.rev.vmobile.jp [202.214.230.150]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by mail1.g3.pair.com (Postfix) with ESMTPSA id 14EBA3FB3F1; Sun, 15 Jan 2017 03:55:36 -0500 (EST) Date: Sun, 15 Jan 2017 17:55:45 +0900 From: Oleg To: gabriel.scherer@gmail.com Cc: caml-list@inria.fr Message-ID: <20170115085545.GA1427@Magus.localnet> Mail-Followup-To: Oleg , gabriel.scherer@gmail.com, caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.6.1 (2016-04-27) Subject: Re: [Caml-list] ANN: BER MetaOCaml N104, for OCaml 4.04.0 Thank you, Gabriel. Sorry for a late reply. > I wondered why attributes were used instead of > extensions. I have thought about this issue and have documented the reasoning behind settling on attributes in the NOTES.txt file of the metalib directory. That file describes many other design decisions, possible alternatives, and future work. > In my book, (e [@attr]) is supposed to be an OCaml term > that behaves as the expression (e), with some extra (tooling- or > optimization- related) expression of intent. On the contrary, [%ext e] > is allowed to have any semantics at all. That is precisely the reason. The type-checker traverses an expression several times (e.g., to collect variables, to check expansiveness, etc.) It totally ignores the extension nodes. But it traverses inside the nodes with attached attributes. This is the behavior I want. The expression inside the brackets is meant to be a regular OCaml expression (only evaluated with a `delay', so to speak), so the typechecker should go inside and check it, etc. If I used extensions, I would need to emulate these extra typechecking traversals somehow. Incidentally, staging literature very often calls brackets and escapes ``staging _annotations_''. There is a reason for that. > One interesting thing with the addition of the two new syntactic > classes "pattern" and "value" is that, from a syntactic point of view, > the idea of using extensions directly instead of home-grown syntax > starts looking more reasonable: [%quote e], [%quote.pat e], > [%quote.val e] (plus long forms metaocaml.quote*). Moving from .< e >. > to [%quote e] is still arguably a bad deal for readability, but for > the other two forms it would actually be an improvement over the > current syntax. So I guess the benefit would depend a lot on how often > these two new forms end up being used by MetaOCaml programmers. Using > the extension syntax directly would certainly simplify a few things > around MetaOCaml -- zero need for non-standard parsing, for example. I fully agree with that. [%quote.pat e] is certainly very appealing. Perhaps we can check carefully how OCaml traverses expressions (besides the normal typechecking pass) and if using extension will be sufficient in the end. If so, one can easily switch to it. > It is interesting that you mention that "function" allows to > easily represent sets of clauses as expressions, as I was recently > thinking about which kind of constructions would be made possible by > taking "sets of clauses" as a first-class syntactic category. We can discuss this further in a couple of days. Some unification will be nice. > I was professionally obligated to remark your formulation on > where (genlet exp) actually places its definition: "The `let` is > inserted right under the binder for the "latest" free variable > contained in `exp`". This is exactly the style of placement used in > sum-equivalence algorithms (and, I suppose, work on partial > evaluation), typically the delimited-control-using presentation of > "Extensional normalisation and type-directed partial evaluation for > typed lambda calculus with sums" by Vincent Balat, Roberto Di Cosmo > and Marcelo Fiore, 2004. Interestingly, these algorithms do not (only) > place let-bindings in this way, but also case statements -- they want > the case-distinction on the bound value to have as large a scope as > possible. This suggests that maybe the "finding the earliest place to > introduce an expression" is a really useful primitive to have for > metaprogramming, and that your "genlet" could be reconstructed from > it, but right now I don't see how to expose it without letting the > user do delimited control -- which is what you started from. As you probably expect, I am well familiar with Balat works and NBE and the problem of placing let and case statements. Before I used delimited control. But the current implementation of MetaOCaml does something different. Internally, a code value is represented as AST along with a set of `virtual' let-bindings. That is, essentially in the form let x1 = e1 and x2 = e2 ... in e That should remind you of `answers' used in call-by-need calculi. The virtual bindings are converted to real let-bindings when the binder is applied to the expression. If the bound variable occurs within ei, the corresponding virtual let-binding must be made real. Others remain virtual and float out. Of course there are complications: an expression may be spliced in several times. So, one has to deal with duplicates. Further, genlet may nest (that is, each ei itself contains virtual let-bindings. When actualizing let-bindings, we have to `straighten them up'). The comments in the main code file trx.ml describe the algorithm in some detail. It should be written up of course. Again, this is something we can talk about in a day.