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 2E9947EE89 for ; Wed, 25 Oct 2017 15:36:50 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ivg@ieee.org; spf=Pass smtp.mailfrom=ivg@ieee.org; spf=None smtp.helo=postmaster@mail-yw0-f171.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of ivg@ieee.org) identity=pra; client-ip=209.85.161.171; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of ivg@ieee.org designates 209.85.161.171 as permitted sender) identity=mailfrom; client-ip=209.85.161.171; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.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@mail-yw0-f171.google.com) identity=helo; client-ip=209.85.161.171; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="postmaster@mail-yw0-f171.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Aaaz9oBQj+F0kBSRaf01vRlS0adpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa67bRGN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8?= =?us-ascii?q?QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnY6Uy/yPgtt?= =?us-ascii?q?J+nzBpWaz4Huj7jzqNXvZFACvju2YbpoIF2J6yCX/usRh4Z5YO5l0BrColNBfe?= =?us-ascii?q?Jb1WJhY1WJkECvyN23+ctC7S1W890m68leWqX7Y79wGb1GAxwnPm04osrxuk+Q?= =?us-ascii?q?HkO0+nIAXzBOwVJzCA/f4US/B8+pvw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CWAQATkvBZh6uhVdFcHRgHDAEFAQsBh?= =?us-ascii?q?BhuJweDc4E2l3SBeoJ7klmCGANcCiWEAQGBFAKEZQdDFAEBAQEBAQEBAQEBEgE?= =?us-ascii?q?BAQgNCQgoL4I4BQEeAQWCPAEEASMEGQEBNwEPCQILNwICIhIBBQEcBhMIEol5B?= =?us-ascii?q?QgQizyRG0CLIWuBbTqDCAEBBYgBAQEBAQYBAQEBAQEBARgIEoMcggeBUIUThF5?= =?us-ascii?q?UgmeCYZh7iH2HZYNkg2WFSYIwQpA0i22KABQFH4EVDyeBfIEHCEk1BoIZAQEBD?= =?us-ascii?q?QmCUxAMggMkNgEBAQGJVG+BVQEBAQ?= X-IPAS-Result: =?us-ascii?q?A0CWAQATkvBZh6uhVdFcHRgHDAEFAQsBhBhuJweDc4E2l3S?= =?us-ascii?q?BeoJ7klmCGANcCiWEAQGBFAKEZQdDFAEBAQEBAQEBAQEBEgEBAQgNCQgoL4I4B?= =?us-ascii?q?QEeAQWCPAEEASMEGQEBNwEPCQILNwICIhIBBQEcBhMIEol5BQgQizyRG0CLIWu?= =?us-ascii?q?BbTqDCAEBBYgBAQEBAQYBAQEBAQEBARgIEoMcggeBUIUThF5UgmeCYZh7iH2HZ?= =?us-ascii?q?YNkg2WFSYIwQpA0i22KABQFH4EVDyeBfIEHCEk1BoIZAQEBDQmCUxAMggMkNgE?= =?us-ascii?q?BAQGJVG+BVQEBAQ?= X-IronPort-AV: E=Sophos;i="5.43,431,1503352800"; d="scan'208,217";a="242335057" Received: from mail-yw0-f171.google.com ([209.85.161.171]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 25 Oct 2017 15:36:48 +0200 Received: by mail-yw0-f171.google.com with SMTP id w5so18001065ywg.11 for ; Wed, 25 Oct 2017 06:36:48 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=ieee-org.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=R0+MD/+TE0L+N65vlIBIBhVkaxOM+gh3gEmaF2Tu3wA=; b=Eieku5DEoqMjQzh0tcXlvCmV89s7qGDETj6UrBCg3LJdvsXLQCs/u+KYWvYILI0Rbf 9zXPXceip8ZV3S1V7HC5xhSIdoiVOWNXBhjHmPJOcbACPvVVL864IlWoWv8uqgJb/Jiw VxlRjhyRsdBtc4qFFPxuraRQ8zN5WVKyNSyKVpJx12Lwh0CJwUhgMyfQiEqMbrYSBPp8 OEALi25fKQLJYk/Hfeau7LqKFzXNiJNXa1AaqAsYZdNikAGVlkqk65B8VRCvuaqPLD4b oF5R6KDVq0eN6n42yMZP1HbNOCrUPPbn1mtj458P4xqJLVnntJVng5SyqwPyBZhar6Zy a3Jg== 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:cc; bh=R0+MD/+TE0L+N65vlIBIBhVkaxOM+gh3gEmaF2Tu3wA=; b=flw8U5bLP+kxhQTt1Ni0cbftWgQ6v7WvuU8uqz0nkKJSZqL/moP9c3/Pu0j6BiM7Oi M9daR8KU56Yg3K/IzBBuLQlNzzxbQXeoIMKfB2ieqZY1dfYKtfqqZyf2OqFkYYIZayKR eLaS9t0ELzFSSxhc0d+eV4GCJmNlsRQySyEtPZhYC10GxKZKPoPGaeliphgQcdP1H8Sn 3FmVOGj2T8JMSJWzYyfVHLASwWYA+Uu/POrDRFTrETPlWhMjNHrgYua2Q09yEk0WCnt1 U8D1hh/k//sYAYJBAL3uSaA+4gspJQvZLAClzFOEvY84cEugC0fKbC6EdqgDzDk+GxXh 1s6w== X-Gm-Message-State: AMCzsaWZcYWKs7cNXjcHAug82r35yiuA5H8jFEyxH16iVqfnyTYZAZrO gV+yxdQYxpOGPJUErcCMnGGTe34jTUm4+UkXN9XpZQ== X-Google-Smtp-Source: ABhQp+RPbdEr2DtR/+dBNLQN9Ew/wtJeUD1sk2J6TcNkaKSprCNVwXvRWo0p6C++4W98JYgRo2pmT89akdrgFnIxoeA= X-Received: by 10.129.30.148 with SMTP id e142mr12842031ywe.117.1508938606157; Wed, 25 Oct 2017 06:36:46 -0700 (PDT) MIME-Version: 1.0 Received: by 10.129.174.33 with HTTP; Wed, 25 Oct 2017 06:36:45 -0700 (PDT) In-Reply-To: <20171025083530.gvggcenrgxolduse@annexia.org> References: <86o9p2ywgc.fsf@gmail.com> <20171020113815.GD32138@nunchakus.loria.fr> <20171024133026.uovvzdbnamnzoknv@annexia.org> <20171025083530.gvggcenrgxolduse@annexia.org> From: Ivan Gotovchits Date: Wed, 25 Oct 2017 09:36:45 -0400 Message-ID: To: "Richard W.M. Jones" Cc: "Petter A. Urkedal" , ptoscano@redhat.com, caml-list Content-Type: multipart/alternative; boundary="001a1142ecd69bd03b055c5f2549" Subject: Re: [Caml-list] What if exn was not an open type? --001a1142ecd69bd03b055c5f2549 Content-Type: text/plain; charset="UTF-8" On Wed, Oct 25, 2017 at 4:35 AM, Richard W.M. Jones wrote: > > Having said all that I was writing a little ML language last > year and I tried to implement a return statement, but it was very > awkward to work out how to map that to my lambda calculus, so > I understand how return statements are rather difficult to implement > in practice. > > Rich. > > The return statement is in fact a tamed exception, as it provides an exceptional, i.e., a non-local control flow. However, exceptions are not first class citizens in functional programming languages as they are not explicitly represented in typed lambda calculus, and are not really represented in the type system (in a sence that an expression with and without exception has the same type). Thus dealing with expressions that may raise an exception is hard, as well as dealing with any expression that has a side effect. OCaml multicore project is actually bringing more than the multicore support, they also reify the effect system into the language. Thus exceptions, as well as the return statements, can be soon easily implemented on top of the effect system and can be reasoned in a much more natural way. With all that said, safe and first class exceptions can be implemented in plain OCaml, or any other functional programming language that provides higher order polymorphism (type classes, functors, etc). The limited form of an exception can be implemented even without it. As it was already noticed, the Maybe monad, as well as the Error monad, or any other monad that reifies non-total computations can be used to implement a poor man return statement. The problem is that when one computation yields the null value, the rest of the computation chain is still evaluated. This is not a big issue if a chain is written manually (i.e., is a block of code, like in your example), but it could be serious if the chain is very long (i.e., processing a big list), or even worse infininte. If the problem with a list of computations can be solved on the monad implementation (as we do in the [Monads][2] library), the problem with the infinite computation can be easily addressed in a non-total monad. The answer is to use the continuation passing style (CPS). We can use delimited continuations (as in the upcoming multicore), or we can use plain non-delimited continuations. The rough idea, is that if you have function that needs to escape the computation prematurely, you can pass a continuation to that function, e.g., let do_stuff return = if world_is_bad then return None else if moon_phase_is_bad then return None else return (compute_some_stuff ()) You may notice, that we still need the else statement as our return function has type `'a -> 'a`, but for the non-local return we need something of type `'a -> 'b`, to implement this we need to switch to the continuation passing style, where each computation is a continuation, i.e., a function of type `('a -> 'b) -> 'b`. For example, this is how the List.fold function will look in the CPS: let fold xs ~init ~f = let rec loop xs k = match xs with | [] -> k | x :: xs -> fun k' -> k (fun a -> loop xs (f a x) k') in loop xs (fun k -> k init) Programming in this style directly is a little bit cubersome, but the good news, is that the continuation passing style can be encoded as a monad. The [Continuation monad][2] has only one extra operator, called call/cc, that calls a function and passes the current continuation (i.e., a first class return statement) to it, e.g., let do_stuff ~cc:return = if world_is_bad then return () >>= fun () -> if moon_phase_is_bad then return () >>= fun () -> compute_some_stuff () let main () = Cont.call do_stuff The interesting thing with the non-delimited continuation is that `cc` here is a first class value that can be stored in a container, resumed multiple times, etc. This gives us enough freedom to implement lots of weird variants of a control flow, e.g., return statement, exceptions, couroutines, concurrency, and, probably, even the [COMEFROM][4] instruction. Basically, a continuation is a first class program label. Is it good or bad, you can decide yourself. Maybe this is too much freedom, however, this is totally a part of the lambda calculus, and is not using any type system escape hatches, like exceptions, even given that the `return` function has type `a -> 'b t`. P.S. Although I took your examples for demonstration purposes of the Cont monad, I still believe that for your particular case a non-total monad would be much nicer and more natural. Using the Monads library Error monad, it can be expressed as: let do_stuff () = if world_is_bad then failf "the world is wrong" () >>= fun () -> if moon_phase_is_bad then failf "look at the Moon!" () >>= fun () -> compute_some_stuff () The Error monad implements the Fail interface, that provides mechanisms for diverging the computation with an exception (not real exception of course), as well as provides the catch operator. The Error monad has a much stricter type discipline, and limited control flow variants, that can be considered as boon in most cases. [1]: http://kcsrk.info/ocaml/multicore/2015/05/20/effects-multicore/ [2]: http://binaryanalysisplatform.github.io/bap/api/v1.3.0/Monads.Std.html [3]: http://binaryanalysisplatform.github.io/bap/api/v1.3.0/Monads.Std.Monad.Cont.html [4]: https://en.wikipedia.org/wiki/COMEFROM [5]: http://binaryanalysisplatform.github.io/bap/api/v1.3.0/Monads.Std.Monad.Fail.S.html --001a1142ecd69bd03b055c5f2549 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Wed, Oct 25, 2017 at 4:35 AM, Richard W.M. Jones &= lt;rich@annexia.org> wrote:
<= br> Having said all that I was writing a little ML language last
year and I tried to implement a return statement, but it was very
awkward to work out how to map that to my lambda calculus, so
I understand how return statements are rather difficult to implement
in practice.

