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 E61247F0D9 for ; Tue, 25 Aug 2015 14:09:11 +0200 (CEST) IronPort-PHdr: 9a23:0WfbqRSmj14SRJAofx0ZOR2POdpsv+yvbD5Q0YIujvd0So/mwa65ZxCN2/xhgRfzUJnB7Loc0qyN4/umBD1LuM7JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvioNuOMk4R3HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1gRVGMbjhoAKgTM6VnfX5P1vzGy4ulw3i+XIc3/QbkxXDWm66pxYBDtgSYDcTU+9TeTwsd5iaYTvQmsvQc3l4XdZYXQMPtlYovce8kbTCxPRJACeTZGB9aEboYVFedJFuZRqoP0vUdG+QO/CBO2CaXkyjZNjHbswYU92O0kFRnc20orGNdY4yecl8n8KKpHCbP996LP1ziWKqoOgTo= Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.chambart@ocamlpro.com; spf=None smtp.mailfrom=pierre.chambart@ocamlpro.com; spf=Pass smtp.helo=postmaster@redisdead.crans.org Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of pierre.chambart@ocamlpro.com) identity=pra; client-ip=138.231.136.39; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="pierre.chambart@ocamlpro.com"; x-sender="pierre.chambart@ocamlpro.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of pierre.chambart@ocamlpro.com) identity=mailfrom; client-ip=138.231.136.39; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="pierre.chambart@ocamlpro.com"; x-sender="pierre.chambart@ocamlpro.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@redisdead.crans.org designates 138.231.136.39 as permitted sender) identity=helo; client-ip=138.231.136.39; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="pierre.chambart@ocamlpro.com"; x-sender="postmaster@redisdead.crans.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DoAQD1WdxVgCeI54pdh326Z4UaglgCgTc6EgEBAQEBAQEBEAEBCxQHUYIdggcBAQQjBFERCxgCAgUWCwICCQMCAQIBRQYBDAgCiCqyOpUfAQEIAQEBAR6BIoo1hFc6gmmBQwEElTSVZZFchCaDOwEBAQ X-IPAS-Result: A0DoAQD1WdxVgCeI54pdh326Z4UaglgCgTc6EgEBAQEBAQEBEAEBCxQHUYIdggcBAQQjBFERCxgCAgUWCwICCQMCAQIBRQYBDAgCiCqyOpUfAQEIAQEBAR6BIoo1hFc6gmmBQwEElTSVZZFchCaDOwEBAQ X-IronPort-AV: E=Sophos;i="5.15,745,1432591200"; d="scan'208";a="143738983" Received: from redisdead.crans.org ([138.231.136.39]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-GCM-SHA384; 25 Aug 2015 14:09:11 +0200 Received: from [192.168.1.102] (perens.inria.fr [128.93.60.79]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by redisdead.crans.org (Postfix) with ESMTPSA id 9F0C0E9; Tue, 25 Aug 2015 14:09:10 +0200 (CEST) Message-ID: <55DC5AE6.9010902@ocamlpro.com> Date: Tue, 25 Aug 2015 14:09:10 +0200 From: Pierre Chambart Organization: OcamlPro User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.8.0 MIME-Version: 1.0 To: Kenneth Adam Miller , caml users References: In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit X-Validation-by: pierre.chambart@ocamlpro.com Subject: Re: [Caml-list] Type Encoding Format Control On 18/08/2015 19:06, 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. Note that there are some ways to avoid allocating options in tight loops using well chosen GADT and CPS style. With CPS style, it is possible to 'return' multiple values (as they are encoded as arguments to the continuation) and GADT's it is possible to encode the tag of a value outside of it, i.e. not needing to box to have different cases. This is kind of a heavy style, but if it is only for the tight loop, it may not matter. For instance, encoding a while loop accumulating on an option can look like: let f x = let r = ref None in while 'condition' do do_something ... if other_condition then r := Some (something) else r := None done Transformed to: type some_type = ... (the thing that will end up in the option) type _ arg = | None_arg : unit arg | Some_arg : some_type arg let f x = let rec loop : type t. t arg -> t -> unit = fun arg_kind r -> if condition then () else begin do_something ... if other_condition then loop Some_arg (something) else loop None_arg () in loop None_arg () Happy encoding ! -- Pierre