caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
To: Alain Frisch <alain@frisch.fr>
Cc: Mailing List OCaml <caml-list@inria.fr>,
	Gerd Stolpmann <info@gerd-stolpmann.de>
Subject: Re: [Caml-list] Immutable strings
Date: Tue, 8 Jul 2014 23:04:25 +0900	[thread overview]
Message-ID: <CA+p7B-xKU0sXG-4jLQZ-Fgry2+wQSq5Gs0es_UAS+nDaCL_xMw@mail.gmail.com> (raw)
In-Reply-To: <53BBF406.9060909@frisch.fr>

[-- Attachment #1: Type: text/plain, Size: 1491 bytes --]

2014/07/08 22:38 "Alain Frisch" <alain@frisch.fr>:
>
> On 07/08/2014 03:23 PM, Jacques Garrigue wrote:
>>
>> Alain’s idea of using an extra type-only parameter (‘a is_a_type) works,
>> and it doesn’t 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 = String and it would copy them when
'a = Bytes.  Similarly, a function could memoize some strings it produces
in order to return them later again, but only when 'a = String, not 'a =
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

[-- Attachment #2: Type: text/html, Size: 1850 bytes --]

  reply	other threads:[~2014-07-08 14:04 UTC|newest]

Thread overview: 29+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2014-07-04 19:18 Gerd Stolpmann
2014-07-04 20:31 ` Anthony Tavener
2014-07-04 20:38   ` Malcolm Matalka
2014-07-04 23:44   ` Daniel Bünzli
2014-07-05 11:04   ` Gerd Stolpmann
2014-07-16 11:38     ` Damien Doligez
2014-07-04 21:01 ` Markus Mottl
2014-07-05 11:24   ` Gerd Stolpmann
2014-07-08 13:23     ` Jacques Garrigue
2014-07-08 13:37       ` Alain Frisch
2014-07-08 14:04         ` Jacques Garrigue [this message]
2014-07-28 11:14   ` Goswin von Brederlow
2014-07-28 15:51     ` Markus Mottl
2014-07-29  2:54       ` Yaron Minsky
2014-07-29  9:46         ` Goswin von Brederlow
2014-07-29 11:48         ` John F. Carr
2014-07-07 12:42 ` Alain Frisch
2014-07-08 12:24   ` Gerd Stolpmann
2014-07-09 13:54     ` Alain Frisch
2014-07-09 18:04       ` Gerd Stolpmann
2014-07-10  6:41         ` Nicolas Boulay
2014-07-14 17:40       ` Richard W.M. Jones
2014-07-08 18:15 ` mattiasw
2014-07-08 19:24   ` Daniel Bünzli
2014-07-08 19:27     ` Raoul Duke
2014-07-09 14:15   ` Daniel Bünzli
2014-07-14 17:45   ` Richard W.M. Jones
2014-07-21 15:06 ` Alain Frisch
     [not found]   ` <20140722.235104.405798419265248505.Christophe.Troestler@umons.ac.be>
2014-08-29 16:30     ` Damien Doligez

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CA+p7B-xKU0sXG-4jLQZ-Fgry2+wQSq5Gs0es_UAS+nDaCL_xMw@mail.gmail.com \
    --to=garrigue@math.nagoya-u.ac.jp \
    --cc=alain@frisch.fr \
    --cc=caml-list@inria.fr \
    --cc=info@gerd-stolpmann.de \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).