Rich.



The return statement is in fact= a tamed exception, as it provides an exceptional, i.e., a non-local contro= l flow. However, exceptions are not first class citizens in functional prog= ramming languages as they are not explicitly represented in typed lambda ca= lculus, and are not really represented in the type system (in a sence that = an expression with and without exception has the same type). Thus dealing w= ith expressions that may raise an exception is hard, as well as dealing wit= h any expression that has a side effect. OCaml multicore project is actuall= y bringing more than the multicore support, they also reify the effect syst= em into the language. Thus exceptions, as well as the return statements, ca= n be soon easily implemented on top of the effect system and can be reasone= d in a much more natural way.=C2=A0

With all that = said, safe and first class exceptions can be implemented in plain OCaml, or= any other functional programming language that provides higher order polym= orphism (type classes, functors, etc). The limited form of an exception can= be implemented even without it. As it was already noticed, the Maybe monad= , as well as the Error monad, or any other monad that reifies non-total com= putations can be used to implement a poor man return statement. The problem= is that when one computation yields the null value, the rest of the comput= ation chain is still evaluated. This is not a big issue if a chain is writt= en manually (i.e., is a block of code, like in your example), but it could = be serious if the chain is very long (i.e., processing a big list), or even= worse infininte. If the problem with a list of computations can be solved = on the monad implementation (as we do in the [Monads][2] library), the prob= lem with the infinite computation can be easily addressed in a non-total mo= nad.=C2=A0

