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 470277FACD for ; Tue, 30 Sep 2014 11:08:28 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.179 as permitted sender) identity=mailfrom; client-ip=209.85.214.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; 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-ob0-f179.google.com) identity=helo; client-ip=209.85.214.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ob0-f179.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArQBAEZyKlTRVdazm2dsb2JhbABghDgEgn7ObwKBCggWAREBAQEBAQYLCwkULIQEAQEDARIRHQEbHQEDDAYFBAc3AgIiAREBBQEcGQgaiAcBAwkInHhuizCBcoMQiRkKGScNZ4Y3AREBBQ6PKGgHgniBUwWSaoo+k2sYKYUWOy+CSgEBAQ X-IPAS-Result: ArQBAEZyKlTRVdazm2dsb2JhbABghDgEgn7ObwKBCggWAREBAQEBAQYLCwkULIQEAQEDARIRHQEbHQEDDAYFBAc3AgIiAREBBQEcGQgaiAcBAwkInHhuizCBcoMQiRkKGScNZ4Y3AREBBQ6PKGgHgniBUwWSaoo+k2sYKYUWOy+CSgEBAQ X-IronPort-AV: E=Sophos;i="5.04,625,1406584800"; d="scan'208";a="81366231" Received: from mail-ob0-f179.google.com ([209.85.214.179]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 30 Sep 2014 11:08:27 +0200 Received: by mail-ob0-f179.google.com with SMTP id wp4so1124031obc.24 for ; Tue, 30 Sep 2014 02:08:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=wSbInKI65H7NL7BY++TAP2lbIb4sujXtXSH5VIylxp4=; b=KQ45rhor8QQaDLZaDAc5lqRSp0QXmN7caLO1a+D0EbpfKLXyk4A48w540mOkE+qB94 eCY7uArvzBhODR7T9Zv3S+rcgzlfJhfT/KDPfNshxEPTYQdMSSkF4RJUNetL8EKhefps KPCw5dX//m06u9joV8Fcnb+kasRh+A7sSrjSzfjBb07j2F3CcOT7kjgKJUGPftj5j8sO vMGpl75MggrRRckU2H6VTmuawiBUyl2ln6wJ6d5D8cuTy6/uyoWsS8RQ669bRAHwT0Dq gTVpva2hi95GKj/NGQs/lVQq3n+aj/exdjVw6QnUqvzqYQpdpH9jFNyo7CcwRINMesw7 M5Og== X-Received: by 10.182.38.138 with SMTP id g10mr46003885obk.21.1412068105766; Tue, 30 Sep 2014 02:08:25 -0700 (PDT) MIME-Version: 1.0 Received: by 10.76.105.196 with HTTP; Tue, 30 Sep 2014 02:07:45 -0700 (PDT) In-Reply-To: <20140930084641.1FFBAC3825@www1.g3.pair.com> References: <20140930084641.1FFBAC3825@www1.g3.pair.com> From: Gabriel Scherer Date: Tue, 30 Sep 2014 11:07:45 +0200 Message-ID: To: oleg@okmij.org Cc: Goswin von Brederlow , caml users Content-Type: multipart/alternative; boundary=001a11c2ec5ad7cb99050444b97c Subject: Re: [Caml-list] Why List.map does not be implemented --001a11c2ec5ad7cb99050444b97c Content-Type: text/plain; charset=UTF-8 That is an extremely interesting story that I would like to understand better. Which pointers would you recommend to read more about mutation in HANSEI? My intuition would be that the mutation should not be observable in this case, as it is only done on "private" data that the List.map function allocate, owns, and which never escapes in its immutable form. While I understand why mutating global data is an observable side-effect that can play badly with any form of backtracking/probabilistic monad, I do not have any intuition about why mutating a privately-owned heap fragment would perturb the system. If I was pressed to make an hypothesis (while not knowing the system), I would guess that this is because of an implementation detail of HANSEI, not because of its actual semantic requirements. On Tue, Sep 30, 2014 at 10:46 AM, wrote: > > Gabriel Scherer wrote > > it is safe to Obj.magic a mutable data-structure into an immutable > > one. The Obj.magic-using code for List.map, implemented in Extlib and > > inherited by Batteries, is careful to use an unsafe cast in exactly > > the second situation. This is a feature that other languages > > (eg. Mezzo) safely provide. > > Let me relay a short anecdote about the List.map function in > Batteries. Once I received a message from a person who was using the > Hansei library of probabilistic programming. He reported a problem: > his program produced clearly wrong results. He even traced the problem > to the function 'List.map' -- saying that if he wrote List.map himself, > the problem disappeared. I was initially puzzled: how one can possibly > mis-write List.map. I asked for more details and he said that he was > using Batteries. That gave me a hunch: I went to the Battery > repository to look at the source code and found what I expected -- > mutation. In probabilistic programs, mutation has to be done > carefully. Mutation to the global heap forces correlation on what > should be independent ``possible worlds''. Mutation has to be done > with world-local heaps, which Hansei provides for that purpose. There > are times when hidden optimizations come to bite us. > > I guess in Mezzo I would have seen from the type that a mutation is > performed, and would have avoided the optimized Map (or the type > checker would make me avoid it). > > --001a11c2ec5ad7cb99050444b97c Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
That is an extremely interesting story that I would like t= o understand better. Which pointers would you recommend to read more about = mutation in HANSEI?

My intuition would be that the mutat= ion should not be observable in this case, as it is only done on "priv= ate" data that the List.map function allocate, owns, and which never e= scapes in its immutable form. While I understand why mutating global data i= s an observable side-effect that can play badly with any form of backtracki= ng/probabilistic monad, I do not have any intuition about why mutating a pr= ivately-owned heap fragment would perturb the system. If I was pressed to m= ake an hypothesis (while not knowing the system), I would guess that this i= s because of an implementation detail of HANSEI, not because of its actual = semantic requirements.

On Tue, Sep 30, 2014 at 10:46 AM, <<= a href=3D"mailto:oleg@okmij.org" target=3D"_blank">oleg@okmij.org> wrote:

Gabriel Scherer wrote
> it is safe to Obj.magic a mutable data-structure into an immutable
> one. The Obj.magic-using code for List.map, implemented in Extlib and<= br> > inherited by Batteries, is careful to use an unsafe cast in exactly
> the second situation. This is a feature that other languages
> (eg. Mezzo) safely provide.

Let me relay a short anecdote about the List.map function in
Batteries. Once I received a message from a person who was using the
Hansei library of probabilistic programming. He reported a problem:
his program produced clearly wrong results. He even traced the problem
to the function 'List.map' -- saying that if he wrote List.map hims= elf,
the problem disappeared. I was initially puzzled: how one can possibly
mis-write List.map. I asked for more details and he said that he was
using Batteries. That gave me a hunch: I went to the Battery
repository to look at the source code and found what I expected --
mutation. In probabilistic programs, mutation has to be done
carefully. Mutation to the global heap forces correlation on what
should be independent ``possible worlds''. Mutation has to be done<= br> with world-local heaps, which Hansei provides for that purpose. There
are times when hidden optimizations come to bite us.

I guess in Mezzo I would have seen from the type that a mutation is
performed, and would have avoided the optimized Map (or the type
checker would make me avoid it).


--001a11c2ec5ad7cb99050444b97c--