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 4AA067EEBF for ; Thu, 20 Aug 2015 11:10:55 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.17.11; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of goswin-v-b@web.de designates 212.227.17.11 as permitted sender) identity=mailfrom; client-ip=212.227.17.11; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; 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@mout.web.de) identity=helo; client-ip=212.227.17.11; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0ApAgCImNVVnAsR49RdhFjFTwKBMEwBAQEBAQESAQEBAQEGDQkJIS6EIwEBAQMBJxNECwsYCSUPBQ0bNIgYAQMKDMkEHysNhVcBCyCLU4JPgkKDGIEUBYxjiEWLAoFqgU2HGAyKFINPg2mEJW+CTAEBAQ X-IPAS-Result: A0ApAgCImNVVnAsR49RdhFjFTwKBMEwBAQEBAQESAQEBAQEGDQkJIS6EIwEBAQMBJxNECwsYCSUPBQ0bNIgYAQMKDMkEHysNhVcBCyCLU4JPgkKDGIEUBYxjiEWLAoFqgU2HGAyKFINPg2mEJW+CTAEBAQ X-IronPort-AV: E=Sophos;i="5.15,714,1432591200"; d="scan'208";a="174280210" Received: from mout.web.de ([212.227.17.11]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 20 Aug 2015 11:10:54 +0200 Received: from frosties.localnet ([95.208.221.151]) by smtp.web.de (mrweb102) with ESMTPSA (Nemesis) id 0Ljaiq-1YvCuT4AMi-00bXzs for ; Thu, 20 Aug 2015 11:10:54 +0200 Received: from mrvn by frosties.localnet with local (Exim 4.84) (envelope-from ) id 1ZSLs5-00049y-BC for caml-list@inria.fr; Thu, 20 Aug 2015 11:10:53 +0200 Date: Thu, 20 Aug 2015 11:10:53 +0200 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20150820091051.GA15458@frosties> References: <20150818185751.GC650@topoi.pooq.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-Provags-ID: V03:K0:RgAR2UC0v1nOBKAs9fQc0MBFWel7JMTtwRKE/wz8m2Oe/klKv4S kb8rhWVNsaHbHAIHmGh96Vg90/ue/oCgSGO9cIDaPlv3YziYYJKIA/lIOTr76VAscbdpbCg W37u0DfMBgjEuFsuAGwUMqZrbpKsoClWYnqq2BgCta4MCFpUpF1k3FPfotDi2qhSAAaDOfa j39gol4qTeGN+kZbmp1zw== X-UI-Out-Filterresults: notjunk:1;V01:K0:H0ptdwj0nec=:5MoW1clCIi2H9llbi9yhVL IzBMxqQHcz9UeEBzN72kzp4+8F+uJTnWEqRJVoIXQrkyxZZWviem0gMd9eKvRoZUGJTSYVD/m v+bh3vN/vnICVnxp7eWsNa9ugoRj5ihaStT4TJRZ0t0oIPTDEfx43x7PWUWBM+a/I+g/jox7E b+qabZyLiCURJcCjSbxWcXek3iFG6SN8mc7IBDgmBJuMxP720UYYc2jelLksdZfZOUaPmQOmj 1oD6vhl9q9eprc6EcwbOIR2rehmdXz+Ooid18wXPXCmnW/s+EhEjjnb4nPrd/XUkIuSZFBJvz 9kSW+Ni0akopKCv1vFtSTf20KVPHtv0fkrr5yuKDRxso9EUS8Yl0JsgWZ+cTATbIUAgppeF0v 6A4aKYDqghFHymwFksG4i3iNZXZp+6jTkDtnjihMpzYWikW7D5EEjBrOXUkkkVZfwvzntnuqV e6PPYf/ibuojSGGKcZgxjW704sXD1H/FFWdWZmYaCWwRrH3I+XHgUpj2IgRmFlDjiC3S5XLJ6 GpUkuNmb+qEvMZ1ppfMmlT70OgaN6NzRCYdOJet8Q3Fv0WNZ/wTahXh86eitmoDXzDVmI2u2L SOWjvIff3OWUUrp3p2zgrRTFgfmWAw4y2m7rfEgBYSIjIYJ7+Qhzte/6gepu7aGAQbWdiicMx g0045BDgRcT4yxzvAeEQQYVedCJCVbK59H0FQD666A+kQd7betwbPjFXuuqCjfKmmE5kF+6R3 S0gVk5uWrNw4VvI5 Subject: Re: [Caml-list] Type Encoding Format Control On Tue, Aug 18, 2015 at 09:44:04PM +0200, Gabriel Scherer wrote: > We've discussed optimisations of ('a option) in the past. Certainly > some things could be done, but it's unclear to me how much value there is in > optimizing ('a option) specifically: what if, for example, we later > understand that ('a, exn) result is the more general abstraction that > we should have used instead, and rely on it heavily in libraries, will > we de-optimize options and work on optimizing results? > > Note that your idea of "either a failure of a value" can be achieved, > in some monomorphic cases (specifically when you know 'a and it has a > product structure) by using a specific type declaration: > > type my_struct = > | None > | Some of int * int array * string > > This will be represented as efficiently as the tuple (int * int array > * string), yet it has a default case (or two, or another case with > exceptions, whatever -- this is more flexible than just options). With > inline records in 4.03 -- not yet released -- you will even be able to > have some of the product structure mutable: > > type my_struct = > | None > | Some of { mutable count : int; values : int array; name : string } Except here you are talking about an already boxed value. The Some part is encoded in the tag of the box you already have. In the case of a pointer you have not box to put the Some tag on. > On Tue, Aug 18, 2015 at 9:01 PM, Kenneth Adam Miller > wrote: > > Well, it's not restricted to pointers - In general I would think that the > > type annotation for Some | None would be left alone. I just used pointer as > > an example because pointers exclude a value, 0x0, from the valid set. In > > which case None is encoded as 0x0. > > > > Thanks for the bit about polymorphism in the context of what a compiler > > would see - clients that do not see the hypothetical additional annotation > > for that specific type to allow a format wouldn't have the augmented > > operational needs to work on such an instance correctly. Got it! There are 2 problems: 1) polymorphism A function taking an 'a option could get 0, which it would easily detect as 0, a pointer to some value or a pointer to box taged Some. But there is no way to separate the last two cases. The pointer doesn't even have to point to an ocaml value so dereferencing and checking if it is a box with Some tag is not an option. And even if you could any variant type with a boxed constructor will have a tag of 0, same as Some. Having different representation for pointer option and other option doesn't work. 2) 'a option option For 'a option None becomes 0x0 and Some pointer becomes pointer. But what about 'a option option. Do you repeat the process? Then None and Some None would both become 0x0 and can't be separated. And if you don't repeat the process you break polymorphism (see 1). What you can do is create a new type that behaves like type 'a ptr_option = NULL | 'a but the type would have to be abstract and you would have to have a function to convert it into an 'a option for pattern matching like match to_option ptr_opt with | None -> ... | Some ptr -> ... and hope the optimizer eliminates the allocation and boxing. Doesn't ocaml-ctypes already have such a type? > > On Tue, Aug 18, 2015 at 2:57 PM, Hendrik Boom > > wrote: > >> > >> On Tue, Aug 18, 2015 at 01:06:55PM -0400, Kenneth Adam Miller wrote: > >> > I was wondering if cases where format control is possible in typing > >> > constructs can allow things like restricting the implementation size > >> > after > >> > compilation of a specific variant type. Say, for instance that I wanted > >> > to > >> > have a malloc implementation instead of returning a Some 'a | None type > >> > that compiles down to a boxed case of first a word and then the > >> > subsequent > >> > 'a instance, down to the 'a instance, where in the values of the word > >> > enum > >> > (or tag) are not present in the possibilities of the 'a instance. > >> > > >> > Maybe it sounds silly, but in really tight loops you want to squeeze for > >> > efficiency. So I was wondering if maybe the same actual code be used > >> > with > >> > the same sanity of type checking, but some annotation provided at the > >> > type > >> > declaration to allow such optimization to take place. > >> > >> Let's see. OCaml steals a bit to indicate whether a valus is a pointer > >> or not, right? Could that bit see duual usage for the option type? So > >> that if it's an optional pointer type, the bit is left off, and if it's > >> an optional nonpointer type, it's turned on (and set to point to > >> location zero, which the GC couls check for)? > >> > >> THe proble I see with this is if the 'a is passed to a generic function > >> where iti isn't statically known where it's a pinter or not. The > >> conpiler will not know whether to test for absence or presence of the > >> bit. > >> > >> -- hendrik MfG Goswin