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 0C0927FA13 for ; Tue, 8 Jul 2014 16:04:27 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jacques.garrigue@gmail.com) identity=pra; client-ip=209.85.223.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="jacques.garrigue@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of jacques.garrigue@gmail.com designates 209.85.223.175 as permitted sender) identity=mailfrom; client-ip=209.85.223.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="jacques.garrigue@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-ie0-f175.google.com) identity=helo; client-ip=209.85.223.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="postmaster@mail-ie0-f175.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjcBAHL5u1PRVd+vlGdsb2JhbABZhDqCb6t9mGkIFg8BAQEBBwsLCRIqhAMBAQEDARIRBBkBOAEDAQsBBQUEBw0qAgIiEgEFARwGEyKIDAMJCKNxaosnhQKOAicNV4UmEQEFDpIygUwFik+MDYQakhsYKYFqgxgu X-IPAS-Result: AjcBAHL5u1PRVd+vlGdsb2JhbABZhDqCb6t9mGkIFg8BAQEBBwsLCRIqhAMBAQEDARIRBBkBOAEDAQsBBQUEBw0qAgIiEgEFARwGEyKIDAMJCKNxaosnhQKOAicNV4UmEQEFDpIygUwFik+MDYQakhsYKYFqgxgu X-IronPort-AV: E=Sophos;i="5.01,625,1400018400"; d="scan'208";a="84161218" Received: from mail-ie0-f175.google.com ([209.85.223.175]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Jul 2014 16:04:26 +0200 Received: by mail-ie0-f175.google.com with SMTP id at20so2217136iec.34 for ; Tue, 08 Jul 2014 07:04:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:date:message-id:subject :from:to:cc:content-type; bh=4h3DAIR1Bvfss7/mKPMotkYQDYXN+QIq2Uii/iAc+Zc=; b=r7IVTkDmhFp6En59u+l2mGbeuGh6uaEvTKVnsFHNrcfTgBmAhG+SrxmwMjKHeHRCx7 GamK9CrkMutnW1TSrnpiUH5ZJ2SxTUaozxZqpr7BJLSYX9eYNXlbIuNppacpMcXdJhRu JLKmltgH9FPkfUM36ou+OtkSDMxTXAKueni9Dd6ko6O1z2KjgtQob3yJK/mGEq9f5fdg 3d/Br/vLhRVGVtMOSH3RwPp/mP4PBZ578UCeUAKKyy7W9QVYQUo9s3C0JMi887c/1C1H eM/ol47Ynx02znVHWVzpXyOm8hKucMJ5LA77kHR2JuDIIRCppE6coySB/xyGDexohoCd 6PjQ== MIME-Version: 1.0 X-Received: by 10.42.72.198 with SMTP id p6mr39372446icj.52.1404828265356; Tue, 08 Jul 2014 07:04:25 -0700 (PDT) Sender: jacques.garrigue@gmail.com Received: by 10.50.20.37 with HTTP; Tue, 8 Jul 2014 07:04:25 -0700 (PDT) Received: by 10.50.20.37 with HTTP; Tue, 8 Jul 2014 07:04:25 -0700 (PDT) In-Reply-To: <53BBF406.9060909@frisch.fr> References: <1404501528.4384.4.camel@e130> <1404559455.4384.32.camel@e130> <53BBF406.9060909@frisch.fr> Date: Tue, 8 Jul 2014 23:04:25 +0900 X-Google-Sender-Auth: pxRlJnhYBsgmGla_Z16Q_QD6EiY Message-ID: From: Jacques Garrigue To: Alain Frisch Cc: Mailing List OCaml , Gerd Stolpmann Content-Type: multipart/alternative; boundary=90e6ba613b9aba240b04fdaf1128 Subject: Re: [Caml-list] Immutable strings --90e6ba613b9aba240b04fdaf1128 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 2014/07/08 22:38 "Alain Frisch" : > > On 07/08/2014 03:23 PM, Jacques Garrigue wrote: >> >> Alain=E2=80=99s idea of using an extra type-only parameter (=E2=80=98a i= s_a_type) works, >> and it doesn=E2=80=99t really need to be a GADT. >> But this is a bit strange to use an extra parameter where a phantom type >> on string itself would solve the problem. > > > I mentioned that some functions could behave differently according to the requested result type. For instance, a function > > val of_bool: 'a is_a_string -> bool -> 'a > > would return string literals when 'a =3D String and it would copy them wh= en 'a =3D Bytes. Similarly, a function could memoize some strings it produces in order to return them later again, but only when 'a =3D String, not 'a =3D Bytes. I see. But in that case we could also have different functions, since the semantics change (at least for physical equality) > Even for functions such as "copy" or "sub", it makes sense to avoid a copy in some cases (when both the input and the output are immutable, and for sub, when the range covers the entire input). Ok, but in that case you will need a flag for both input and output strings, since there is no way to recover this information from the string itself. > So I don't think that "'a is_a_string" can really be only a phantom type. I see. I think that both approaches have interesting applications. But from a type system point of view they are clearly advanced. Jacques --90e6ba613b9aba240b04fdaf1128 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

2014/07/08 22:38 "Alain Frisch" <alain@frisch.fr>:
>
> On 07/08/2014 03:23 PM, Jacques Garrigue wrote:
>>
>> Alain=E2=80=99s idea of using an extra type-only parameter (=E2=80= =98a is_a_type) works,
>> and it doesn=E2=80=99t really need to be a GADT.
>> But this is a bit strange to use an extra parameter where a phanto= m type
>> on string itself would solve the problem.
>
>
> I mentioned that some functions could behave differently according to = the requested result type. =C2=A0For instance, a function
>
> =C2=A0val of_bool: 'a is_a_string -> bool -> 'a
>
> would return string literals when 'a =3D String and it would copy = them when 'a =3D Bytes. =C2=A0Similarly, a function could memoize some = strings it produces in order to return them later again, but only when '= ;a =3D String, not 'a =3D Bytes.

I see. But in that case we could also have different functio= ns, since the semantics change (at least for physical equality)

> Even for functions such as "copy" or "su= b", it makes sense to avoid a copy in some cases (when both the input = and the output are immutable, and for sub, when the range covers the entire= input).

Ok, but in that case you will need a flag for both input and= output strings, since there is no way to recover this information from the= string itself.

> So I don't think that "'a is_a_string"= ; can really be only a phantom type.

I see.
I think that both approaches have interesting applications.
But from a type system point of view they are clearly advanced.

Jacques

--90e6ba613b9aba240b04fdaf1128--