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