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 DA74B80130 for ; Tue, 9 May 2017 19:16:08 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yminsky@janestreet.com; spf=Pass smtp.mailfrom=yminsky@janestreet.com; spf=None smtp.helo=postmaster@mxout1.mail.janestreet.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yminsky@janestreet.com) identity=pra; client-ip=38.105.200.78; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="yminsky@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yminsky@janestreet.com designates 38.105.200.78 as permitted sender) identity=mailfrom; client-ip=38.105.200.78; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="yminsky@janestreet.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mxout1.mail.janestreet.com) identity=helo; client-ip=38.105.200.78; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="postmaster@mxout1.mail.janestreet.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AvhR4XR8CD0S4Wf9uRHKM819IXTAuvvDOBiVQ1KB2?= =?us-ascii?q?1egcTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/?= =?us-ascii?q?8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1?= =?us-ascii?q?Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+?= =?us-ascii?q?RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTF?= =?us-ascii?q?UACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiC?= =?us-ascii?q?gZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsYSmpPXshfWS9PDJ6i?= =?us-ascii?q?YYQTAOQMJvpYr5DnqlcSsReyGQuhCeXywTFInH/22qg63vwjHg7cxgwgGNQOu2?= =?us-ascii?q?nTotX0MqcSSuO1zanVxjjEb/JW3Db96I7TchAiofCBRrBwftDXyUYxDAPFkk+Q?= =?us-ascii?q?ppL7MDOJzOgCr2+b7+95WO+plmUppQZxoj21ycctjInEnoUVylPB9SV4woY5P9?= =?us-ascii?q?q4SFR0YdOiDZBetDmaOpN4T84hWW1kpTo2x70ctZKlYCQG1I4ryhzcZvCfbYSE?= =?us-ascii?q?/hbuWPySLDp4nn5pZq+zihSo/US9zuDxUs+520tQoCVfiNnDrHUN2gTT6seZTv?= =?us-ascii?q?t9+V+s2TOA1gDU9+FEPV04mbDeK5E7w74wkoAfsUbZES/whkr2l7OWdl869ee2?= =?us-ascii?q?9+TreKnpppiZN4NsiwH+NLohmtCnDOk2MQUCRXWX9fi82bH540H1XKlGguc0n6?= =?us-ascii?q?TaqJzaIN4Upq+9Aw9byIYj7BO/Ai+m0dQdnHkHKklFeBGHjoXyOVHBOvb4Aumk?= =?us-ascii?q?g1Swijdk2e7JPqH7DprRKXjDla/tfaxh5E5E1Aoz0ddf6opIBb4bJfLzXlb9tN?= =?us-ascii?q?jZDh8iLwy52P3nCdV41oMGQ22DGK6ZMKXIsV+J/O0jOeeMZJVG8Ar6ft8h6vGm?= =?us-ascii?q?2Xg9lFA1eqqs3JlRb2q3SLAuKEWebHXhmP8cFH8D+wwzUKrmhRnKGzVaYnL3W6?= =?us-ascii?q?Mn+hk6DpinBMHNXMrl1LeI2SP+GpxNekhHDEqNGDHmbdPAE8YFciWUaupglCcH?= =?us-ascii?q?RPD1Woog0wqtpSf4wrxqNfbO9yAE85nk0Y4xr8TVlBV60DV4D82D2nmAQ21l1j?= =?us-ascii?q?cBQT4y9Lpyqkt8zhGEy6cu0NJCEtkG1vpTVQFyEJ/a1O9rQ4TjXwPHZdSYYFSv?= =?us-ascii?q?RNi9HSs8Q853yNgLNRUuU+6+hwzOinL5S4QekKaGUdltqvrR?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AIBAB9+BFZfU7IaSZdHQEFAQsBGAEFA?= =?us-ascii?q?QsBhAyBDAeDYptvlXKCDyyFdAICAoRlB0EWAQEBAQEBAQEBAQESAQELFAhXgjM?= =?us-ascii?q?iAYJAAQIDIx0BATgPCwsNAgImAgIiEgEFARwGARKKIQMLph4/ix1rgiaDCQEBB?= =?us-ascii?q?YdhAQEBBwEBAQEBAQEZCBJ5hVSEeYJ8hHGCX54KhxyDM4hKglmIKYZpkngUH4E?= =?us-ascii?q?VJgWBNi8gCBkVXwaERg8cgX9aiHQBAQE?= X-IPAS-Result: =?us-ascii?q?A0AIBAB9+BFZfU7IaSZdHQEFAQsBGAEFAQsBhAyBDAeDYpt?= =?us-ascii?q?vlXKCDyyFdAICAoRlB0EWAQEBAQEBAQEBAQESAQELFAhXgjMiAYJAAQIDIx0BA?= =?us-ascii?q?TgPCwsNAgImAgIiEgEFARwGARKKIQMLph4/ix1rgiaDCQEBBYdhAQEBBwEBAQE?= =?us-ascii?q?BAQEZCBJ5hVSEeYJ8hHGCX54KhxyDM4hKglmIKYZpkngUH4EVJgWBNi8gCBkVX?= =?us-ascii?q?waERg8cgX9aiHQBAQE?= X-IronPort-AV: E=Sophos;i="5.38,315,1491256800"; d="scan'208";a="272373402" Received: from mxout1.mail.janestreet.com ([38.105.200.78]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 09 May 2017 19:16:07 +0200 Received: from [172.27.56.106] (helo=tot-qpr-mailcore2) by mxout1.mail.janestreet.com with esmtps (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256) (Exim 4.89) (envelope-from ) id 1d88k2-000350-L7 for caml-list@inria.fr; Tue, 09 May 2017 13:16:06 -0400 X-JS-Flow: external X-JS-Scanner-attachment: (ok) No attachments Received: by tot-qpr-mailcore2 with ocaml/mailcore/mailcore 1.0+90 (160ed8e8fef2) (envelope-from ) id BZEflW-AGic8Y-UG; 2017-05-09 13:16:06.646278-04:00 Received: from mail-ua0-f199.google.com ([209.85.217.199]) by mxgoog1.mail.janestreet.com with esmtps (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128) (Exim 4.89) (envelope-from ) id 1d88k2-0000Gv-Jy for caml-list@inria.fr; Tue, 09 May 2017 13:16:06 -0400 Received: by mail-ua0-f199.google.com with SMTP id j62so3275928uaj.12 for ; Tue, 09 May 2017 10:16:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=janestreet.com; s=google; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :content-transfer-encoding; bh=0l1eMavKIumnylleHa/4JRFP/8pYoej2fNOMWrGN6BI=; b=1KUakyEyLO43dcrTu/7T398AdWoC4Pd76q+/K92L/BQCQ+6YNvrgvtNVsS9DzlFjXv Od2jubCIEwsDctWkzkKzk6vhn5R4cUO4bReyiv/xDXbW9fUpzsOGTM/SxDfva1eb6s/d KxPyNPmv1ybDvMc6xqztOIxrWE8n9DEqXwtac= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:content-transfer-encoding; bh=0l1eMavKIumnylleHa/4JRFP/8pYoej2fNOMWrGN6BI=; b=VBqeBwmmT0KolbKmc8uF/myrcZIfOV3wVmONNhmUlUXvqlW/hlxLVbes+8xVsIkIwv tcTeXthM7HbW+Rh9vYnK4Lk6i3u13T0XFI/28scHEovBZaXXu0y0qhfbVgYhloJJdoiG XPqJJPCVlfrwSTSo4Lsx0HTnjJrmShKNSeMI8AXcr0BuF4U/CPLVfv4y8feMA7PmzyDe gGLb8xeI4ZpK3p9fLu0j+EupqA1/oSF59z+jFXEmA3S1Pv1k5yx0KdAaKRt8lubGxPZs JMlkBMumNdw+2TV8JoBBQK9PggcRuZJIF8p27I6lim50ALd3J3Cinq6CGRB8/FrgO1xW bGVg== X-Gm-Message-State: AODbwcD7KQz+Oz01xlhQE5OiYyom8drQmqk0w2IRMH4u+ZWjJI+22+pj dBtC8SVbpAuKokD0dujMlgBB0yJwOmKPPk0jEjIko3PVzDj2s8OIvo3rHB4YleoNYOvDfLEOg7n 3BgKH8UUJTbsVGjtK X-Received: by 10.159.48.144 with SMTP id j16mr588211uab.131.1494350165909; Tue, 09 May 2017 10:16:05 -0700 (PDT) X-Received: by 10.159.48.144 with SMTP id j16mr588203uab.131.1494350165562; Tue, 09 May 2017 10:16:05 -0700 (PDT) MIME-Version: 1.0 Received: by 10.31.236.197 with HTTP; Tue, 9 May 2017 10:15:45 -0700 (PDT) In-Reply-To: <20170509134051.GA3873@Magus.localnet> References: <5af3b33f-d4eb-05dc-d774-b42f63275776@umpa-net.de> <20170509134051.GA3873@Magus.localnet> From:Yaron Minsky Date: Tue, 9 May 2017 13:15:45 -0400 Message-ID: To:Oleg , choeger@umpa-net.de, "caml-list@inria.fr" , Yaron Minsky , Anil Madhavapeddy Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-JS-Exim-Data-Received: 2017-05-09 13:16:06-0400 X-JS-Processed-by: mailcore Subject: Re: [Caml-list] Transforming side-effects to a monad I like monadic encodings of concurrency because they make the places at which interleavings can occur explicit in the types and the code. What I've seen from more direct encodings does not have this killer feature. I don't want to go back to the world of mutexes and semaphores... Maybe some version of algebraic effects plus appropriate tracking in the type system will solve all the problems. But for now, I like my monads. y On Tue, May 9, 2017 at 9:40 AM, Oleg wrote: > > Back on Mar 24, Christoph H=C3=B6ger wrote: > >> Assume a simple OCaml program with two primitives that can cause >> side-effects: > >> let counter =3D ref 0 >> let incr x =3D counter :=3D !counter + x ; !counter >> let put n =3D counter :=3D n; !counter >> put (5 + let f x =3D incr x in f 3) > >> This example can be transformed into a pure program using a counter >> monad (using ppx_monadic syntax): > >> do_; >> i <-- let f x =3D incr x in f 3 ; >> p <-- put (5 + i) >> return p > >> For a suitable definition of bind and return, both programs behave >> equivalently. My question is: How can one automatically translate a >> program of the former kind to the latter? > > More recently (Apr 29), Yaron Minsky, contrasting his view with the > moderate position by Anil Madhavapeddy, spoke very highly about > monads. > > One really wonders why this obsession with monads. Why to use monadic > encoding if effects can be expressed directly? Is really > >> do_; >> i <-- let f x =3D incr x in f 3 ; >> p <-- put (5 + i) >> return p > > so much better than > let res =3D put (int 5 + let f x =3D incr x in f 3) > > ? > > One can say that the do-notation lets us use the other ways to > implement counters. Well, so does the direct notation: > let res =3D put (int 5 + let f x =3D incr x in f 3) > This is truly OCaml code, with no PPX or other pre-processors. > > It all depends on how the `primitives' int, put, incr are > defined. They can use a reference cell or pass the state or talk to a > remote computer via some RPC. If we abstract over the primitives, the > same expression can be evaluated with different models of > `counters'. Incidentally, we did not have to abstract over `let' in > this example. And we did not have to abstract over functions. Very > often our DSL can be kept to first order. Embedding into expressive > OCaml compensates. Incidentally, types really help to tell which > expression belongs to which `level' -- effectful DSL or OCaml (which > acts as a higher-order, typed `macro' language). > > The recent article > http://okmij.org/ftp/tagless-final/nondet-effect.html > > presents quite a bit more challenging example, of > non-determinism. Once can write literally Curry (*) code in OCaml -- > with no PPX or other preprocessors, using multiple interpretations of > non-determinism. All works in vanilla OCaml 4.04. We don't have to > put up with functors: first-class modules really help. The modular > implicits will help even more, by putting the `implementation' > argument out of sight. > > (*) Curry is a functional-logic programming language, with built-in > non-determinism