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 CD3977EEBF for ; Tue, 18 Aug 2015 21:55:17 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of kennethadammiller@gmail.com) identity=pra; client-ip=209.85.214.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="kennethadammiller@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of kennethadammiller@gmail.com designates 209.85.214.174 as permitted sender) identity=mailfrom; client-ip=209.85.214.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="kennethadammiller@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-f174.google.com) identity=helo; client-ip=209.85.214.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="postmaster@mail-ob0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CKAQAnjdNVm67WVdFdhEkPBoMewmACgTIHTAEBAQEBARIBAQEBAQYLCwkhLoQjAQEBAwESER0BGx0BAwELBgULDSoCAiEBAREBBQEcBhMih3YBAwoIrkWBLz4xi0CBbIJ5iwYKGScNV4UAAQEBAQEFAQEBAQEBARUBBQ6LRYJPgVdkB4JpgUMFjF+IQop/gW2BSpEvg0+CGxIjgRcXhCgiM4JMAQEB X-IPAS-Result: A0CKAQAnjdNVm67WVdFdhEkPBoMewmACgTIHTAEBAQEBARIBAQEBAQYLCwkhLoQjAQEBAwESER0BGx0BAwELBgULDSoCAiEBAREBBQEcBhMih3YBAwoIrkWBLz4xi0CBbIJ5iwYKGScNV4UAAQEBAQEFAQEBAQEBARUBBQ6LRYJPgVdkB4JpgUMFjF+IQop/gW2BSpEvg0+CGxIjgRcXhCgiM4JMAQEB X-IronPort-AV: E=Sophos;i="5.15,704,1432591200"; d="scan'208";a="143090187" Received: from mail-ob0-f174.google.com ([209.85.214.174]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 18 Aug 2015 21:55:08 +0200 Received: by obbop1 with SMTP id op1so151137698obb.2 for ; Tue, 18 Aug 2015 12:55:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=ZR5UPB1j05SIz4DhSkazswFsWMqtY4Hq41FjNANXUE8=; b=qoMjNU2ql5jFEu2WcSe/esd2kxLVvKNlNYkN4tOpbt2N4NbQpPgh6gsnf6/vD8yvZA Y+v1XtquleJhOF8//JO7EOn+jaS+AqLX5KH8uN0KVzYdJiZWqrJbIAam6oAg3oVSpHE7 MnP47wuQcmMH7dw8vhm3IHkNfQ4w1R/Ckx/Tf/lEgpKigIvvnxyw0RrY1JXpM79C2znY woGNM/etUDue/LPyX5EtQD6sgBTNYZj94TKsZ5mmltnMXjsWkyFRLQRzgdjySPk9tvUT 3sgwe4DvaPSTHCa7qaNeh+VP7xlcaJgEcUGK7b6ZczRqHXBZpg4xcDw29r3nD3Mothry hckQ== MIME-Version: 1.0 X-Received: by 10.60.76.4 with SMTP id g4mr7249293oew.81.1439927706693; Tue, 18 Aug 2015 12:55:06 -0700 (PDT) Received: by 10.202.191.8 with HTTP; Tue, 18 Aug 2015 12:55:06 -0700 (PDT) In-Reply-To: References: <20150818185751.GC650@topoi.pooq.com> Date: Tue, 18 Aug 2015 15:55:06 -0400 Message-ID: From: Kenneth Adam Miller To: Gabriel Scherer Cc: Hendrik Boom , caml users Content-Type: multipart/alternative; boundary=047d7b33d4aa75b6b3051d9b4bb1 Subject: Re: [Caml-list] Type Encoding Format Control --047d7b33d4aa75b6b3051d9b4bb1 Content-Type: text/plain; charset=UTF-8 I wouldn't know future route in regards to the question about preferring exceptions instead later. I wouldn't say go back and undo anything necessarily, my idea about how this would be implemented would be an extra annotation that allows the compiler to see that there are potential value instances of such a type that allow excision of the tag. In the case of my_struct, you would have instead maybe some extension to the vernacular like: type my_struct = | None | Some of int * int array * string where_instance 0 * [||] * "" is None In this case, you could continue your annotation of the type my_struct with more expressive capabilities for situations where there is more than one hole that represents None. I don't really believe this constitutes so much value in a language that's already fast. It would be line noise in almost all applications, and users might not have incentives to draw from such a language feature unless they were pushing for improvements in some very tight loop. It was just a curiosity. On Tue, Aug 18, 2015 at 3:44 PM, 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 } > > 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! > > > > 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 > > > > > --047d7b33d4aa75b6b3051d9b4bb1 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I wouldn't know future route in regards to the questio= n about preferring exceptions instead later. I wouldn't say go back and= undo anything necessarily, my idea about how this would be implemented wou= ld be an extra annotation that allows the compiler to see that there are po= tential value instances of such a type that allow excision of the tag.
=
In the case of my_struct, you would have instead maybe some = extension to the vernacular like:

type my_struct = =3D=C2=A0
=C2=A0 | None
=C2=A0 | Some of int * int arra= y * string where_instance 0 * [||] * "" is None

In this case, you could continue your annotation of the type my_str= uct with more expressive capabilities for situations where there is more th= an one hole that represents None.

I don't real= ly believe this constitutes so much value in a language that's already = fast. It would be line noise in almost all applications, and users might no= t have incentives to draw from such a language feature unless they were pus= hing for improvements in some very tight loop. It was just a curiosity.

On Tue, A= ug 18, 2015 at 3:44 PM, Gabriel Scherer <gabriel.scherer@gmail.com= > wrote:
We've discusse= d 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 achie= ved,
in some monomorphic cases (specifically when you know 'a and it has a product structure) by using a specific type declaration:

=C2=A0 type my_struct =3D
=C2=A0 =C2=A0 | None
=C2=A0 =C2=A0 | 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:

=C2=A0 type my_struct =3D
=C2=A0 =C2=A0 | None
=C2=A0 =C2=A0 | Some of { mutable count : int; values : int array; name : s= tring }

On Tue, Aug 18, 2015 at 9:01 PM, Kenneth Adam Miller
<kennethadammiller@gmail.= com> wrote:
> Well, it's not restricted to pointers - In general I would think t= hat the
> type annotation for Some | None would be left alone. I just used point= er 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 compile= r
> would see - clients that do not see the hypothetical additional annota= tion
> for that specific type to allow a format wouldn't have the augment= ed
> operational needs to work on such an instance correctly. Got it!
>
> On Tue, Aug 18, 2015 at 2:57 PM, Hendrik Boom <hendrik@topoi.pooq.com>
> wrote:
>>
>> On Tue, Aug 18, 2015 at 01:06:55PM -0400, Kenneth Adam Miller wrot= e:
>> > I was wondering if cases where format control is possible in = typing
>> > constructs can allow things like restricting the implementati= on size
>> > after
>> > compilation of a specific variant type. Say, for instance tha= t 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 t= he
>> > subsequent
>> > 'a instance, down to the 'a instance, where in the va= lues of the word
>> > enum
>> > (or tag) are not present in the possibilities of the 'a i= nstance.
>> >
>> > 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 provide= d at the
>> > type
>> > declaration to allow such optimization to take place.
>>
>> Let's see.=C2=A0 OCaml steals a bit to indicate whether a valu= s is a pointer
>> or not, right?=C2=A0 Could that bit see duual usage for the option= type?=C2=A0 So
>> that if it's an optional pointer type, the bit is left off, an= d 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 no= t.=C2=A0 The
>> conpiler will not know whether to test for absence or presence of = the
>> bit.
>>
>> -- hendrik
>
>

--047d7b33d4aa75b6b3051d9b4bb1--