The answer is to use the continuation p= assing style (CPS). We can use delimited continuations (as in the upcoming = multicore), or we can use plain non-delimited continuations. The rough idea= , is that if you have function that needs to escape the computation prematu= rely, you can pass a continuation to that function, e.g.,

=C2=A0 =C2=A0 =C2=A0let do_stuff return =3D=C2=A0
=C2=A0 = =C2=A0 =C2=A0 =C2=A0if world_is_bad then return None
=C2=A0 =C2= =A0 =C2=A0 =C2=A0else if moon_phase_is_bad then return None
=C2= =A0 =C2=A0 =C2=A0 =C2=A0else return (compute_some_stuff ())

<= /div>
You may notice, that we still need the else statement as our retu= rn function has type `'a -> 'a`, but for the non-local return we= need something of type `'a -> 'b`, to implement this we need to= switch to the continuation passing style, where each computation is a cont= inuation, i.e., a function of type `('a -> 'b) -> 'b`. Fo= r example, this is how the List.fold function will look in the CPS:

=C2=A0 =C2=A0 =C2=A0 =C2=A0 let fold xs ~init ~f =3D=
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 let rec loop xs k =3D match x= s with
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 | [] -> k
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 | x :: xs -> fun k'= ->=C2=A0 k (fun a -> loop xs (f a x) k') in
=C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 loop xs (fun k -> k init)

