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 9293D7EEBF for ; Tue, 18 Aug 2015 21:44:46 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.177; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.177 as permitted sender) identity=mailfrom; client-ip=209.85.223.177; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-io0-f177.google.com) identity=helo; client-ip=209.85.223.177; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f177.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CJAQDKitNVm7HfVdFdhFgGgx7CYAKBMgdMAQEBAQEBEgEBAQEBBgsLCSEuhCQBAQQSER0BGx0BAwwGBQsNAgImAgIhAQERAQUBHAYTCBqHdgEDEq5LgS8+MYtAgWyCeYsFChknDVeFAAEBAQEGAQEBARgBBQ6BFIoxgk+COweCaYFDBYxfiEKKf4FtgUqRL4NPghsSI4EXF4QOPDOCTAEBAQ X-IPAS-Result: A0CJAQDKitNVm7HfVdFdhFgGgx7CYAKBMgdMAQEBAQEBEgEBAQEBBgsLCSEuhCQBAQQSER0BGx0BAwwGBQsNAgImAgIhAQERAQUBHAYTCBqHdgEDEq5LgS8+MYtAgWyCeYsFChknDVeFAAEBAQEGAQEBARgBBQ6BFIoxgk+COweCaYFDBYxfiEKKf4FtgUqRL4NPghsSI4EXF4QOPDOCTAEBAQ X-IronPort-AV: E=Sophos;i="5.15,704,1432591200"; d="scan'208";a="173999338" Received: from mail-io0-f177.google.com ([209.85.223.177]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 18 Aug 2015 21:44:45 +0200 Received: by iods203 with SMTP id s203so202284895iod.0 for ; Tue, 18 Aug 2015 12:44:44 -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=vczd01JwddFpN7GI74oNdWQJnoFDKue7ED+Fnb3yrso=; b=yKA/MDRhfmnDdl6Df0ReUawj/cQdMdeQ0Kd4/xj9uhH4i1Zk1pzOKPjuKLCYOgAMn7 xU9nLPv5F7OVO7i4WdTAKkc7IayLwTSMGjtgnfc9CxeE6IDatDk2FmoxPpJRWke0ebJA QKQ7Ub7GK73OAy0CzKq42Oco7J4wdKnHdBM33KhJ3iGCnJXdlWJbcOcakxq11B5TVA2c bt96vuMHw3jXWDtAXdtzVW8PyzzonJB3FxJmB2ZrcoMLrqd+cnkvgeFAqdZ2c1nzdnXU l27CDeGgzb490/JGosPtdGfDLdvxLirYPNl3RONpo1Y8x2S2dC8lGzdmkbHz0FeFIRub w5uw== X-Received: by 10.107.19.94 with SMTP id b91mr8279395ioj.144.1439927084155; Tue, 18 Aug 2015 12:44:44 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.68.132 with HTTP; Tue, 18 Aug 2015 12:44:04 -0700 (PDT) In-Reply-To: References: <20150818185751.GC650@topoi.pooq.com> From: Gabriel Scherer Date: Tue, 18 Aug 2015 21:44:04 +0200 Message-ID: To: Kenneth Adam Miller Cc: Hendrik Boom , caml users Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Type Encoding Format Control 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 > >