<= /div>
Programming in this style directly is a little bit cubersome, but= the good news, is that the continuation passing style can be encoded as a = monad. The [Continuation monad][2] has only one extra operator, called call= /cc, that calls a function and passes the current continuation (i.e., a fir= st class return statement) to it, e.g.,=C2=A0

=C2= =A0 =C2=A0 =C2=A0 =C2=A0let do_stuff ~cc:return =3D=C2=A0
=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0if world_is_bad then return () >>=3D fun (= ) ->=C2=A0
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0if moon_phase_is_= bad then return () >>=3D fun () ->
=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0compute_some_stuff ()

=C2=A0 =C2=A0 = =C2=A0let main () =3D Cont.call do_stuff=C2=A0

The= interesting thing with the non-delimited continuation is that=C2=A0 `cc` h= ere is a first class value that can be stored in a container, resumed multi= ple times, etc. This gives us enough freedom to implement lots of weird var= iants of a control flow, e.g., return statement, exceptions, couroutines, c= oncurrency, and, probably, even the [COMEFROM][4] instruction. Basically, a= continuation is a first class program label.=C2=A0

Is it good or bad, you can decide yourself. Maybe this is too much freedo= m, however, this is totally a part of the lambda calculus, and is not using= any type system escape hatches, like exceptions, even given that the `retu= rn` function has type `a -> 'b t`.=C2=A0=C2=A0

<= div>P.S. Although I took your examples for demonstration purposes of the Co= nt monad, I still believe that for your particular case a non-total monad w= ould be much nicer and more natural. Using the Monads library Error monad, = it can be expressed as:

=C2=A0 =C2=A0let do_stuff = () =3D=C2=A0
=C2=A0 =C2=A0 =C2=A0if world_is_bad then failf "= ;the world is wrong" () >>=3D fun () ->=C2=A0
=C2= =A0 =C2=A0 =C2=A0if moon_phase_is_bad then failf "look at the Moon!&qu= ot; () >>=3D fun () ->
=C2=A0 =C2=A0 =C2=A0compute_some_= stuff ()
=C2=A0=C2=A0
 --001a1142ecd69bd03b055c5f2549--